这篇文字的起因是《The Little Prover》中提到了偏函数，好奇心驱使探究了一番。
偏函数即 partial function，在计算机领域，它常常和柯里化相关的 partial application 混淆。这里谈的不是 partial application，而是更为神秘诡异的 partial function。
1. 背景，诡异的偏函数
1.1. total function
前阵子看有关定理证明的一本书，《The Little Prover》，其中提到证明一个函数时，需要确保该函数是 total function。所谓 total function 是指对于任何输入，函数都会返回一个值。
有定理 if-same 如下：
(equal? (if x y y) y)意思是说，(if x y y) 其中无论 x 为何，最终的结果都为 y。例如，如果 (equal? y z) 成立，那么 (equal? (if x y y) z) 也成立，反之亦然。
下面这个表达式中的 list0? 函数判断参数 x 是否是长度为 0 的 list。
(equal?
(if (list0? (x)) #f #f)
#f)将定理 if-same 应用到这个表达式，结果恒为真，#f 等于 #f，无论参数 x 为何值。当然前提是 list0? 是 total function。
一个函数是 total function 的条件是，其内部所有子函数是 total 的。
(define list0? (x)
(equal? x '()))list0? 判断参数 x 是否是空列表，其内部调用了 equal? 函数，只要 eqaul? 是 total 的（所有内部方法如都是 total 的），那么 list0? 就是 total 的。
1.2. partial function
如果函数不是 total 的会发生什么呢？ 非 total 的函数称为 partial function，即偏函数。
既然是 total function 的反面，可知它并不是对所有的输入，都会返回一个结果。
(define part (x)
(if (part x) #f #t))这个 part 函数就是一个 partial function，如果调用 part(0)，它将无休止地一直运行下去，不会返回任何结果。
把 part 函数应用到定理 if-same 中:
(equal?
(if (part (x)) #f #f)
#f)第一个 #f 处于 (part x) 为真的条件下，将其替换为 (if (part x) #f #t)，第二个 #f 处于 (part x) 为假的条件下，将其替换为 (if (part x) #t #f)。
(equal?
(if (part (x))
(if (part x)
#f
#t)
(if (part x)
#t
#f))
#f)在根据 part 的定义替换内层的两个 (part x)
(equal?
(if (part (x))
(if (if (part x) #f #t)
#f
#t)
(if (if (part x) #f #t)
#t
#f))
#f)此时内层的第一个 (part x) 为真，第二个 (part x) 为假，化简得到：
(equal?
(if (part (x))
(if #f #f #t)
(if #t #t #f))
#f)进一步简化：
(equal?
(if (part (x)) #t #t)
#f)根据定理 if-same，最后得到 true 等于 false。
(equal? #t #f)通过对 partial function 应用定理证明，最终得到了 true 等于 false 的错误结论。
1.3. measure function
了解了 partial function 的诡异之处，那该如何判断一个函数是 total 的还是 partial 的呢。
partial function 都是可能发生无限循环的函数，像之前的 part 函数。
下面的 list? 是一个递归函数，它判断参数 x 是否是一个 list。它是否是 total 的？
(define list? (x)
(if (atom? x)
(equal? x '())
(list? (cdr x))))《The Little Prover》引入了 measure function 来判断函数是否是 total 的。measure function 的大致思路是，判断函数是否朝着其终止的方向收敛。
比如函数 list?，当参数 x 为空时程序终止运行函数返回，而且函数每次递归时都会减小参数 x 的长度。所以最后一定会终止，它必定是 total 的。
(if (natp (size x))
(if (atom x)
#t
(< (size (cdr x)) (size x)))
#f)这是 list? 对应的 measure function，其中 natp 用于保证 (size x) 一定是自然数，这个函数恒为真，list? 一定是 total 的。
2. 判断无限循环
2.1. lambda 解释器中的循环判断
以前实现的一个 lambda 演算解释器 lambda-interp，其中 reduce 函数负责规约一个表达式，直到最简形式。
表达式 (%x.x) (%y.y) 规约后为 (%y.y)。有些表达式会无休止地规约，例如 (%x.x x) (%y.y y)。
为了防止无限规约这些表达式时出现栈溢出，在 reduce 函数中判断了调用次数，如果大于 1000，说明当前表达式可能是一个无限循环无法规约的表达式。
public Expr reduce(Expr expr, Env env, int count) {
if (count == 1000) {
throw new UnlimitedReduceException("Maybe the expr can not be reduced");
}
}这种方式虽然简单，但对于一些非常复杂（所需规约次数超过 1000 次）的表达式，会造成误判，本来是一个普通表达式，却被当成无限循环的表达式处理了。
受 measure function 的启发，lambda-interp 完全可以在运行时判 reduce 是否是无限循环。
lambda-interp 的工作方式是，解释器将需要化简的 lambda 表达式作为输入参数传递给 reduce 函数，reduce 函数对输入表达式进行一次规约后将结果返回。如果规约后的表达式还不是最简形式，那么将结果再传递给 reduce 函数，直到得到的结果不能再继续规约。
表达式 ((%x.(%y.(x y)) (%z.z)) (%x.x)) 会经过三次规约，最终化简为 (%z.z)：
reduce ((%x.(%y.(x y)) (%z.z)) (%x.x)) -> ((%y.((%x.x) y)) (%z.z))
reduce ((%y.((%x.x) y)) (%z.z)) -> ((%x.x) (%z.z))
reduce ((%x.x) (%z.z)) -> (%z.z)设所有 lambda 表达式的集合为 Q，集合内元素（即任意 lambda 表达式）用 \(x_i\) 表示，reduce 函数的含义为将集合 Q 内元素映射到其自身。对于初始值 \(x_0\)，有如下序列：
\(x_0\), \(x_1\) = reduce(\(x_0\)), \(x_2\) = reduce(\(x_1\)), …, \(x_i\) = reduce(\(x_{i-1}\))
如果存在无限循环，则一定有 \(x_{i+n}\) = \(x_i\) 发生。也就是说，当 reduce 进行规约时，输入和之前的某一个输入一样，之后必定会如此无限循环下去。
比如下面这个例子：
reduce ((%x.(%y.(x y)) (((%y.y y) (%y.y y)))) (%x.x)) -> ((%y.((%x.x) y)) (((%y.y y) (%y.y y)))) // x1
reduce ((%y.((%x.x) y)) (((%y.y y) (%y.y y)))) -> ((%x.x) (((%y.y y) (%y.y y)))) // x2
reduce ((%x.x) (((%y.y y) (%y.y y)))) -> (((%y.y y) (%y.y y))) // x3
reduce (((%y.y y) (%y.y y))) -> (((%y.y y) (%y.y y))) // x4
reduce (((%y.y y) (%y.y y))) -> (((%y.y y) (%y.y y))) // x5
reduce (((%y.y y) (%y.y y))) -> (((%y.y y) (%y.y y))) // x6这个例子从 \(x_0\) 为 ((%x.(%y.(x y)) (((%y.y y) (%y.y y)))) (%x.x)) 开始，到 \(x_4\) 时，出现了 \(x_4\) = \(x_3\) 时，说明发生了无限循环。
在实现上，只要在解释器中保存之前调用 reduce 的输入，将当前输入和之前的比较，如果已经存在则可以判定发生了无限循环。
理论上，这个推论成立的条件是『集合 Q 是有限的』。如果 Q 是一个无限集合，则可能会出现这种情况，reduce 无休止地运行，表达式一直没有规约到最简形式，同时也不会出现 \(x_{i+n}\) = \(x_i\)。
lambda 表达式的集合并不有限的，但 reduce 函数会将 lambda 表达式朝着收敛的方向进行，所以不会出现上述问题。其实我也不确定 lambda 是否会随着规约而不断收敛，只是没有想到反例。有没有可能一个简单表达式越规约越复杂？如果知道的朋友请一定留言告知，万分感谢（特地装了个评论插件 ^_^）。
2.2. 通用程序中的循环判断
既然这个方法可以用于 reduce 函数中，那能不能应用在通用程序语言中呢。答案当然是否定的，不然就解决了停机问题，数学证明总是如磐石般坚固。但这里还是试着讨论一下，对于运行时的无限循环检测，究竟能做到什么程度。
2.2.1. 引用透明
和 lambda 演算解释器相比，通用程序情况会复杂一些。
一个区别在于引用透明。之前判断是否存在 \(x_{i+n}\) = \(x_i\) 时，前提是 reduce 函数是没有副作用的，即相同的输入一定会得到相同的输出。通用程序中很多时候不具备引用透明的特性。
let f = 0;
function foo(x) {
f += 1;
return (x + f) % 10;
}
function bar() {
let x = 1;
while (true) {
const out = foo(x);
console.log(`foo(${x}) -> ${out}`);
x = out;
if (x == 9) {
break;
}
}
}
bar();这段 JavaScript 代码中的 foo 函数依赖外部变量 f，即使输入相同，输出也可能不一样。执行 bar 函数后程序打印输出后正常终止，不会陷入无限循环。
foo(1) -> 2 // x1
foo(2) -> 4 // x2
foo(4) -> 7 // x3
foo(7) -> 1 // x4
foo(1) -> 6 // x5
foo(6) -> 2 // x6
foo(2) -> 9 // x7使用之前的判断方法会发现，foo 执行到第七次就出现了 \(x_6\) = \(x_1\) 的情况，实际上并没有无限循环发生。
不过这也还不足以说明之前方法在通用程序中无效。再看一下之前的序列：
\(x_0\), \(x_1\) = foo(\(x_0\)), \(x_2\) = foo(\(x_1\)), …, \(x_i\) = foo(\(x_{i-1}\))
如果函数 foo 没有任何副作用，那么若存在无限循环，则一定有 foo(\(x_{i+n}\)) = \(x_i\) 发生。可惜 foo 函数引用了自由变量 f，造成相同的输入得到不同的输出。但我们不仅可以记录 foo 的输入参数 x，还可以将自由变量 f 的值也记录下来。最终这个序列是这样的：
\(x_0\), \(x_1\) = foo(\(x_0\), f), \(x_2\) = foo(\(x_1\), f), …, \(x_i\) = foo(\(x_{i-1}\), f)
发生无限循环的条件变为 foo(\(x_{i+n}\), f) = \(x_i\)。
foo(1, 1) -> 2 // x1
foo(2, 2) -> 4 // x2
foo(4, 3) -> 7 // x3
foo(7, 4) -> 1 // x4
foo(1, 5) -> 6 // x5
foo(6, 6) -> 2 // x6
foo(2, 7) -> 9 // x7以新的条件再来考查之前的序列，就没有检测到无限循环了。
这只是一个小例子，仅仅包含了一个自由变量 f，实际的情况可能会非常复杂。按照这个思路，实现上可以在每一步后保存整个运行时的快照，包括全局变量以及堆栈的所有状态，如果快照和之前的某一个快照一致，则表示发生了无限循环。
当然，这个方案成本太高。但如果所有输入（运行时状态）的集合是有限的，理论上（不考虑资源限制）它确实可以检测到无限循环发生。
2.2.2. 逐渐收敛
计算机程序处理的数据大多是一个无穷集合，这个序列可以无限展开永不重复。
\(x_0\), \(x_1\) = foo(\(x_0\)), \(x_2\) = foo(\(x_1\)), …, \(x_i\) = foo(\(x_{i-1}\)), …, foo(\(x_\infty\))
这段程序会一直运行不会终止，且永远不会出现 foo(\(x_{i+n}\)) = \(x_i\)。严格来讲，这已经不算是无限『循环』了，因为没有出现如 \(x_{i+n}\) = \(x_i\) 这样周而复始的过程。为了叙述上的方便，将这种情况也称作无限循环。
function foo(x) {
return x + 1;
}
function bar() {
let x = 1;
while (true) {
const out = foo(x);
console.log(`foo(${x}) -> ${out}`);
x = out;
}
}
bar();这个问题看上去依然是可以修复的，方法就是引入 measure function 的思路，判断函数是否存在终止条件，并且朝着终止条件收敛。
再考虑另一种情况，下面这段 Haskell 代码定义了一个 double 函数，接受一个列表，将列表里的每一个元素都乘以 2，最后返回一个新列表。
double x = case x of
[] -> []
(d:ds) -> (d * 2):double ds单从函数体看，其终止条件是列表为空，且每一次递归都是向着（tail x）终止条件收敛的，看起来它不会发生无限循环。
double [] -- []
double [1, 2, 3, 4, 5] -- [2,4,6,8,10]然而事实并非如此，这也是使用 Haskell 来写这段函数的原因。如果传递给它一个无穷列表，它会永无休止地一直运行。
double [1..] -- endless running收敛仅仅保证了当参数为有限数据时，其会逐渐收缩，直到终止条件。但当参数本身就是无限集合时，收敛是没有作用的，一个无限集合再怎么收敛也依然是无限的。
2.2.3. 不确定的条件
如果程序存在终止条件，但不是逐渐收敛的，程序会不会终止呢。
findX 函数是一个寻找列表中是否包含元素 42 的函数，找到立即返回，否则继续寻找直到列表为空。程序终止的条件在于参数列表中是否包含 42。
findX [] = Nothing
findX (d:ds) = if d == 42
then Just d
else findX ds这个例子实在是难以判断程序是否会无限循环，如果 42 出现在无限列表的开头，程序立即终止，如果不存在，则一直运行下去。
findX [1..] -- 返回 Just 42
findX [43..] -- endless running也不排除解释器已经聪明到了可以判断参数中是否包含 42，从而知道程序是否会终止。确实，当输入为 [1..]，这是一个从 1 开始递增的无限列表，它其中一定包含了 42。而 [43..] 是一个从 43 开始的无限列表，其中没有 42，这个参数必定会导致程序无限循环。也许解释器真的能够办。
但如果逻辑再复杂一点呢。
function collatz(n) {
while(n > 1)
n = (n % 2 === 0) && (n / 2) || (n * 3 + 1);
}collatz 函数接受一个正整数参数 n，如果是奇数，则对其乘以 3 再加 1；偶数则对其除以 2。直到 n 等于 1 时终止，否则一直进行下去。collatz 函数对于大于 1 的任意 n，它总是会终止吗？
答案是不知道，这个被成为考拉兹猜想的预言说，是任意正整数，如果它是奇数，则对它乘 3 再加 1，偶数则对它除以 2，如此循环，最终都能够得到 1。但是否对任意正整数都成立，至今未知。
显然解释器还远没有聪明到能够预知 collatz 是否会无限循环，但也没有数学上直接的证明（也许有？）证明它不行，所以才有了那个简洁但很不直接的停机问题反证法。
3. 偏函数何以如此诡异
3.1. 停机问题的反证法
关于停机问题最著名的证明方法，都不会陌生。我最初看到这个证明时，一直耿耿于怀，虽然反证法确实证明了不存在一个通用的判定方法，但究竟为什么不存在，问题出在哪里呢？反证法并没有告诉我们。
把这个证明用代码写出来，可以发现这也是一个关于 partial function 的问题。
function runForever() {
while (true) {
}
}
function foo() {
return willStop(foo) && runForever();
}
console.log(willStop(foo));假设通用判定方法（willStop）是存在的，使用它判断一下 foo 函数是否会终止，结果如何呢。分析一下就会发现矛盾，willStop 无非返回 true 和 false。
-
如果 foo 函数定义中的 willStop(foo) 返回 true，则进入 run_forever 函数，foo 将一直运行不停机。console.log 中的 willStop(foo) 将返回 false，与刚刚的假设矛盾
-
如果 foo 函数定义中的 willStop(foo) 返回 false，foo 函数直接返回。console.log 中的 willStop(foo) 将返回 true，又与刚刚的假设矛盾
可见如果 willStop 存在，它会导致矛盾，所以通用判定方法是不存在。出现矛盾的原因在于 foo 函数，这是一个递归函数，并且是 partial function。
3.1.1. 递归函数的本质
递归函数是一个可以引用自身（自指）的函数。下面是一个计算阶乘的递归函数。
function factorial(n) {
if (n == 0) {
return 1;
} else {
return n * factorial(n - 1);
}
}要弄清递归函数，可以看看如果不使用递归应该怎么实现阶乘。既然不能引用自身，让它暂时抛一个异常。
function unreachable(x) {
throw "unreachable function";
}
let factorial = function (n) {
if (n == 0) {
return 1;
} else {
return n * unreachable(n - 1);
}
};
console.log(factorial(0)); // 1
console.log(factorial(1)); // exception "unreachable function"这个缺乏递归的 factorial 其实是可以工作的，只不过它只能计算 0 的阶乘。如果把 factorial 的定义复制一下，它就能计算 1 的阶乘。
let factorial = function (n) {
if (n == 0) {
return 1;
} else {
return n * function (n) {
if (n == 0) {
return 1;
} else {
return n * unreachable(n - 1);
}
}(n - 1);
}
};
console.log(factorial(0)); // 1
console.log(factorial(1)); // 1
console.log(factorial(2)); // exception "unreachable function"照这个方法，factorial 可以计算更多的阶乘（简洁起见，抽象了公共代码）。
let factorial = function(f) {
return f(f(f(f(f(f(f(f(f(f(f(unreachable)))))))))));
}(
function(f) {
return function (n) {
if (n == 0) {
return 1;
} else {
return n * f(n - 1);
}
};
}
);
console.log(factorial(0)); // 1
console.log(factorial(1)); // 1
console.log(factorial(2)); // 2
...
console.log(factorial(10)); // 3628800
console.log(factorial(11)); // exception "unreachable function"问题是，我们不知道要处理的数据究竟有多大多长，不可能事先定义好方法。所以我们需要递归函数，来处理那些（理论上）无穷无尽的数据。
递归意味着无穷。
3.1.2. 暧昧的层次
停机问题表面上没有涉及无限集合，但它包含了自指，如果存在通用方法可以判定一段程序是否停机，这个方法本身也是一段程序，它也可以被方法判定。由此产生了无穷集合和嵌套的层次关系。
停机问题那段代码，其中的 foo 是一个递归函数，我们按照改写 factorial 函数一样改写 foo 函数：
function unreachable() {
throw "unreachable function";
}
function foo() { // foo0
return willStop(
function(){ // foo1
return willStop(
function(){ // foo2
return willStop(
function(){ // foo3
return willStop(
...
function(){ // foon
return willStop(
function(){
return willStop(unreachable) && runForever(); // never reach
}
) && runForever();
}
...
) && runForever();
}
) && runForever();
}
) && runForever();
}
) && runForever();
}
console.log(willStop(foo));其中的 unreachable 函数并不会被调用，写在这里相当一个占位符，在它之前嵌套了无限个匿名方法 function(){return willStop(...) && runForever();} 。这个匿名方法其实就是 foo 函数本身，为了方便描述，我们给它编上号，foo\(_0\)、foo\(_1\)、foo\(_2\)、foo\(_3\)、一直到 foo\(_n\)，其中 foo\(_0\) 是最顶层的 foo 函数，n 趋近无穷。
在改写后的代码的基础上，我们想象一下 willStop(foo\(_0\))（即 console.log 中的 willStop(foo)）的执行过程。当 willStop 看到 foo\(_0\)，这是一个无限嵌套的函数。foo\(_0\) 是否停机，取决于 willStop(foo\(_1\)) 的结果，即 foo\(_1\) 是否停机。而 foo\(_1\) 是否停机又取决于 foo\(_2\) 是否停机，foo\(_n\) 是否停机又取决于 foo\(_{n+1}\) 是否停机，这样无限地依赖下去。
有了这个模型，再回看一下之前反证法的两个假设：
1)，『如果 foo 函数定义中的 willStop(foo) 返回 true，则进入 run_forever 函数，foo 将一直运行不停机。console.log 中的 willStop(foo) 将返回 false，与刚刚的假设矛盾』
当我们用自然语言说『如果 willStop(foo) 返回 true』时，这里的 foo 是可以指任意一个 foo\(_n\) 的，我们假设是 foo\(_3\)。如果 willStop(foo\(_3\)) 返回 true，也就是 foo\(_3\) 会停机。忽略 foo\(_3\) 的内部实现，代码简化成这样：
function foo() { // foo0
return willStop(
function(){ // foo1
return willStop(
function(){ // foo2
return willStop(foo3) && runForever();
}
) && runForever();
}
) && runForever();
}foo\(_3\) 会停机，相应地，foo\(_2\) 不会停机，foo\(_1\) 会停机，foo\(_0\) 不会停机。
2)，『如果 foo 函数定义中的 willStop(foo) 返回 false，foo 函数直接返回。console.log 中的 willStop(foo) 将返回 true，又与刚刚的假设矛盾』
用同样的思路来处理这个假设：foo\(_3\) 不会停机，那么 foo\(_2\) 会停机，foo\(_1\) 不会停机，foo\(_0\) 最终会停机。
到这里应该比较明显了，问题在于讨论对象的层次是不明确的。foo\(_0\)、foo\(_1\)、foo\(_2\)、foo\(_n\) 其实只是我们为了方便描述取的一个编号，他们其实都是 foo 函数。在每次假设中，我们两次提到了 foo 函数，其实它们分别指的是不同层次的东西。
3.2. 罗素悖论的目的
和停机问题类似的另一个问题，罗素悖论。它有一个等价且更通俗的表述，理发师悖论：有一位理发师，它立下一个规则，他只为且一定要为城里所有不为自己理发的人理发。——那么问，他要不要给自己理发？
要知道罗素提出这个悖论是 1901 年，很难想象如果他提出这个悖论是为了说明逻辑也有无能为力的时候（就像停机问题的通用解法不存在），那为什么之后还会花近十年来写《数学原理》呢。
其实罗素不是以此说明逻辑不行，而为了指出集合论的问题。罗素悖论的原始形式这样的：定义集合 S，它是所有不是自身子集的集合的集合。——那么请问，集合 S 是否已属于自己？听起来有点绕，但它和理发师悖论含义是一样的，都具有自己包含自己（自指）的特点。关于集合的论断，必须区分『集合』、『集合的集合』、以及『集合的集合的集合』等等，至于自指这一特点，则应该彻底踢出集合论。
这也就是上面说的层次问题。如果将罗素悖论写成代码，会发现它也是一个 partial function，使用和 willStop(foo) 同样的方式改写函数，可以看出它所指的层次同样是不明确的。
3.3. true 等于 false
开头对 part 函数应用定理之后得到 true 等于 false，也是混淆了层次的关系。
我们在 (part x) 为真的情况下，将 #f 替换为了 (if (part x) #f #t)，然后又根据 (part x) 的定义，进一步地变为 (if (if (part x) #f #t) #f #t)。
由于替换后的整个结果都处于 (part x) 为真的条件下，所以 (if (if (part x) #f #t) #f #t) 中的 (part x) 理应也为真，问题就此产生了。因为内层的 (part x) 和外层的 (part x) 并不是一个层次的东西，我们仅仅因为长得一样而混淆了。
套用停机问题中对于判定方法是否存在的问法，我们也可以问：根据 part 函数的定义，(part x) 究竟是真还是假呢？
(define part (x)
(if (part x) #f #t))结果就是，它即为真又为假。和真实世界中的判定方法不同，part 函数已经写出来了，我们实在没法说它不存在。
4. 偏函数一定是无限循环？
参考维基百科，partial function 在数学上的定义是，对于函数 f(x)，x 仅在部分定义域中才使得 f(x) 成立。
『In mathematics, a partial function from X to Y is a function f: X′ → Y, for some subset X′ of X.』
这样的函数其实很常见，比如 f(x) = \({\frac{1}x}\)，其中的 x 就不能为 0，我们称 f(x) 在 x = 0 时没有意义。那为什么数学中的『没有意义』到了程序语言就成了无限循环了呢。
数学是一个理想模型，『没有意义』是指，函数在某些定义域内不存在取值，我们完全可以不用讨论它。而程序是不能限制输入的，当定义了一个除法函数 onediv(x) = 1 / x，显然 x 不能 0，但谁也不能阻止我们将 0 传给 onediv 函数。
根据定义，onediv 在数学上是一个 partial function，但是它在程序语言中仍然是 partial 的吗？
答案取决于程序语言中是否容忍异常，这个问题并没有准确答案，在大多数语言中，onediv(0) 会抛出一个除零异常，而异常（exception）也算是一个返回值。在 python 中调用 onediv(0) 后得到了一个 ZeroDivisionError 异常，好比 make_ex 函数构造一个异常然后返回，很难说它是一个 partial function。
def make_ex(name):
return NameError(name)在更接近数学模型的 Haskell 中，onediv 则是一个 partial function。在 Haskell 中，任何会产生 error，以及无限循环的函数都是 partial function。
（完）
参考链接：