lambda演算系列搬运cgnail的blog，源blog连接为这里。

现在，我们在lambda演算中引入了数字，只差两件事情就可以表达任意计算了：一个是如何表达选择（分支），另一个是如何表示重复。在这篇文章中，我将讨论布尔值和选择，下一篇将介绍重复和递归。

我们希望能够写出形如 if / then / else语句的表达式，就像我们在大多数编程语言做的那样。继像丘奇数那样将数字表示为函数之后，我们也将true和false值表示为对其参数执行一个if-then-else操作的函数：

1
2
let TRUE = lambda x y . x 
let FALSE = lambda x y . y

于是，现在我们可以写一个“if”函数，它的第一个参数是一个条件表达式，第二个参数是如果条件为真时才进行运算的表达式，第三个参数则如果条件为假时要进行的运算。

1
let IfThenElse = lambda cond true_expr false_expr . cond true_expr false_expr

此外我们还需要定义常用的逻辑运算：

1
2
3
let BoolAnd = lambda x y . x y FALSE 
let BoolOr = lambda x y. x TRUE y 
let BoolNot = lambda x . x FALSE TRUE

现在，就让我们过一遍这些定义。让我们先看看BoolAnd：

  • BoolAnd TRUE FALSE，展开TRUE和FALSE定义：BoolAnd (lambda x y . x) (lambda x y . y)
  • alpha变换true和false：BoolAnd (lambda xt yt . xt) (lambda xf yf . yf)
  • 现在，展开BoolAnd：(lambda x y. x y FALSE) (lambda xt yt . xt) (lambda xf yf . yf)
  • beta规约：(lambda xt yt.xt) (lambda xf yf. yf) FALSE
  • 再次beta规约：(lambda xf xf . yf)

于是我们得到结果：BoolAnd TRUE FALSE = FALSE。再让我们来看看BoolAnd FALSE TRUE：

  • BoolAnd (lambda x y . y) (lambda x y .x)
  • alpha变换：BoolAnd (lambda xf yf . yf) (lambda xt yt . xt)
  • 展开BoolAnd： (lambda x y .x y FALSE) (lambda xf yf . yf) (lambda xt yt . xt)
  • beta规约：(lambda xf yf . yf) (lambda xt yt . xt) FALSE
  • 再beta规约：FALSE

所以，BoolAnd FALSE TRUE = FALSE

最后让我们来算算，BoolAnd TRUE TRUE：

  • 展开两个TRUE： BoolAnd (lambda x y . x) (lambda x y . x)
  • alpha变换： BoolAnd (lambda xa ya . xa) (lambda xb yb . xb)
  • 展开BoolAnd： (lambda x y . x y FALSE) (lambda xa ya . xa) (lambda xb yb . xb)
  • beta规约： (lambda xa ya . xa) (lambda xb yb . xb) FALSE
  • beta规约： (lambda xb yb .xb)

所以，BoolAnd TRUE TRUE = TRUE