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等价吗?从结果上来看,他们对于同样的输入给出同样的输出,然而我们仍然无法判定这两个“规则”是否是等价的。

淦。

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)$
Jun 9, 2021


[+] click to leave a comment [+]
the comment system on this blog works via email. The button
below will generate a mailto: link based on this page's url 
and invoke your email client - please edit the comment there!

[optional] even better, encrypt the email with my public key

- don't modify the subject field
- specify a nickname, otherwise your comment will be shown as   
  anonymous
- your email address will not be disclosed
- you agree that the comment is to be made public.
- to take down a comment, send the request via email.

>> SEND COMMENT <<




Fun with Image Maps and SVGs via benji February 20, 2024

Over the past few weeks I've been playing around with making some images on my website interactive. My "informatics" class in high school taught us some basic HTML. By basic I mean in notepad and writing everything by hand, saving to a...

Goblin Week 2024 via Helvetica Blanc January 26, 2024

It snuck up on me, but I managed to draw my little goblins to celebrate the week! I love my children - they're like awful Pikmin. I've uploaded the whole parade as a print, as well as individual prints for each goblin. There's something very fu…

How to trust gpg keys via Travis Shears Personal Site October 27, 2023

After moving some GPG keys to a new computer I kept getting these trust warnings. It is NOT certain that the key belongs to the person named in the user ID.If you * really * know what you are doing, you may answer the next question with yes. Use this key a…

Generated by openring from webring