Termination check (foetus & size-change)

about posts categories aya
9/10/2022 dependent-types

停机问题是一种不可判定 (undecidable) 问题。即不存在一个函数 P(x)P(x) 对任意输入的程序 xx 都能判断其是否停机。 证明：假设存在这样的函数 P:X→BoolP : X \rightarrow Bool 则下面的程序存在矛盾：

int oops() {
  if (P(oops)) 
    return oops();  // does not terminate but P(oops) is true!
  else 
    return 114514;  // terminates but P(oops) is false!
}

题外话：根据饭饭定理 (Rice's Theorem)，程序的任何非平凡性质 (non-trivial semantic property) 都是不可判定的。 例如：程序是否内存泄漏，程序是否会死锁等等，都可以通过上面的方式构造出悖论或者直接证明该定理。

# Structural recursion

我们仍然可以通过引入结构递归 (structural recursion) 来判断一部分程序的停机问题。 它的思想是：如果一个程序的所有可能的执行路径都会停机，那么这个程序就会停机。

这个思想很重要，这引导我们定义「一条执行路径怎样停机」：每次直接或者间接递归调用函数自身时，总有至少一个参数严格减小 (strictly decrease)。

用一个例子来展示什么是严格减小，在下面的程序中：

factorial : Nat -> Nat
factorial 0 = 1
factorial n = n * factorial (n - 1)
--        ^ (1)   ^^^^^^^^^^^^^^^^^ (2)

factorial 一个典型的递归函数，用于计算一个数的阶乘。这里存在一次递归调用，即使用 (2) 标记的地方， 该递归调用传入的参数是 n - 1，该参数相比本次调用时提供的参数 n 即使用 (1) 标记的地方，严格减小了。

但是上面的例子并不够好，因为自然数类型 Nat 的更一般定义为:

data Nat : Set where
  | zero : Nat
  | suc  : Nat -> Nat

这是一种归纳数据类型 (inductive data types)，其含义是：

  • zero 是一个自然数，即 00
  • 如果 n 是一个自然数，那么 suc n 作为 n 的后继 (successor)，也是一个自然数

阶乘函数是对归纳数据类型的递归函数，自然地该函数应该对其参数进行归纳:

factorial : Nat -> Nat
factorial zero    = 1
factorial (suc n) = suc n * factorial n

不难发现，递归调用时使用的参数 n，相比本次调用时提供的参数 suc n，在归纳结构上，确实严格减小。

# The foetus checker

Andreas Abel 等人在 2002 年提出了一种基于结构递归的停机检查算法，该算法定义了如下结构:

  • Relation：两个参数之间的关系，即上面定义的 <\lt，==， ?? 三种关系
  • Semiring of Relation: 在 Relation 上定义加法、乘法、00 和 11，使 RelationRelation 成为一个半环
  • Call Matrix: 函数 ff 调用函数 gg 时，每个传给 gg 的参数和 ff 自身的参数之间的关系的矩阵
  • Call Graph: 整个程序的调用图，其中每个节点表示一个函数，每条边表示一个函数调用（并使用 Call Matrix 描述调用中的参数关系）

接下来将一一介绍这些构造

# Relation

假设存在两个表达式 aa 和 bb，如果满足下列任何一项，称 aa 严格小于 bb，用符号表示为 a<ba \lt b:

  • aa 可以写成 C(⋯,b,⋯)C(\cdots, b, \cdots) 的形式，其中 CC 是某个构造器 (constructor)，bb 是其中的一个参数
  • aa 可以写成 b.xb.x 的形式，其中 bb 是投影操作的头部，xx 是一个字段 (field) 或者下标 (index)
  • aa 可以写成 bxb\; x 的形式，其中 bb 是函数应用的头部，xx 是一个表达式

假如存在两个表达式 aa 和 bb，如果满足下列任何一项，称 aa 不严格小于 bb，用符号表示为 a=ba = b:

  • aa 可以写成 C(x⃗)C(\vec{x}) 的形式，且 bb 可以写成 C(y⃗)C(\vec{y}) 的形式，其中 x⃗=y⃗\vec{x} = \vec{y}
  • aa 和 bb 都是对变量的引用，且引用的是同一个变量

如果上面的条件都不满足，则 aa 和 bb 的关系不确定，用符号表示为 a?ba \;?\; b。

# Semiring of Relations

可以在 Relation 上定义"加法"、"乘法"、"0" 和 "1"，使 Relation 成为一个半环。

这是为了在后续的操作中，关系之间可以进行合并。例如：假设有关系：x<yx \lt y 和 x?yx \; ? \; y， 很自然地根据不同的情况，合并的方式也可以不同：

  • 如果 xx 和 yy 是相关的参数（即 xx 和 yy 是同一个函数的同一个参数），我们希望得到其「更差」的合并
  • 如果 xx 和 yy 是不相关的参数，我们希望得到其「更好」的合并

可以初步定义「更差」和「更好」：

  • 更差：关于参数变化的不确定度增加了。例如：从 <\lt 变化到 == (或者 ??) 属于该类。
  • 更好：关于参数变化的不确定度减小了。例如：从 ?? 变化到 <\lt (或者 ==) 属于该类。

至于相关参数使用「更差」合并，而不相关参数使用「更好」合并，是因为该算法希望通过某些运算， 找到所有递归调用中的最差情况，并以此检查递归是否停机。 其中的思想是：如果最差的递归情况一定会停机，那其他更好的情况也一定会停机。 关于这个思想的具体解释，会在后文该部分中进行详细说明。

自然地，可以将产生「更差」的合并的运算定义为"乘法"，将产生「更好」的合并的运算定义为"加法"：

+<=?<<<<=<==?<=?×<=?<<<?=<=?????\begin{array}{c|ccc} + & \lt & = & ? \\ \hline \lt & \lt & \lt & \lt \\ = & \lt & = & = \\ ? & \lt & = & ? \\ \end{array} \quad\quad\quad\quad \begin{array}{c|ccc} \times & \lt & = & ? \\ \hline \lt & \lt & \lt & ? \\ = & \lt & = & ? \\ ? & ? & ? & ? \\ \end{array}

从上面的表可以看出，"0" 是 ??，"1" 是 "="。

# Call Matrix

// TODO: trivial

# Call Graph

// TODO: trivial

# Completion of Call Graph

// TODO: trivial

# The size-change principle

上面的 foetus 算法并不能处理更复杂的情况。例如 foetus 认为下面两个函数并不停机，但是实际上是停机的：

sum : List Nat -> Nat
sum [] = 0
sum zero    :: xs = sum xs
sum (suc x) :: xs = suc (sum (x :: xs))
--  ^^^^^^^^^^^^^             ^^^^^^^ (1) look here!

add : Nat -> Nat -> Nat
add a zero    = a
add a (suc b) = add b a
--  ^^^^^^^^^       ^^^ (2) look here!

// TODO: finish this part!

# Reference

© Kiva 2019 – 2024