Lambda 演算

Lambda演算学习笔记，

注0：一切名词术语以英语/德语标注为准，中文是我瞎鸡巴翻的。
注1：说“返回一个值”其实不严格, β-规约到最后也不会获得一个真正的“自然数”，因为Lambda calculus 中只有演算，没有数字。自然数由Church Encoding定义，其本质也是λ-Term
注2：汉字入和lambda λ长得太tm像了，所以文中的入我都写成“进”之类的词。

# Terminologies:

变量 Variable 如 x,y,a,b…
符号 Symbol 如 1,2,3,+,-…
参数 Argument. 参数可以是其他的λ项
抽象 abstraction
应用 Application
α变换 α-conversion
β规约 β-reduction / reduktion
组合子 Combinator / Kombinator
绑定变量 BV(Bounded-Var) / GV(Gebondene Var.)
自由变量 FV(Free/Freie Var.)
λ项 λ-Term

# Intro: λ-calculus basics

什么是λ演算？
λ演算(λ-calculus/kalül)是一套研究抽象定义和应用函数的形式系统。

比如以下场景：

1.定义表达式 $x^2+1$
2.如果x=2，那么表达式等于多少？

1 和 2 分别涉及了λ-演算的两个重要部分：抽象定义(abstraction)和函数应用(application)。下面用λ-calculus表述以上的情况:

首先定义 λ-Term (方括号里的内容不是正规的写法，但为了方便理解姑且先这么写)

M = λx.[x^2 + 1]

λ运算符绑定了x，也就是说，这个λ-Term在等待一个参数，获得参数后就将其替换(Substitution)进后面表达式中x对应的位置。λ符号本身没有意义，它只是说"我在等一个input来替换给x"。

Application:
M a 表示: 把λ-Term M 应用到参数a上,并获取一个新的东西（在这里是获取一个值，但它也可以是其他的λ-Term）.

M 2 =  λx.[x^2 + 1] 2
    => 2^2 + 1         (*)
    =  4 + 1
    =  5

β-归约(reduction)
其实上面的(*)就是完成了一次β-规约：读取一个东西，把一个被绑定的变量替换成它。

(λx.M) N => M [x:=N]

M [x:=N] 表示将M中所有的x替换成N。就这么简单，lambda演算的核心就这。

多变量怎么整
例如计算两个参数的和 SUM(x,y) = x + y

SUM = λx.(λy.(+ x y))

λ-Term SUM 每次只读取一个参数，当它读到第一个参数后，返回的不是值，而是一个新的“运算”，这个新的运算进一步读取下一个参数，然后返回结果。

SUM 1 2 =  λx.(λy.(+ x y)) 1 2
        =>    (λy.(+ 1 y)) 2  
        =>    (+ 1 2)

# 正经定义 & 语法

λ-Terms

所有的变量(variable)都是λ-term
如果 M 和 N 都是λ-term, 那么 M N也是λ-term
如果 M 是λ-term, x是变量, 那么 (λx.M) 是λ-term

2定义的λ-term也叫"应用项(application terms)"
3定义的λ-term也叫"抽象项(abstraction terms)"

左结合(left associative)

A B C = ( (A B) C)

绑定变量(BV或GV)与自由变量(FV)

RULE (M,N是λ-term, x是变量)

Rule#	FV	BV
(1)	FV(x)={x}	BV(x) = ø
(2)	FV(M N)=FV(M) ∩ FV(N)	BV(M N)=BV(M) ∩ BV(N)
(3)	FV(λx.M)=FV(M) / {x}	BV(λx.M)=BV(M) ∪ {x}

代入/替换(Substitution)

x[x:=M] ≡ M
y[x:=M] ≡ y (y和x是不同的变量，无事发生)
(AB)[x:=M] ≡ A[x:=M] B[x:=M]
(λx.A)[x:=M] ≡ λx.A 绑定变量不会被替换
(λy.A)[x:=M] ≡ λy.(A[x:=M]) 去A里碰碰运气

α-变换(Conversion) 其实就是给变量改名
M =>(α) N : e.g. 将M中所有λx[A]替换为λy[A[x:=y]]

栗子

(λab.x a b) =>(α) (λaz.x a z)

β-规约(reduction)

(λx.M N) => M[x:=N]

要求：BV(M) ∪ FV(N) = ø THIS IS IMPORTANT!

例如，
(λx.y)[y:=x] => λx.x 是错误的, 或者说, λy.(λx.y) x => λx.x 是错误的β-规约.

# Haskell.

定义函数 f(x,y) = 2x + y. Haskell 中可以这样写:

1
2


f :: Int -> Int -> Int
f x y = (+) ( (*) 2 x ) y

函数类型为什么要写作 Int -> Int -> Int 呢？按照其他编程语言的习惯，写成 (Int Int) -> (Int) 也许会更直观一点。但是从λ演算的角度看，前者才是合理的。

所谓函数，就是“接受一个东西，返回一个东西”。所以说我们是不能直接去定义“接受两个东西，返回一个东西”的函数的，而是通过嵌套来间接定义f.

定义term f

f = (λx.(λy.( + (* 2 x) y )))
  = (λxy.( + (* 2 x) y ))

那么

   f 1 2
=> (λy.(+ (* 2 1) y)) 2    [1]
=> (+ (* 2 1) 2)           [2]
=  (+ 2 2)             
=  4

f 在读取第一个参数1后，经过一次β-reduction 得到[1], 可以看到，[1]在等待下一个参数，或者确切地说:

1

[1] :: Int -> Int

当[1]进一步读取下一个参数2并做β-reduction 后，就会得到[2]

[2] =>* Int

用人话讲：所谓 f :: Int -> Int -> Int其实是说：

函数f: 接受一个整数参数后，返回一个函数f'
函数f’:接受一个整数，返回一个整数。
例如 f a b, f接受a, 返回 f’, 而f’ 进一步接受b，返回整数结果

# 一些习题

求FV,BV:

(λx.x y ) (λy.y)
      ^
      free

BV={x,y}
FV={y}

(λx.(λy.z (λz.z (λx.y))))
        ^     ^
        |     this one not free
        |
        this one free

BV={x,y,z} 
FV={z}

(λx.(λy.x z (y z)))  (λx.y (λy.y))
|_________________|  |___________|
BV={x,y} FV={z}       BV={x,y} FV={y}
|________________________________|
        BV={x,y} FV={z,y}

β-reduction

    (λx.(λy.x z (y z))) (λx.y (λy.y))
=   (λxy.x z (y z))  (λx.y (λy.y))
=>  (λxt.x z (t z))  (___________)    [α-conversion y->t]
=>  (λt.(λx.y (λy.y)) z (t z))
=>  (λt.y (λy.y) (t z))

    (λx.(λy.(λz.z))) x (+ y 1)
=>  (λy.(λz.z)) (+ y 1)
=>  (λz.z)

    (λx.(λy.x (λz.y z))) (((λx.(λy.y)) 8) (λx.(λy.y) x))
=   (λxy.x (λz.y z))   ( (λxy.y 8)  (λx.(λy.y) x) )
=>  (______________)   ( (λy.y   )   (λx. x     ) )
=>  (______________)   ( λx.x )
=>  (λy. (λx.x) (λz.y z))
=>  (λy. (λz.y z))

REFS

Stanford Encyclopedia of Philosophy
UPenn CIS-194
TU Dresden ‘Programmierung’

主要参考学校Programmierung课程讲义

在vim insert模式下，按下 Ctrl+k, 然后输入l*即可得到λ符号.