4.4 对编码
实行对编码,我们需要三类操作:
- 结合两个值
- 提取第一个值的操作
- 提取第二个值的操作
话句话说,我们需要 mkpair, fst, snd 满足下述等式:
f s t ( m k p a i r M N ) = n M s n d ( m k p a i r M N ) = n N fst(mkpair\ M\ N) =_n M\\ snd(mkpair \ M\ N) =_n N fst(mkpair M N)=nMsnd(mkpair M N)=nN
我们也可以使用符号 ⟨M, N⟩ 作为对的缩写(第一个值为M,第二个值为N)。一种寻找 mkpair 等定义的方法是考虑一个 ⟨M, N⟩ 的值可能长什么样。
因为我们所有的值都是函数,⟨M, N⟩ 也必须是一个函数,这个函数需要包含 M 和 N 的表达式,并且,它必须又返回给用户其中一个值的方法(取决于用户需要第一个还是第二个值)。这提示了用户必须以函数的方式调用对,并且提供 true 来得到第一个值,提供 false 来得到第二个值:
⟨ M , N ⟩ ≐ λ s . i f s M N ⟨M,N⟩\doteq \lambda s.if\ s\ M\ N ⟨M,N⟩≐λs.if s M N
前一小节说过,if 函数并不是必要的,所以上述函数可以通过丢弃 if 简化。
这样编码, fst 函数接收对值,并且应用其作为 true的参数。
f s t ≐ λ p . p t r u e fst\doteq\lambda p.p\ true fst≐λp.p true
类似地, snd 应用对值作为false的参数。最终,为了定义 mkpair,我们将 ⟨M, N⟩ 抽象缩写成任意 M 与 N。
练习 4.5
证明上述的 mkpair,fst 和 snd 满足此小节开头的等式。
题解
-
fst (mkpair M N) = (λp.p true) ((λx.λy.λs.s x y) M N)
→nβ ((λx.λy.λs.s x y) M N) true
→nβ (λy.λs.s M y) N) true
→nβ (λs.s M N) true
→nβ true M N = (λx.λy.x) M N
→nβ (λ.M) N
→nβ M
-
snd (mkpair M N) = (λp.p false) ((λx.λy.λs.s x y) M N)
→nβ ((λx.λy.λs.s x y) M N) false
→nβ (λy.λs.s M y) N) false
→nβ (λs.s M N) false
→nβ false M N = (λx.λy.y) M N
→nβ (λy.y) N
→nβ N