写完之后我突然发现这个标题看上去貌似有“以下实现是由本人完成的”这样的误导，所以特此澄清，下文出现的代码统统摘自
apache/spark.
首先简单介绍 SVD++ 算法在协同过滤中的应用及其数学直觉。
考虑 CF 中最为常见的用户给电影评分的场景，我们需要一个数学模型来模拟用户给电影打分的场景，i.e. 对评分进行预测。
一个 Naive 的方案可以是将评分矩阵看作是两个矩阵的乘积：
$$
U = \begin{bmatrix}
u_{11} & \cdots & u_{1k} \\
\vdots & \ddots & \vdots \\
u_{m1} & \cdots & u_{mk}
\end{bmatrix}
\begin{bmatrix}
i_{11} & \cdots & i_{1n} \\
\vdots & \ddots & \vdots \\
i_{k1} & \cdots & i_{kn}
\end{bmatrix}
$$.
最近搬了个地儿，离开了生活了近6年的合肥。呆在合肥的时候不觉得她有什么不好，现在想想空气质量是真不照；呆在合肥的时候不觉得她有什么好，现在想想吃饭是真便宜。
总之就是这段时间一堆烂事，导致前边挖下的坑没能及时填上。另外，随着研究方向的逐渐明确，也许不能再写这些“不务正业”的玩意了，也许会写点跟方向相关的内容，虽然我觉得这个方向上的工作纯忽悠，完全不值一提。我就是一个始终觉得别人研究的东西无比高大上，自己手上的东西都是crap的人。
上一篇结尾提到的那篇论文总算是看完了。既然不能完全消化，吸收，然后拉出屎来；那么我就简单粗暴地吞下去，嚼一嚼，吐出来好了（美其名曰翻译+注释）。
论文很长，肯定不能逐字翻，我主要关心的是第三章，但是直接跳过前边又不行，所以先简单节选些第二章的内容。
听说了一个有趣的结论：两个随机的正整数互质的概率为 $\frac{6}{\pi ^2}$，对它的推导过程感到好奇，于是通过wikipedia学习了一些数学知识…
何为“两个随机正整数”？正整数集合的度是无穷大，所以要使得所有整数对出现的概率相同是无法达到的。
问题需要如此描述：我们用 $Z_2(t)$ 表示互质整数对的个数，其中每个整数对中的两个整数都不大于t，于是所要求的概率即为 $limit_{t \to \infty} \frac{Z_2(t)}{t ^2} $。
我们忽略这个定义，直接考虑无穷的情形，两个整数互质，说明对任意的质数p，它们不能同时被p整除；一个随机正整数被p整除的概率为$1/p$，于是它们不同时被p整除的概率为$1-1/p ^2$，对于不同的质数p，相互独立；于是所求即为：
$$
\prod\limits_{prime\ p} (1-1/p ^2)\tag{1}\label{eq1}
$$.
之前挖下的坑还没有填完，但在此之前，由于各种原因，我决定先写些有关拜占庭将军问题的东西。
拜占庭将军问题是可信计算中的一个非常经典的问题，这个名称我估计是源于Lamport对古罗马的莫名情愫。关于历史的问题，我不懂就不逼逼了。
拜占庭军队有许多分支，驻扎在敌人城外，每一分支由各自的将军指挥。将军们只能靠通讯员进行通讯。在观察了敌人以后，忠诚的将军们必须制订一个统一的行动计划。然而，这些将军中有叛徒。叛徒试图扰乱计划的制定。
因此，能够解决该问题的正确算法必须保证如下两点：
最近写的尽是些有的没的，完全没有干货。怎么说，最近考虑在思考人生，价值观在改变，简而言之就是又退化到科学>>技术的中二阶段。一方面看到现阶段所谓“技术产物”的各种各样的问题，另一方面由于自身智力，能力，精力的限制，没有办法对其进行改进和提升，只能采取粗暴的、眼不见为净的鸵鸟政策。其实我知道自己是躲不掉的（当然我说的是找工作），但是还是想在不得不面对之前关心些别的，或者说补救些别的，能补多少是多少吧。年轻的时候有大把时间，却不想念书，现在老了，想念书了，却没有多少时间了（有时间也架不住嗜睡）。
Anyway, 我接下来准备翻译大段的关于无类型lambda-calculus中Church-Rosser定理的证明，为什么要做这么无聊的事情？因为我觉得有趣…为什么不先完善下之前对STLC的证明？1.不求甚解是我的一贯毛（feng）病（ge）；2.这个定理在它的证明中会有一丢丢的作用，Normalization证明的补充会在之后进行。
十多天前我在software fundation的练习中过了一遍有关STLC的weak normalization性质的证明。
当时有些任务心态，想着把上面留的坑填完就完事了，好多大段的引理证明不仅没仔细看，也没有细想引理的用处。
前几天无意中翻到了王垠的一篇老文，于是试图回忆这个定理的证明过程，却发现脑中是空白的，无奈翻出之前的形式化证明从头屡一屡。
由于我的表述能力的限制，以及我对此证明本质的粗浅认识，这将很难成为一篇好的科普文。另外此文只涉及到关于此性质的核心证明(very informal)，其中可能涉及到许多前文已经证明过的引理，如果想了解完整的证明，请参照software fundation或相关文献。
放假闲的慌，于是开始折腾些有的没的，忘记是怎么看到这个repo的了…觉得很好玩的样子，就打算试试看。但是折腾的过程中发现，要让这个插件跟我原有的配置共洽，稍稍有点费劲，于是在此记录下我的无聊行径。
一开始发现它和zsh-syntax-highlighting闹矛盾，翻了下github的issue，发现有两个branch解决了这个问题，分别是pu和thb，没搞懂名字怎么来的…
pu比thb多了自动纠正，其实我对自动纠正挺反感的，无奈的是thb有些其它的bug，比如在按下tab补全路径的时候会多一个/，总之就是我选择了pu这个分支。