λ-calculus

计算本身并不平凡

α等价：约束变量名字不同
(λ x. f)(a) x: head; f: an expression; a: another expression
只有匿名函数
β-reduction,
β normal form：无法进一步β归约的项

John Trump’s λ diagram

丘奇-图灵命题：丘奇λ函数与图灵机的等价性
反应了面向对象编程和面向函数编程的等价性

$$
\text{True}:=\lambda x y .x,\text{False}:=\lambda xy.y
$$
$$
\text {if} b ~\text{do} ~x\text{else} ~y:=\lambda bxy.bxy
$$

turning’s fix combinator
Θ=λf. (λx. f (x x)) (λx. f (x x))
ΘF=F(ΘF)

Church-Rosser Theorem （合流定理，Confluence Theorem）：如果一个λ项可以通过不同的归约路径到达两个不同的项，那么这两个项最终可以归约到同一个共同项。但有的归约路径可能发散
发散式如 Ω=(λx.xx)(λx.xx) 会无限归约

• 应用序（Applicative Order）：先对函数的所有参数求值，再应用函数。类似于严格求值（如C语言）。可能有自应用，导致无限循环
• 正则序（Normal Order）：先展开函数体（最外，最左），直到无法继续归约时才对参数求值。类似于惰性求值（如Haskell）。by 标准化定理（Standardization Theorem），保证归约到beta范式

eg (λx.y)(Ω)

• 正则序：
  1. 最左最外的redex是 (λx.y)(Ω)。
  2. 归约得到 y（直接得到范式，不计算 Ω）。
• 应用序：
  1. 先归约参数 Ω，导致无限循环，永远无法得到 y。

     def f():
     	return f()+1
     def g(x,y):
     	return y
     g(f(),1)

Type
$$
\lambda b^{\text{boolen}}
$$

Curry-Howard 同构

$$
A\to B~\sim ~A\Rightarrow B
$$