summaryrefslogtreecommitdiff
path: root/docs/fype.txt
diff options
context:
space:
mode:
authoradmin (centauri.fritz.box) <puppet@mx.buetow.org>2014-06-30 23:53:04 +0200
committeradmin (centauri.fritz.box) <puppet@mx.buetow.org>2014-06-30 23:53:04 +0200
commitadc4b59a3e7c9db6f33670164490830d87331228 (patch)
treeadc5d21856852bfb5c3cca794a9c07ad476d877e /docs/fype.txt
parent63cf3028445d8d213ffc774f77aafd7283cb4fbd (diff)
parent5ab5de91eb0ae6ed9db78a2c8c47ec67f105e504 (diff)
Diffstat (limited to 'docs/fype.txt')
-rw-r--r--docs/fype.txt31
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);
+
+
+
+