佚名

无类型的Lambda演算

参考资料：The Lambda Calculus Its Syntax and Semantics

Lambda项

  • 关于归纳定义，可参见从不动点定理到编程语言
  • Lambda演算是函数的演算
    • 函数f –> 抽象\lambda x.f(x)
    • 求值f(a) –> 作用(\lambda x.f(x))(a)
    • 函数的变量可以重命名，

          \[ f \rightarrow \lambda x.f(x),\; \lambda y.f(y). \]

    • 函数的求值可以视为替换，

          \[ f(a) \rightarrow (\lambda x.f(x))(a) = f(x)|_{x = a}. \]

    • 在不同的地方，\lambda x.f(x)有不同的形式。在数学中，它可以记为x \mapsto f(x)；在编程语言中，它可以记为fn x => f(x)
  • 上面的演算经过形式化，可以得到无类型的Lambda演算，它可能不符合函数的特点。比如，函数应该作用于变量，但是我们允许变量作用于变量
    • （变量）变量的集合V
    • （抽象）变量x，表达式M –> \lambda x. M
    • （作用）表达式M、N –> MN
  • Lambda项\Lambda，归纳定义
    • （变量）如果x \in V，那么x \in \Lambda
    • （抽象）如果x \in V，M \in \Lambda，那么\lambda x.M \in \Lambda
    • （作用）如果M、N \in \Lambda，那么MN \in \Lambda
  • M的子项Sub(M)，归纳定义
    • （变量）Sub(x) = \{ x \}
    • （抽象）Sub(\lambda x.M) = Sub(M) \cup \{ \lambda x.M \}
    • （作用）Sub(MN) = Sub(M) \cup Sub(N) \cup \{ MN \}
  • M的自由变量FV(M)，归纳定义
    • （变量）FV(x) = \{ x \}
    • （抽象）FV(\lambda x.M) = FV(M) - \{ x \}
    • （作用）FV(MN) = FV(M) \cup FV(N)
    • 也就是说，出现在\lambda后面的变量是绑定变量，不出现在\lambda后面的变量是自由变量。如果FV(M) = \emptyset，即M没有自由变量，那么M称为闭的Lambda项

替换、Alpha转换、Beta规约

  • 在Lambda项M中，将其中的变量x替换为另一个Lambda项N，记为

        \[ M[x := N] \]

    替换的规则，归纳定义
    • （变量）x[x := N] \equiv N，y[x := N] \equiv y（x \not\equiv y）
    • （抽象）(\lambda y.M)[x := N] \equiv \lambda y.(M[x := N])
    • （作用）(M_1M_2)[x := N] \equiv (M_1[x := N])(M_2[x := N])
  • （Alpha转换）将函数的变量x重命名为变量y，这对应于Alpha转换（Alpha Conversion）

        \[ \lambda x.M \equiv_\alpha \lambda y.M[x := y]. \]

    我们需要避免如下的情形，比如
    • （新的绑定旧的）\lambda x.y \not\equiv_\alpha \lambda y(new).y(old)
    • （旧的绑定新的）\lambda x.(\lambda z.(\lambda y.x)) \not\equiv_\alpha \lambda y(new).\lambda z.\lambda y(old).y(new)
    • 也就是说，重名名使用的变量y不能是M的自由变量，也不能是\lambda后面的绑定变量，所以我们必须使用全新的变量，比如

          \[ \lambda x.y \equiv_\alpha \lambda z.y,\; \lambda x.(\lambda z.(\lambda y.x)) \equiv_\alpha \lambda w.\lambda z.\lambda y.w \]

    • 因为\equiv_\alpha是一个等价关系，所以也叫做Alpha等价。以后，我们将Alpha等价的Lambda项视为恒等的，并且将\equiv_\alpha视为\equiv
  • （Beta规约）将函数的求值视为替换，这对应于Beta规约（Beta Reduction）

        \[ (\lambda x.M)(N) = M[x := N]. \]

    除了Beta规约以外，我们还有如下的关系
    • （等价关系）=是一个等价关系
    • （抽象）如果M = N，那么\lambda x.M = \lambda x.N
    • （作用）如果M = N，那么MZ = NZ，ZM = ZN

Church-Rosser定理

  • 根据Beta规约，我们可以对Lambda项进行计算，这类似于函数的化简
  • 然而，Lambda项的计算可能没有结果，或者结果不唯一。Church-Rosser定理用于刻画Lambda项的计算结果