Church 编码

发表于 |

介绍 Church 编码和 Scott 编码。

邱奇数使用 lambda 构成的高阶函数来描述自然数。事实上邱奇编码可以用来描述一些很基本的结构，例如布尔值、元组、列表和 tagged unions。
可以将 0 表示为函数 zero 即 \f x. x。x 是什么并不重要，但我们可以将 f 令为 add1，将 x 令为 0。那么 0 就是 zero(add1, 0) = 0。
然后，可以将 1 表示为函数 one 即 \f x. f x。进行代换可以得到 one(add1, 0) = add1(0)。同理，将 2 表示为 \f x. f (f x)。
任意一个数 n 可以表示为($) f^n x，我们要想出一个结构实现把 f 执行 n 次，那实际上需要套一个递归的概念。下面来定义这个 Successor 函数 s。
递推函数 s 可以求出 n 的 Successor 为 \n f x -> f (($) n f x)。检查类型

1
2
ghci> :t s
s :: ((t1 -> t2) -> t3 -> t1) -> (t1 -> t2) -> t3 -> t2

可以理解为 s 是接受一个函数 n，返回另一个和 f/x 有关的函数。不妨简单带入

  1. add1 (($) zero add1 0) 为 1
  2. add1 (($) one add1 0) 为 2

实现加法函数plus(m, n) = m + n，plus = \m n f x. m f(n f x)。这里用到了性质f^(m+n) x = f^m f^n x。
实现乘法函数multi(m, n) = m * n，multi = \m n f x. m (n f) x。相当于将 n f 应用 m 次在 x 上。而 n f 表示 n。

1
2
3
4
5
6
7
8
9
10
11
add1 x = x + 1
shownat n = ($) n add1 0
zero = \f x -> x
s = \n f x -> f (($) n f x)
one = s zero
two = s one
three = s two
shownat one

add n m f x = ($) n f (($) m f x)
multi n m f = n (m f)
1
2
3
4
5
6
7
8
ghci> :t zero
zero :: p1 -> p2 -> p2
ghci> :t one
one :: (t1 -> t2) -> t1 -> t2
ghci> :t two
two :: (t3 -> t3) -> t3 -> t3
ghci> :t three
three :: (t3 -> t3) -> t3 -> t3

下面定义和 bool 量有关的函数。可以看到，true 就是传两个元素选择第一个，false 就是选择第二个。

1
2
3
true x y = x
false x y = y
showbool b = ($) b True False

容易看出，通过 true 和 false，可以自然而然定义出 if-then-else 语义

1
ifte pred x y = ($) pred x y

下面定义 pair 结构。不同于一般编程中指定如何构造结构，这里的思路是定义如何去消费这个结构。这里可以传入一个 sel。sel 可以是 fst 和 snd，表示选出 a 或者 b。

1
2
3
4
pair a b sel = ($) sel a b
fst p = p true
snd p = p false
shownat (fst (($) pair one two))

这里有个小问题，写成 pair a b sel = sel $ a b 会有错误

1
2
3
4
5
<interactive>:28:1: error:
    ? Non type-variable argument in the constraint: Num (t3 -> t3)
      (Use FlexibleContexts to permit this)
    ? When checking the inferred type
        it :: forall {t3}. Num (t3 -> t3) => t3 -> t3

下面定义 pair 上的函数 next。(next (: pair a b)) 返回 (: pair (s a) a)，可以理解为 pair 上的 Successor。
思路很简单，新构造一个 pair，它的第二个元素是 (fst p)，第一个元素是 s (fst p)>

1
2
3
next p = ($) pair (s (fst p)) (fst p)
nn_of_a a = ($) fst (next (($) pair a a))
shownat $ nn_of_a one

实现减法函数，首先先实现一个 pred 函数。它可以求出 n - 1 是什么。例如 pred two 是 one，但 pred zero 是 zero。这里的方案是从 pair zero zero 开始，调用 n 次 next，就可以得到 (n, n - 1)。使用 snd 返回就行。

1
pred n = snd (($) n next (($) pair zero zero))

减法函数

1
sub m n = ($) m (pred n)

下面这个函数用来判断 n 是不是 0。

1
isZero n = ($) n (\x -> false) true

不妨进行代入来看看原理

  1. zero

    1
    ($) (\f x -> x) (\x -> false) true

    这里的 f 实际上就是 (\x -> false)，而 x 就是 true。所以肯定是 true。

  2. one

    1
    ($) (\f x -> f x) (\x -> false) true

    这里代入就是 (\x -> false) true，即 false。

Reference

  1. http://learnyouahaskell.com
  2. https://www.zhihu.com/question/19804597
    Church 编码
  3. https://faculty.iiit.ac.in/~venkatesh.choppella/popl/current-topics/lambda-calculus-2/index.html
    Church 编码