diff options
| author | Paul Buetow <paul@buetow.org> | 2010-05-09 10:24:06 +0000 |
|---|---|---|
| committer | Paul Buetow <paul@buetow.org> | 2010-05-09 10:24:06 +0000 |
| commit | 0b7e31f8586a8237297f29793169b3eb27842f46 (patch) | |
| tree | d9fc06ec69b3a5b02b1261971698547a109356f0 | |
| parent | 5e108defdc5d94252eb81a25b084e39a782a5b03 (diff) | |
| -rw-r--r-- | docs/fype.txt | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/docs/fype.txt b/docs/fype.txt index 87ebee2..77ccdad 100644 --- a/docs/fype.txt +++ b/docs/fype.txt @@ -1,11 +1,13 @@ -Lambda Rules +Lambda Rules: (1) x ϵ V => x ϵ Λ (2) M,N ϵ Λ => (M N) ϵ Λ (Application) (3) M ϵ Λ and x ϵ V => (λx.M) ϵ Λ (Abstraction) (4) No further Terms in Λ existent -(λx.(λy.x)) ≡ λx.λy.x ≡ λxy.x ≡ False -(λx.(λy.y)) ≡ λx.λy.y ≡ λxy.y ≡ True -λx.λy.((x y) False) ≡ λxy.((x y) False) ≡ "And" +Examples: + +(λx.(λy.x)) ≡ λx.λy.x ≡ λx y.x ≡ false +(λx.(λy.y)) ≡ λx.λy.y ≡ λx y.y ≡ true +λx.λy.((x y) false) ≡ λx y.((x y) false) ≡ and |