Language

对丘奇整数的一点思路整理

记录自己在理解sicp习题2.6中Church计数时的思考过程，对术语的定义均来自wiki。谨记函数为一等公民，过程即数据。

λ演算

  • λ演算由阿隆佐·丘奇和他的学生在20世纪30年代引入，对函数式编程语言有巨大的影响。λ演算之通用在于，任何一个可计算函数都能用这种形式来表达和求值。λ演算强调的是变换规则的运用，而非实现它们的具体机器。
  • 在λ演算中，每个表达式都代表一个函数，该函数接受一个参数并返回一个值，且无论参数还是返回值均为一个单参函数。即λ演算中存在且仅存在一种类型，为单参函数。对于现实中看起来接受两个参数的函数，实质为一个接受单一参数并返回接受另一个“接受单一参数”的函数，即柯里化。
  • 在sicp的习题2.6中，对Church计数的0和add-1定义如下。
1
2
3
4
(define zero (lambda (f) (lambda (x) x)))

(define (add-1 n)
	(lambda (f) (lambda (x) (f ((n f) x)))))
  • 对上面的代码而言，通过柯里化转换成如下格式可能较易理解。但上面的形式复合λ演算的定义，即全部通过单参匿名函数实现。
1
2
3
(define zero (lambda (f x) (x)))

(define (add-1 n) (lambda (f x) (f (n f x))))

形式化描述

  • λ演算的非形式化描述通过λ表达式匿名定义，如函数\(f(x)=x+2\)的表示为\(\lambda x.x+2\)或\(\lambda y.y+2\)，参数名无关紧要），\(f(3)\)即\(3+2\)可表示为\((\lambda x.x+2) 3\)，也可以表示为\((\lambda f.f 3)(\lambda x.x+2)\)，这三者等价。然而并非所有的lambda表达式都可以规约成某种通用的函数，例如考虑\((\lambda x.x x)(\lambda x.x x)\)，其不具有确定值。
  • 对λ演算的形式化定义为，从一个标识符的可数无穷集合开始，如\({a, b, c, \ldots, x, y, …}\)，则所有的λ表达式可以通过下述上下文无关文法描述，前两条规则用来生成函数，第三条描述了函数对参数的作用方式。其中函数定义为左结合，且λ操作符绑定到它后面的整个表达式，因此括号在无歧义情况下可以舍弃。
    • <表达式> ::= <标识符>
    • <表达式> ::=(λ<标识符> .<表达式>)
    • <表达式> ::=(<表达式> <表达式>)
  • 以上λ表达式并未定义函数，例如\(\lambda x.(x y)\)中变量y的出现时自由的，其并未被绑定到表达式的任何一个λ上。一个λ表达式的自由变量的集合通过下面规则定义，分别对应上面形式化定义的各点。
    • 在表达式\(V\)中，V为变量，则该表达式自由变量的集合只有V。
    • 在表达式\(\lambda V .E\)中（V为变量，E是另一个表达式），自由变量的集合为E中自由变量的集合减去变量V。因此E中的V被绑定在λ上。例如\(\lambda x.x\)，将第一个x视为变量，第二个x视为表达式，则其自由变量集合为空集。
    • 在表达式\((E E’)\)中，自由变量的集合石E和E’中自由变量集合的并集。例如\(\lambda x.x x\)，可以看作\(((\lambda x.x)(x))\)，因此自由变量集合为\({x}\)。

归约

  • 根据λ演算的形式化定义，可以在λ表达式的集合上定义等价关系，即表述：“两个表达式其实表示的是同一个函数”。
  • α-变换：被绑定变量的名称是不重要的。具体陈述为：若V与W均为变量，E是一个λ表达式，同时E[V:=W]是指把表达式E中的所有的V的自由出现都替换为W，那么在W不是E中的一个自由出现，且如果W替换了V，W不会被E中的λ绑定的情况下，有λV.E == λW.E[V:=W]
  • β-归约：其表达的是函数作用的概念。陈述了若所有的E’的自由出现在E [V:=E’]中仍然是自由的情况下，有((λV.E) E') == E [V:=E']成立。
  • η-变换：表达的是外延性的概念，即两个函数对于所有的参数得到的结果都一致，当且仅当它们是同一个函数。

丘奇整数

  • 丘奇整数是将自然数用高阶函数展示的一种形式。它将自然数n表示为任意给定函数f自身的n重复合。所有的丘奇整数都是接受两个参数的函数，可以通过λ演算定义如下。
1
2
3
4
5
6
0 ≡ λf.λx. x
1 ≡ λf.λx. f x
2 ≡ λf.λx. f (f x)
3 ≡ λf.λx. f (f (f x))
...
n ≡ λf.λx. fn x
  • 对于sicp给出的0和add定义，可以用haskell表示，并用:t查看其type。
1
2
3
4
5
6
7
8
Prelude> let zero = (\f -> \x -> x)
Prelude> :t zero
zero :: t -> t1 -> t1
Prelude> let add1 n = (\f -> \x -> f ((n f) x))
Prelude> :t add1
add1 :: ((t1 -> t) -> t2 -> t1) -> (t1 -> t) -> t2 -> t
Prelude> :t (add1 zero)
(add1 zero) :: (t1 -> t) -> t1 -> t
  • 由此可以得出1、2、3的定义：
1
2
3
4
5
(define one (add-1 zero)
(define one (lambda (f x) (f x))
(define one (lambda (f) (lambda (x) (f x))))
(define two (lambda (f) (lambda (x) (f (f x)))))
(define three (lambda (f) (lambda (x) (f (f (f x))))))
  • 回头看add-1的最初定义，已经感受到一致性：对n做add-1，就是对n所代表的过程再复合指定的函数f。这与丘奇整数的值和其复合指数相同一致。
1
2
(define (add-1 n)
	(lambda (f) (lambda (x) (f ((n f) x)))))
  • 下面是haskell对丘奇整数和整数之间转换的函数。
1
2
3
4
5
6
7
8
type Church a = (a -> a) -> a -> a

church :: Integer -> Church Integer
church 0 = \f -> \x -> x
church n = \f -> \x -> f (church (n-1) f x)

unchurch :: Church Integer -> Integer
unchurch cn = cn (+ 1) 0
  • 丘奇函数加深了对高阶函数、数据的过程性和书中“总可以将数据定义为一组适当的选择函数和构造函数，以及为使这些过程成为一套合法表示，他们就必须满足的一组特定条件”的认识。日后对λ演算做深入学习时再作补充。

参考文献： 《计算机程序的构造和解释》

原创作品，允许转载，转载时无需告知，但请务必以超链接形式标明文章原始出处(https://forec.github.io/2016/03/24/church-count/) 、作者信息（Forec）和本声明。

分享到