Lambda-calculus: 布尔逻辑
使用λ-演算定义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等价吗?从结果上来看,他们对于同样的输入给出同样的输出,然而我们仍然无法判定这两个“规则”是否是等价的。
淦。
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)$
[+] click to leave a comment [+]
>> SEND COMMENT <<