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