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

  1. 所有的变量(variable)都是λ-term
  2. 如果 MN 都是λ-term, 那么 M N也是λ-term
  3. 如果 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)

  1. x[x:=M] ≡ M
  2. y[x:=M] ≡ y (y和x是不同的变量,无事发生)
  3. (AB)[x:=M] ≡ A[x:=M] B[x:=M]
  4. (λx.A)[x:=M] ≡ λx.A 绑定变量不会被替换
  5. (λ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 中可以这样写:

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] :: 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*即可得到λ符号.