diff options
| author | admin (centauri.fritz.box) <puppet@mx.buetow.org> | 2014-06-30 23:53:04 +0200 |
|---|---|---|
| committer | admin (centauri.fritz.box) <puppet@mx.buetow.org> | 2014-06-30 23:53:04 +0200 |
| commit | adc4b59a3e7c9db6f33670164490830d87331228 (patch) | |
| tree | adc5d21856852bfb5c3cca794a9c07ad476d877e /docs/fype.txt | |
| parent | 63cf3028445d8d213ffc774f77aafd7283cb4fbd (diff) | |
| parent | 5ab5de91eb0ae6ed9db78a2c8c47ec67f105e504 (diff) | |
Mergebuild-010393-lambda
Diffstat (limited to 'docs/fype.txt')
| -rw-r--r-- | docs/fype.txt | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/docs/fype.txt b/docs/fype.txt new file mode 100644 index 0000000..004652e --- /dev/null +++ b/docs/fype.txt @@ -0,0 +1,31 @@ +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 + +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 + +Syntax: + +(λx . (λy.x)) ≡ λx.λy.x ≡ λx y . x ≡ false +true: x y = x; + +(λx.(λy.y)) ≡ λx.λy.y ≡ λx y . y ≡ true +false: x y = y; + +λx.λy.((x y) false) ≡ λx y.((x y) false) ≡ and +and: x y = (x y) false; + +id: x = x; + +greet: x = say (~ "Hello " x); + + + + |
