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 中可以这样写:

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

Jun 7, 2021


[+] click to leave a comment [+]
the comment system on this blog works via email. The button
below will generate a mailto: link based on this page's url 
and invoke your email client - please edit the comment there!

[optional] even better, encrypt the email with my public key

- don't modify the subject field
- specify a nickname, otherwise your comment will be shown as   
  anonymous
- your email address will not be disclosed
- you agree that the comment is to be made public.
- to take down a comment, send the request via email.

>> SEND COMMENT <<




Fun with Image Maps and SVGs via benji February 20, 2024

Over the past few weeks I've been playing around with making some images on my website interactive. My "informatics" class in high school taught us some basic HTML. By basic I mean in notepad and writing everything by hand, saving to a...

Goblin Week 2024 via Helvetica Blanc January 26, 2024

It snuck up on me, but I managed to draw my little goblins to celebrate the week! I love my children - they're like awful Pikmin. I've uploaded the whole parade as a print, as well as individual prints for each goblin. There's something very fu…

How to trust gpg keys via Travis Shears Personal Site October 27, 2023

After moving some GPG keys to a new computer I kept getting these trust warnings. It is NOT certain that the key belongs to the person named in the user ID.If you * really * know what you are doing, you may answer the next question with yes. Use this key a…

Generated by openring from webring