使用λ-演算定义True/False, 并进行布尔运算。

Recap: λ-Combinators
A λ-Term without free variables is a combinator.

Lambda-Calculus

首先定义λ-Term TRUE 和 FALSE

$\text{TRUE}:= \lambda x.(\lambda y. x)$
$\text{FALSE}:= \lambda x.(\lambda y. y)$

TRUE 和FALSE 都是“函数”,TRUE 接受两个参数，返回第一个参数，FALSE接受两个参数，返回第二个参数。

定义NOT运算
$\text{NOT}:= \lambda a.(a)(\text{FALSE TRUE})$

WTF? … Let’s see…

下面证明
$\neg \text{TRUE}=\text{FALSE}$
$\neg \text{FALSE}=\text{TRUE}$

    NOT TRUE
=   (λa.(a) (FALSE TRUE)) TRUE
=>  (TRUE) (FALSE TRUE)
=>  FALSE              

根据TRUE的定义，接受两个参数，返回第一个,所以(TRUE) (FALSE TRUE) 返回 FALSE

    NOT FALSE
=   (λa.(a) (FALSE TRUE)) FALSE
=>  (FALSE) (FALSE TRUE)
=>  TRUE              

同理

AND $\text{AND}:= \lambda xy.(x)(y)(\text{FALSE})$

    AND X  Y
=>  (X) (Y) (FALSE)

当X为TRUE时，返回第一个参数Y
当X为FALSE时，返回第二个参数FALSE

x\y  | TRUE | FALSE
--------------------
TRUE | TRUE | FALSE
--------------------
FALSE| FALSE| FALSE

OR $\text{OR}:= \lambda xy.(x)(\text{TRUE})(y)$

     OR X Y
=>   X (TRUE) Y

当X为TRUE时，返回第一个参数TRUE
当X为FALSE时，返回第二个参数Y

x\y  | TRUE | FALSE
--------------------
TRUE | TRUE | TRUE
--------------------
FALSE| TRUE | FALSE

是否满足性质？

使用真值表可以很方便地证明各种性质。。。然而这是一个哲学问题：

例如我想证明 (AND X Y) = (AND Y X)
本质上是要证明 (AND X Y) 和 (AND Y X) 等价。然而左右都是函数，如何证明两个函数等价？

真值表的方法说：如果函数f和函数g对于同样的输入给出同样的输出，那么f和g等价。这是集合映射的思路:

用集合，二元函数AND 可以理解为

AND(x,y): {TRUE,FALSE}x{TRUE,FALSE} -> {TRUE,FALSE}
f = {<<TRUE,TRUE>,TRUE> , ...... }

判定f和g等价，只需要判定f和g所表示的关系集合相等。(Functions-as-set)。通过集合定义的函数是“外延的”(extensional)

然而λ-calculus所定义的函数并不是通过关系集合来定义的，而是通过“规则”.(Functions-as-rules), 他是非外延的(non-extensional)，(但也不完全是内涵intensional的)

对于λ项M N, 虽然可以判断他们在某些情况下是否有同样的表现，但无法直接判定他们是否等价。

如果使用真值表的方法证明M ≡ N, 那么我们得到的结论是: M和N的外延等价。

再举一个例子是:

F := λx.[x + 1]
G := λx.[x + 2 - 1]

我们能说F 和 G等价吗？从结果上来看，他们对于同样的输入给出同样的输出，然而我们仍然无法判定这两个“规则”是否是等价的。

淦。

SEE THIS

Bool logic:

值 Values

• True (1)
• False (0)

运算

• AND $\wedge$
• OR $\vee$
• NOT $\neg$

其他运算如XOR,Implication, 可以通过AND OR NOT定义。

定律/性质

• 结合律
  • $x\vee (y\vee z) = (x\vee y) \vee z$
  • $x\wedge (y\wedge z) = (x\wedge y) \wedge z$
• 交换律
  • $x\vee y=y\vee x$
  • $x\wedge y=y\wedge x$
• 分配率
  • $x\wedge (y\vee z) = (x\wedge y)\vee (x\wedge z)$
  • $x\vee (y\wedge z) = (x\vee y)\wedge (x\vee z)$
• identy
  • $x\vee 0 = x$
  • $x\wedge 1 = x$
• Annihilator
  • $x\wedge 0 = 0$
  • $y\vee1 = 1$
• Idempotence
  • $x\vee x = x$
  • $x\wedge x = x$
• Absorption
  • $x\wedge (x\vee y)=x$
  • $x\vee (x\wedge y)=x$
• Complementation
  • $x\wedge \neg x = 0$
  • $x\vee \neg x = 1$
• Double negation:
  • $\neg(\neg x) = x$
• De Morgan laws:
  • $\neg x \wedge \neg y = \neg(x\vee y)$
  • $\neg x \vee \neg y = \neg(x\wedge y)$