作者 Ivan Chien
始于 
分类：PL
Tags: [ PL ]
程序语言理论和实现 Week 2

λ Calculus

Tiny Language 3

增加了函数（function）和函数应用（apply）：

type rec expr =
  ...
  | Fn (list<string>, expr)
  | App (expr, list<expr>)

函数里列表是形式参数（formal parameters），应用里的列表是实际参数（actual arguments）。

type rec value =
    | Vint (int)
    | Vclosure (env, list<string>, expr)

let rec eval = (expr : expr, env : env) : value => {
    switch expr {
        ...
        | App(e, es) => {
            let Vclosure(env_closure, xs, body) = eval(e, env) // 求函数本身
            let vs = map(es, e => eval(e, env)) // 求参数列表
            let fun_env = concatMany([zip (xs, vs), env_closure]) // 将参数与闭包环境拼接
            eval(body, fun_env)
        }
    }
}

Tiny Language 4

将 Tiny Language 3 lower 到 nameless style 的版本。

比如对 \x -> x + 1 可以 lower 成 fn (Var[0] + 1) 的样子，或者 \x y -> x + y 可以 lower 成 fn (Var[0] + Var[1]) 的样子。

Simplification to Lambda Calculus

Let(x, e1, e2) 和 App(Fn(x, e2), e1) 在理论上是等价的，但是实际上后者效率会较低。

Cst i 可以用 Church numerals 表示。Bool 也有对应的等价表示。

Fn(x1, x2, e) 这种多参数的函数可以柯里化成 Fn(x1, Fn(x2, e))，类似的 App(e, e1, e2) 变为了 App(App(e, e1), e2)。

这样可以得到一个更简单的 AST，把它称为 lambda：

type rec lambda =
    | Var (string)          // 变量名
    | Fn (string, lambda)   // 单参数函数
    | App (lambda, lambda)  // 单参数应用

相关计算就是 lambda calculus。

Formally

Terms:

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

这样的一个语言是与图灵机等价的，也就是图灵完备的（Turing complete），即和任何（图灵完备的）编程语言的表达能力都相同。

因为 lambda calculus 很简单，所以更便于在它上面做一些形式化的推导。

$\lambda$ Calculus

$\beta$-reduction

Confluence of Untyped Lambda Caculus

Church-Rosser theorem：使用不同的归约路径最终都能得到一样的结果。

Interpreter, Natural Semantics

Evaluate closed term, called by value. Closed term 让我们不考虑 \x -> y 这种情况，就是这个变量 y 是没有绑定的；同时像 App(a, b) 这样的应用，如果是 a 不为 function 的 bad state 也不在我们的考虑范围内。就有下面的定义：

let rec eval = (t : lambda) => {
    switch t {
    | Var(_) => assert false  // bottom, unbound value
    | Fn(_, _) => t
    | App(f, arg) => {
            let Fn(x, body) = eval(f)
            let va = eval(arg)
            eval(subst(x, va, body))  // substitution, body[va/x]
        }
    }
}

Primitives

Booleans

Church Pair

Church Numerals

$\bar{n} = \lambda f x. f^n(x)$

Isomorphism in ReScript (Peano numbers):

type rec nat = Z | S (nat)
let three = S (S (S Z))

compare with the Church numeral: $\bar{3} = \lambda f x. f (f (f\ x))$

Arithmetic Functions

Infinite Reduction

$\omega = \lambda x. xx$
$\Omega = \omega \omega$

这个 $\Omega$ 就可以无限归约下去，即 lambda calculus 可以构造出无限循环，也就是说图灵机也可以无限循环。

Y combinator

$Y = \lambda f. (\lambda x. f(xx)) (\lambda x. f(xx))$

这样就有 $Y F = F (Y F)$。这里的 $Y F$ 也被叫作 $F$ 的一个不动点（fixed-point）。

于是这样可以定义 Church numerals 的乘法：

$(\times) = Y\ F$

$F = \lambda f n m. $ if ( $n = 0$ ) then 0 else $(m + f\ (n - 1) m)$

这样就可以通过对 F 的第一个参数 f 的调用去除对 F 的递归。因为 $Y F = F (Y F)$，所以就有了：

$(\times) = \lambda n m. $ if (n = 0) then 0 else $(m + (n - 1) \times m)$

Untying the Knot

比如 fib 函数的递归定义：

let rec fib = n => {
    switch n {
    | 0 | 1 => 1
    | _ => fib (n - 1) + fib (n - 2)
    }
}

使用 rec 关键字可以 tying the knot，即将递归调用的 fib 绑定到定义的这个 fib 上，这个关键字所表示的语义是一种 fixed recursion。

相对的有 open recursion：

let myfib = (myfib, n) => {
    switch n {
    | 0 | 1 => 1
    | _ => myfib (n - 1) + myfib (n - 2)
    }
}

这样的写法其实不包括真正的递归。

我们使用 Y 组合子将 myfib 直接变成与 fib 等价的函数，但同样的我们可以在这个 Y 组合子上做点手脚，比如加上缓存功能：

// 这里的 memo 就是魔改过的 Y combinator
let memo = anyFunc => {
    let cache = Hashtbl.create(100)
    let rec fix = (n) => {
        switch Hashtbl.find_opt(cache, n) {
        | Some(x) => x
        | None => {
                let x = anyFunc(fix, n)
                Hashtbl.replace(cache, n, x)
                x
            }
        }
    }
    fix
}

let memofib = memo(myfib)

HW

-- Implement the substitution function N[v/x]:
-- subst (N: lambda, x: string, v: value) : lambda

data Lambda
    = Var String
    | Fun String Lambda
    | App Lambda Lambda
    deriving Show

churchTrue = Fun "x" (Fun "y" (Var "x"))
churchFalse = Fun "x" (Fun "y" (Var "y"))
ifThenElse = Fun "x" $ Var "x"

subst :: String -> Lambda -> Lambda -> Lambda
subst x va body@(Var name) = if name == x then va else body
subst x va body@(Fun funParam funBody) = if funParam == x then body else Fun x (subst x va funBody)
subst x va body@(App fun argument) = App (subst x va fun) $ subst x va argument

eval :: Lambda -> Lambda
eval v@(Var _) = v
eval t@(Fun _ _) = t
eval (App f arg) = eval $ subst x va body
    where (Fun x body) = eval f
          va = eval arg

test = eval (App (App (App ifThenElse churchTrue) churchFalse) churchTrue)

main :: IO ()
main = print test