如何在lambda演算中编码

Question

我在Haskell学习lambda演算,在那期间,我遇到了这个问题.

这些问题的解决方案是这样的:

但我无法理解他们如何得出答案.就像eq一样,我不明白他们是如何做到这一点的: ?ab.a b (b (?xy.y) (?xy.x)) 和nand一样.如果有人解释它并帮助我理解这个问题,那将是非常好的.

谢谢.

Answer 1

让我们首先用实际数据类型编写有问题的函数(但没有模式匹配:仅if/ then/ else):

data Bool = False | True -- recall this definition
not  a   = if a then False else True
eq   a b = if a then (if b then True  else False)
                else (if b then False else True )
nand a b = if a then (if b then False else True )
                else (if b then True  else True )

如果您购买这些定义 - 这些定义非常简单,只需列出函数的真值表 - 那么我们就可以开始做一些推理了.首先,我们可以简化外部分支eq和nand函数:

eq   a b = if a then b else not b
nand a b = if a then not b else True

现在我们基本完成了.我们只需更换每一个False和True他们的if/ then/ else行为,并更换所有的if/ then/ else与功能应用:

type Bool a = a -> a -> a
false a b = a -- `if False then a else b` becomes `false a b`
true  a b = b -- `if True  then a else b` becomes `true  a b`

not  a   = a false true   -- from `if a then False else True`
eq   a b = a b (not b)    -- from `if a then b else not b`
nand a b = a (not b) true -- from `if a then not b else True`

这些是您的解决方案中给出的定义,但不可否认的是Haskell语法而不是lambda演算语法.