计算lambda演算-或FALSE-TRUE

Question

TRUE=λxy。x

FALSE=λxy。y

IF=λbtf。b t f

AND=λxy。如果x y错误

OR=λxy。如果x真y

NOT=λx。如果x假真

我如何使用lambda演算来β-减少表达式OR FALSE TRUE？我不知道从哪里开始。我的讲师没有复习。这是我的尝试

(xy.IF x TRUE y)(xy.y)(xy.x)
= (xy.IF x TRUE y)[x := (xy.y))(xy.x)
= (y. IF (xy.y) TRUE y)(xy.x)
= (IF (xy.y) TRUE y)[y := (xy.x))
= IF (xy.y) TRUE (xy.x)

Answer 1

当您使用Church编码时，我认为最好尽可能保持抽象，即不应急切地展开TRUE、FALSE、IF和NOT，而应仅在需要时展开。

相反，你首先想证明他们行为的基本结果，这也有助于进行理智检查。对于IF，您需要检查IF TRUE t f = t和IF FALSE t f = f。

IF TRUE t f = TRUE t f   (IF returns its arguments directly)
= t          (TRUE returns its first argument)

与IF FALSE相同。

现在

OR FALSE TRUE = IF FALSE TRUE TRUE

通过应用你已经证明的身份，你应该能够得出结论。