add homework material

67 files changed, 767 insertions, 0 deletions

diff --git a/tests/examples/beta.lam b/tests/examples/beta.lam
new file mode 100644
index 0000000..9d53b08
--- /dev/null
+++ b/tests/examples/beta.lam
@@ -0,0 +1,3 @@
+(\ x . (\ z . z z) x three) ((\ y . y y) (\ w . w))
+
+-- Should reduce to three
diff --git a/tests/examples/beta.out b/tests/examples/beta.out
new file mode 100644
index 0000000..ac8f0f0
--- /dev/null
+++ b/tests/examples/beta.out
@@ -0,0 +1 @@
+(\x . (\z . z z) x three) ((\y . y y) (\w . w))
diff --git a/tests/examples/beta1.lam b/tests/examples/beta1.lam
new file mode 100644
index 0000000..3ffc446
--- /dev/null
+++ b/tests/examples/beta1.lam
@@ -0,0 +1,3 @@
+(\x . x three) (\y . plus y y)
+
+-- Should reduce to plus three three
diff --git a/tests/examples/beta1.out b/tests/examples/beta1.out
new file mode 100644
index 0000000..6ceecd5
--- /dev/null
+++ b/tests/examples/beta1.out
@@ -0,0 +1 @@
+(\x . x three) (\y . plus y y)
diff --git a/tests/examples/beta2.lam b/tests/examples/beta2.lam
new file mode 100644
index 0000000..02ae576
--- /dev/null
+++ b/tests/examples/beta2.lam
@@ -0,0 +1,3 @@
+(\x . (\x . x) x) one
+
+-- should reduce to one
diff --git a/tests/examples/beta2.out b/tests/examples/beta2.out
new file mode 100644
index 0000000..3434328
--- /dev/null
+++ b/tests/examples/beta2.out
@@ -0,0 +1 @@
+(\x . (\x . x) x) one
diff --git a/tests/examples/beta3.lam b/tests/examples/beta3.lam
new file mode 100644
index 0000000..e112b5c
--- /dev/null
+++ b/tests/examples/beta3.lam
@@ -0,0 +1,3 @@
+(\ x . \ y . x y ) y
+
+-- Should reduce to \z . y z (for some fresh z)
diff --git a/tests/examples/beta3.out b/tests/examples/beta3.out
new file mode 100644
index 0000000..322346c
--- /dev/null
+++ b/tests/examples/beta3.out
@@ -0,0 +1 @@
+(\x . \y . x y) y
diff --git a/tests/examples/bools-and-t-f.lam b/tests/examples/bools-and-t-f.lam
new file mode 100644
index 0000000..fd9a29c
--- /dev/null
+++ b/tests/examples/bools-and-t-f.lam
@@ -0,0 +1,16 @@
+(\ true false and or not .
+
+    and true false
+
+    -- Should reduce to false, i.e., \ x y . y
+)
+-- true
+(\ x y . x)
+-- false
+(\ x y . y)
+-- and
+(\ p q . p q p)
+-- or
+(\ p q . p p q)
+-- not
+(\ p x y . p y x)
diff --git a/tests/examples/bools-and-t-f.out b/tests/examples/bools-and-t-f.out
new file mode 100644
index 0000000..e422fcc
--- /dev/null
+++ b/tests/examples/bools-and-t-f.out
@@ -0,0 +1 @@
+(\true . \false . \and . \or . \not . and true false) (\x . \y . x) (\x . \y . y) (\p . \q . p q p) (\p . \q . p p q) (\p . \x . \y . p y x)
diff --git a/tests/examples/bools-not-t.lam b/tests/examples/bools-not-t.lam
new file mode 100644
index 0000000..9afcc48
--- /dev/null
+++ b/tests/examples/bools-not-t.lam
@@ -0,0 +1,16 @@
+(\ true false and or not .
+
+    not true
+
+    -- Should reduce to false, i.e., \ x y . y
+)
+-- true
+(\ x y . x)
+-- false
+(\ x y . y)
+-- and
+(\ p q . p q p)
+-- or
+(\ p q . p p q)
+-- not
+(\ p x y . p y x)
diff --git a/tests/examples/bools-not-t.out b/tests/examples/bools-not-t.out
new file mode 100644
index 0000000..2a6a257
--- /dev/null
+++ b/tests/examples/bools-not-t.out
@@ -0,0 +1 @@
+(\true . \false . \and . \or . \not . not true) (\x . \y . x) (\x . \y . y) (\p . \q . p q p) (\p . \q . p p q) (\p . \x . \y . p y x)
diff --git a/tests/examples/bools-or-f-t.lam b/tests/examples/bools-or-f-t.lam
new file mode 100644
index 0000000..5c39cd8
--- /dev/null
+++ b/tests/examples/bools-or-f-t.lam
@@ -0,0 +1,16 @@
+(\ true false and or not .
+
+    or false true
+
+    -- Should reduce to true, i.e., \ x y . x
+)
+-- true
+(\ x y . x)
+-- false
+(\ x y . y)
+-- and
+(\ p q . p q p)
+-- or
+(\ p q . p p q)
+-- not
+(\ p x y . p y x)
diff --git a/tests/examples/bools-or-f-t.out b/tests/examples/bools-or-f-t.out
new file mode 100644
index 0000000..78a2057
--- /dev/null
+++ b/tests/examples/bools-or-f-t.out
@@ -0,0 +1 @@
+(\true . \false . \and . \or . \not . or false true) (\x . \y . x) (\x . \y . y) (\p . \q . p q p) (\p . \q . p p q) (\p . \x . \y . p y x)
diff --git a/tests/examples/currying.lam b/tests/examples/currying.lam
new file mode 100644
index 0000000..5463ce7
--- /dev/null
+++ b/tests/examples/currying.lam
@@ -0,0 +1,3 @@
+(\x y. plus (plus x y) x) one two
+
+-- Should reduce to plus (plus one two) one
diff --git a/tests/examples/currying.out b/tests/examples/currying.out
new file mode 100644
index 0000000..5660f00
--- /dev/null
+++ b/tests/examples/currying.out
@@ -0,0 +1 @@
+(\x . \y . plus (plus x y) x) one two
diff --git a/tests/examples/fac-three.lam b/tests/examples/fac-three.lam
new file mode 100644
index 0000000..613c933
--- /dev/null
+++ b/tests/examples/fac-three.lam
@@ -0,0 +1,31 @@
+(\ zero one two three succ plus mult pred minus isZero yComb .
+    (\ fac .
+        fac three
+       -- NOTE: the y-combinator does not have a normal form
+    ) (yComb (\ f n . (isZero n) one (mult n (f (pred n)))))
+)
+
+-- zero
+(\ f x . x)
+-- one
+(\ f x . f x)
+-- two
+(\ f x . f (f x))
+-- three
+(\ f x . f (f (f x)))
+
+-- succ
+(\n f x . f (n f x))
+-- plus
+(\m n f x . m f (n f x))
+-- mult
+(\m n f . m (n f))
+-- pred
+(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u))
+-- minus
+(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m)
+-- isZero
+(\ n . n (\ x . (\ x y . y)) (\ x y . x))
+
+-- yComb
+(\ f . (\ x . f (x x)) (\ x . f (x x)))
diff --git a/tests/examples/fac-three.out b/tests/examples/fac-three.out
new file mode 100644
index 0000000..5430f7f
--- /dev/null
+++ b/tests/examples/fac-three.out
@@ -0,0 +1 @@
+(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . \yComb . (\fac . fac three) (yComb (\f . \n . isZero n one (mult n (f (pred n)))))) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) (\f . (\x . f (x x)) (\x . f (x x)))
diff --git a/tests/examples/head-normal-form.lam b/tests/examples/head-normal-form.lam
new file mode 100644
index 0000000..bf859a0
--- /dev/null
+++ b/tests/examples/head-normal-form.lam
@@ -0,0 +1,6 @@
+-- normal form              N
+-- weak normal form         N
+-- head normal form         Y
+-- weak head normal form    Y
+
+f ((\x . x x) (\x . x x))
diff --git a/tests/examples/head-normal-form.out b/tests/examples/head-normal-form.out
new file mode 100644
index 0000000..574706c
--- /dev/null
+++ b/tests/examples/head-normal-form.out
@@ -0,0 +1 @@
+f ((\x . x x) (\x . x x))
diff --git a/tests/examples/normal-form.lam b/tests/examples/normal-form.lam
new file mode 100644
index 0000000..36afd00
--- /dev/null
+++ b/tests/examples/normal-form.lam
@@ -0,0 +1,6 @@
+-- normal form              Y
+-- weak normal form         Y
+-- head normal form         Y
+-- weak head normal form    Y
+
+f (\x . x x) (\x . x x)
diff --git a/tests/examples/normal-form.out b/tests/examples/normal-form.out
new file mode 100644
index 0000000..07dc4b3
--- /dev/null
+++ b/tests/examples/normal-form.out
@@ -0,0 +1 @@
+f (\x . x x) (\x . x x)
diff --git a/tests/examples/nums-env.lam b/tests/examples/nums-env.lam
new file mode 100644
index 0000000..c8e8a7e
--- /dev/null
+++ b/tests/examples/nums-env.lam
@@ -0,0 +1,27 @@
+(\ zero one two three succ plus mult pred minus isZero .
+
+    insert_your_expression_here
+
+)
+
+-- zero
+(\ f x . x)
+-- one
+(\ f x . f x)
+-- two
+(\ f x . f (f x))
+-- three
+(\ f x . f (f (f x)))
+
+-- succ
+(\n f x . f (n f x))
+-- plus
+(\m n f x . m f (n f x))
+-- mult
+(\m n f . m (n f))
+-- pred
+(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u))
+-- minus
+(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m)
+-- isZero
+(\ n . n (\ x . (\ x y . y)) (\ x y . x))
diff --git a/tests/examples/nums-env.out b/tests/examples/nums-env.out
new file mode 100644
index 0000000..41b34f0
--- /dev/null
+++ b/tests/examples/nums-env.out
@@ -0,0 +1 @@
+(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . insert_your_expression_here) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x))
diff --git a/tests/examples/nums-isZero-one.lam b/tests/examples/nums-isZero-one.lam
new file mode 100644
index 0000000..67e54dd
--- /dev/null
+++ b/tests/examples/nums-isZero-one.lam
@@ -0,0 +1,27 @@
+(\ zero one two three succ plus mult pred minus isZero .
+
+    isZero one
+    -- Should evaluate to false, i.e., \ x y . y
+)
+
+-- zero
+(\ f x . x)
+-- one
+(\ f x . f x)
+-- two
+(\ f x . f (f x))
+-- three
+(\ f x . f (f (f x)))
+
+-- succ
+(\n f x . f (n f x))
+-- plus
+(\m n f x . m f (n f x))
+-- mult
+(\m n f . m (n f))
+-- pred
+(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u))
+-- minus
+(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m)
+-- isZero
+(\ n . n (\ x . (\ x y . y)) (\ x y . x))
diff --git a/tests/examples/nums-isZero-one.out b/tests/examples/nums-isZero-one.out
new file mode 100644
index 0000000..4d24c9e
--- /dev/null
+++ b/tests/examples/nums-isZero-one.out
@@ -0,0 +1 @@
+(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . isZero one) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x))
diff --git a/tests/examples/nums-isZero-two.lam b/tests/examples/nums-isZero-two.lam
new file mode 100644
index 0000000..086bdc0
--- /dev/null
+++ b/tests/examples/nums-isZero-two.lam
@@ -0,0 +1,27 @@
+(\ zero one two three succ plus mult pred minus isZero .
+
+    isZero two
+    -- Should evaluate to false, i.e., \ x y . y
+)
+
+-- zero
+(\ f x . x)
+-- one
+(\ f x . f x)
+-- two
+(\ f x . f (f x))
+-- three
+(\ f x . f (f (f x)))
+
+-- succ
+(\n f x . f (n f x))
+-- plus
+(\m n f x . m f (n f x))
+-- mult
+(\m n f . m (n f))
+-- pred
+(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u))
+-- minus
+(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m)
+-- isZero
+(\ n . n (\ x . (\ x y . y)) (\ x y . x))
diff --git a/tests/examples/nums-isZero-two.out b/tests/examples/nums-isZero-two.out
new file mode 100644
index 0000000..b897fd1
--- /dev/null
+++ b/tests/examples/nums-isZero-two.out
@@ -0,0 +1 @@
+(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . isZero two) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x))
diff --git a/tests/examples/nums-isZero-zero.lam b/tests/examples/nums-isZero-zero.lam
new file mode 100644
index 0000000..4cf9dd3
--- /dev/null
+++ b/tests/examples/nums-isZero-zero.lam
@@ -0,0 +1,27 @@
+(\ zero one two three succ plus mult pred minus isZero .
+
+    isZero zero
+    -- Should evaluate to true, i.e., \ x y . x
+)
+
+-- zero
+(\ f x . x)
+-- one
+(\ f x . f x)
+-- two
+(\ f x . f (f x))
+-- three
+(\ f x . f (f (f x)))
+
+-- succ
+(\n f x . f (n f x))
+-- plus
+(\m n f x . m f (n f x))
+-- mult
+(\m n f . m (n f))
+-- pred
+(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u))
+-- minus
+(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m)
+-- isZero
+(\ n . n (\ x . (\ x y . y)) (\ x y . x))
diff --git a/tests/examples/nums-isZero-zero.out b/tests/examples/nums-isZero-zero.out
new file mode 100644
index 0000000..88be213
--- /dev/null
+++ b/tests/examples/nums-isZero-zero.out
@@ -0,0 +1 @@
+(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . isZero zero) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x))
diff --git a/tests/examples/nums-minus-one-two.lam b/tests/examples/nums-minus-one-two.lam
new file mode 100644
index 0000000..cd54d34
--- /dev/null
+++ b/tests/examples/nums-minus-one-two.lam
@@ -0,0 +1,27 @@
+(\ zero one two three succ plus mult pred minus isZero .
+
+    minus one two
+    -- Should evaluate to zero, i.e., \ f x . x
+)
+
+-- zero
+(\ f x . x)
+-- one
+(\ f x . f x)
+-- two
+(\ f x . f (f x))
+-- three
+(\ f x . f (f (f x)))
+
+-- succ
+(\n f x . f (n f x))
+-- plus
+(\m n f x . m f (n f x))
+-- mult
+(\m n f . m (n f))
+-- pred
+(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u))
+-- minus
+(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m)
+-- isZero
+(\ n . n (\ x . (\ x y . y)) (\ x y . x))
diff --git a/tests/examples/nums-minus-one-two.out b/tests/examples/nums-minus-one-two.out
new file mode 100644
index 0000000..04b0c6a
--- /dev/null
+++ b/tests/examples/nums-minus-one-two.out
@@ -0,0 +1 @@
+(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . minus one two) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x))
diff --git a/tests/examples/nums-minus-three-two.lam b/tests/examples/nums-minus-three-two.lam
new file mode 100644
index 0000000..e2fe489
--- /dev/null
+++ b/tests/examples/nums-minus-three-two.lam
@@ -0,0 +1,27 @@
+(\ zero one two three succ plus mult pred minus isZero .
+
+    minus three two
+    -- Should evaluate to one, i.e., \ f x . f x
+)
+
+-- zero
+(\ f x . x)
+-- one
+(\ f x . f x)
+-- two
+(\ f x . f (f x))
+-- three
+(\ f x . f (f (f x)))
+
+-- succ
+(\n f x . f (n f x))
+-- plus
+(\m n f x . m f (n f x))
+-- mult
+(\m n f . m (n f))
+-- pred
+(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u))
+-- minus
+(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m)
+-- isZero
+(\ n . n (\ x . (\ x y . y)) (\ x y . x))
diff --git a/tests/examples/nums-minus-three-two.out b/tests/examples/nums-minus-three-two.out
new file mode 100644
index 0000000..e924284
--- /dev/null
+++ b/tests/examples/nums-minus-three-two.out
@@ -0,0 +1 @@
+(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . minus three two) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x))
diff --git a/tests/examples/nums-mult-two-three.lam b/tests/examples/nums-mult-two-three.lam
new file mode 100644
index 0000000..f8ea7ed
--- /dev/null
+++ b/tests/examples/nums-mult-two-three.lam
@@ -0,0 +1,27 @@
+(\ zero one two three succ plus mult pred minus isZero .
+
+    mult two three
+    -- Should evaluate to six, i.e., \ f x . f (f (f (f (f (f x)))))
+)
+
+-- zero
+(\ f x . x)
+-- one
+(\ f x . f x)
+-- two
+(\ f x . f (f x))
+-- three
+(\ f x . f (f (f x)))
+
+-- succ
+(\n f x . f (n f x))
+-- plus
+(\m n f x . m f (n f x))
+-- mult
+(\m n f . m (n f))
+-- pred
+(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u))
+-- minus
+(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m)
+-- isZero
+(\ n . n (\ x . (\ x y . y)) (\ x y . x))
diff --git a/tests/examples/nums-mult-two-three.out b/tests/examples/nums-mult-two-three.out
new file mode 100644
index 0000000..1390573
--- /dev/null
+++ b/tests/examples/nums-mult-two-three.out
@@ -0,0 +1 @@
+(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . mult two three) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x))
diff --git a/tests/examples/nums-plus-three-two.lam b/tests/examples/nums-plus-three-two.lam
new file mode 100644
index 0000000..70839a5
--- /dev/null
+++ b/tests/examples/nums-plus-three-two.lam
@@ -0,0 +1,27 @@
+(\ zero one two three succ plus mult pred minus isZero .
+
+    plus three two
+    -- Should evaluate to five, i.e., (\ f x . f (f (f (f (f x)))))
+)
+
+-- zero
+(\ f x . x)
+-- one
+(\ f x . f x)
+-- two
+(\ f x . f (f x))
+-- three
+(\ f x . f (f (f x)))
+
+-- succ
+(\n f x . f (n f x))
+-- plus
+(\m n f x . m f (n f x))
+-- mult
+(\m n f . m (n f))
+-- pred
+(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u))
+-- minus
+(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m)
+-- isZero
+(\ n . n (\ x . (\ x y . y)) (\ x y . x))
diff --git a/tests/examples/nums-plus-three-two.out b/tests/examples/nums-plus-three-two.out
new file mode 100644
index 0000000..67ccb01
--- /dev/null
+++ b/tests/examples/nums-plus-three-two.out
@@ -0,0 +1 @@
+(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . plus three two) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x))
diff --git a/tests/examples/nums-pred-four.lam b/tests/examples/nums-pred-four.lam
new file mode 100644
index 0000000..02602c0
--- /dev/null
+++ b/tests/examples/nums-pred-four.lam
@@ -0,0 +1,27 @@
+(\ zero one two three succ plus mult pred minus isZero .
+
+    pred four
+    -- Should evaluate to three, i.e., \ f x . f (f (f x))
+)
+
+-- zero
+(\ f x . x)
+-- one
+(\ f x . f x)
+-- two
+(\ f x . f (f x))
+-- three
+(\ f x . f (f (f x)))
+
+-- succ
+(\n f x . f (n f x))
+-- plus
+(\m n f x . m f (n f x))
+-- mult
+(\m n f . m (n f))
+-- pred
+(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u))
+-- minus
+(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m)
+-- isZero
+(\ n . n (\ x . (\ x y . y)) (\ x y . x))
diff --git a/tests/examples/nums-pred-four.out b/tests/examples/nums-pred-four.out
new file mode 100644
index 0000000..f57d3e0
--- /dev/null
+++ b/tests/examples/nums-pred-four.out
@@ -0,0 +1 @@
+(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . pred four) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x))
diff --git a/tests/examples/nums-pred-one.lam b/tests/examples/nums-pred-one.lam
new file mode 100644
index 0000000..413046d
--- /dev/null
+++ b/tests/examples/nums-pred-one.lam
@@ -0,0 +1,27 @@
+(\ zero one two three succ plus mult pred minus isZero .
+
+    pred one
+    -- Should evaluate to zero, i.e., \ f x . x
+)
+
+-- zero
+(\ f x . x)
+-- one
+(\ f x . f x)
+-- two
+(\ f x . f (f x))
+-- three
+(\ f x . f (f (f x)))
+
+-- succ
+(\n f x . f (n f x))
+-- plus
+(\m n f x . m f (n f x))
+-- mult
+(\m n f . m (n f))
+-- pred
+(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u))
+-- minus
+(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m)
+-- isZero
+(\ n . n (\ x . (\ x y . y)) (\ x y . x))
diff --git a/tests/examples/nums-pred-one.out b/tests/examples/nums-pred-one.out
new file mode 100644
index 0000000..5e72285
--- /dev/null
+++ b/tests/examples/nums-pred-one.out
@@ -0,0 +1 @@
+(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . pred one) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x))
diff --git a/tests/examples/nums-pred-two.lam b/tests/examples/nums-pred-two.lam
new file mode 100644
index 0000000..d003d33
--- /dev/null
+++ b/tests/examples/nums-pred-two.lam
@@ -0,0 +1,27 @@
+(\ zero one two three succ plus mult pred minus isZero .
+
+    pred two
+    -- Should evaluate to zero, i.e., \ f x . f x
+)
+
+-- zero
+(\ f x . x)
+-- one
+(\ f x . f x)
+-- two
+(\ f x . f (f x))
+-- three
+(\ f x . f (f (f x)))
+
+-- succ
+(\n f x . f (n f x))
+-- plus
+(\m n f x . m f (n f x))
+-- mult
+(\m n f . m (n f))
+-- pred
+(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u))
+-- minus
+(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m)
+-- isZero
+(\ n . n (\ x . (\ x y . y)) (\ x y . x))
diff --git a/tests/examples/nums-pred-two.out b/tests/examples/nums-pred-two.out
new file mode 100644
index 0000000..7c032fd
--- /dev/null
+++ b/tests/examples/nums-pred-two.out
@@ -0,0 +1 @@
+(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . pred two) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x))
diff --git a/tests/examples/nums-pred-zero.lam b/tests/examples/nums-pred-zero.lam
new file mode 100644
index 0000000..dd0a17b
--- /dev/null
+++ b/tests/examples/nums-pred-zero.lam
@@ -0,0 +1,27 @@
+(\ zero one two three succ plus mult pred minus isZero .
+
+    pred zero
+    -- Should evaluate to zero, i.e., \ f x . x
+)
+
+-- zero
+(\ f x . x)
+-- one
+(\ f x . f x)
+-- two
+(\ f x . f (f x))
+-- three
+(\ f x . f (f (f x)))
+
+-- succ
+(\n f x . f (n f x))
+-- plus
+(\m n f x . m f (n f x))
+-- mult
+(\m n f . m (n f))
+-- pred
+(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u))
+-- minus
+(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m)
+-- isZero
+(\ n . n (\ x . (\ x y . y)) (\ x y . x))
diff --git a/tests/examples/nums-pred-zero.out b/tests/examples/nums-pred-zero.out
new file mode 100644
index 0000000..7f3455b
--- /dev/null
+++ b/tests/examples/nums-pred-zero.out
@@ -0,0 +1 @@
+(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . pred zero) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x))
diff --git a/tests/examples/nums-succ-two.lam b/tests/examples/nums-succ-two.lam
new file mode 100644
index 0000000..89f5761
--- /dev/null
+++ b/tests/examples/nums-succ-two.lam
@@ -0,0 +1,27 @@
+(\ zero one two three succ plus mult pred minus isZero .
+
+    succ two
+    -- Should evaluate to three, i.e., \ f x . f (f (f x))
+)
+
+-- zero
+(\ f x . x)
+-- one
+(\ f x . f x)
+-- two
+(\ f x . f (f x))
+-- three
+(\ f x . f (f (f x)))
+
+-- succ
+(\n f x . f (n f x))
+-- plus
+(\m n f x . m f (n f x))
+-- mult
+(\m n f . m (n f))
+-- pred
+(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u))
+-- minus
+(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m)
+-- isZero
+(\ n . n (\ x . (\ x y . y)) (\ x y . x))
diff --git a/tests/examples/nums-succ-two.out b/tests/examples/nums-succ-two.out
new file mode 100644
index 0000000..3973621
--- /dev/null
+++ b/tests/examples/nums-succ-two.out
@@ -0,0 +1 @@
+(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . succ two) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x))
diff --git a/tests/examples/nums-succ-zero.lam b/tests/examples/nums-succ-zero.lam
new file mode 100644
index 0000000..28b0d8c
--- /dev/null
+++ b/tests/examples/nums-succ-zero.lam
@@ -0,0 +1,27 @@
+(\ zero one two three succ plus mult pred minus isZero .
+
+    succ zero
+    -- Should evaluate to one, i.e., (\ f x . f x)
+)
+
+-- zero
+(\ f x . x)
+-- one
+(\ f x . f x)
+-- two
+(\ f x . f (f x))
+-- three
+(\ f x . f (f (f x)))
+
+-- succ
+(\n f x . f (n f x))
+-- plus
+(\m n f x . m f (n f x))
+-- mult
+(\m n f . m (n f))
+-- pred
+(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u))
+-- minus
+(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m)
+-- isZero
+(\ n . n (\ x . (\ x y . y)) (\ x y . x))
diff --git a/tests/examples/nums-succ-zero.out b/tests/examples/nums-succ-zero.out
new file mode 100644
index 0000000..716960a
--- /dev/null
+++ b/tests/examples/nums-succ-zero.out
@@ -0,0 +1 @@
+(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . succ zero) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x))
diff --git a/tests/examples/omega-arg.lam b/tests/examples/omega-arg.lam
new file mode 100644
index 0000000..8a7138a
--- /dev/null
+++ b/tests/examples/omega-arg.lam
@@ -0,0 +1 @@
+(\a x . x) ((\z . z z) (\z . z z))
diff --git a/tests/examples/omega-arg.out b/tests/examples/omega-arg.out
new file mode 100644
index 0000000..33d80d7
--- /dev/null
+++ b/tests/examples/omega-arg.out
@@ -0,0 +1 @@
+(\a . \x . x) ((\z . z z) (\z . z z))
diff --git a/tests/examples/omega.lam b/tests/examples/omega.lam
new file mode 100644
index 0000000..29ed0ff
--- /dev/null
+++ b/tests/examples/omega.lam
@@ -0,0 +1,6 @@
+-- normal form              N
+-- weak normal form         N
+-- head normal form         N
+-- weak head normal form    N
+
+(\x . x x) (\x . x x)
diff --git a/tests/examples/omega.out b/tests/examples/omega.out
new file mode 100644
index 0000000..f7f18c2
--- /dev/null
+++ b/tests/examples/omega.out
@@ -0,0 +1 @@
+(\x . x x) (\x . x x)
diff --git a/tests/examples/pairs-fst-snd.lam b/tests/examples/pairs-fst-snd.lam
new file mode 100644
index 0000000..19791ad
--- /dev/null
+++ b/tests/examples/pairs-fst-snd.lam
@@ -0,0 +1,15 @@
+(\ pair fst snd .
+
+    fst (snd (pair (pair a b) (pair c d)))
+
+    -- Should reduce to c
+)
+
+-- pair
+(\ x y f . f x y)
+
+-- fst
+(\ p . p (\ x y . x))
+
+-- snd
+(\ p . p (\ x y . y))
diff --git a/tests/examples/pairs-fst-snd.out b/tests/examples/pairs-fst-snd.out
new file mode 100644
index 0000000..cb53fb8
--- /dev/null
+++ b/tests/examples/pairs-fst-snd.out
@@ -0,0 +1 @@
+(\pair . \fst . \snd . fst (snd (pair (pair a b) (pair c d)))) (\x . \y . \f . f x y) (\p . p (\x . \y . x)) (\p . p (\x . \y . y))
diff --git a/tests/examples/pairs-fst.lam b/tests/examples/pairs-fst.lam
new file mode 100644
index 0000000..5ee215a
--- /dev/null
+++ b/tests/examples/pairs-fst.lam
@@ -0,0 +1,15 @@
+(\ pair fst snd .
+
+    fst (pair a b)
+
+    -- Should reduce to a
+)
+
+-- pair
+(\ x y f . f x y)
+
+-- fst
+(\ p . p (\ x y . x))
+
+-- snd
+(\ p . p (\ x y . y))
diff --git a/tests/examples/pairs-fst.out b/tests/examples/pairs-fst.out
new file mode 100644
index 0000000..c11f799
--- /dev/null
+++ b/tests/examples/pairs-fst.out
@@ -0,0 +1 @@
+(\pair . \fst . \snd . fst (pair a b)) (\x . \y . \f . f x y) (\p . p (\x . \y . x)) (\p . p (\x . \y . y))
diff --git a/tests/examples/pairs-snd.lam b/tests/examples/pairs-snd.lam
new file mode 100644
index 0000000..b2f0a75
--- /dev/null
+++ b/tests/examples/pairs-snd.lam
@@ -0,0 +1,15 @@
+(\ pair fst snd .
+
+    snd (pair a b)
+
+    -- Should reduce to b
+)
+
+-- pair
+(\ x y f . f x y)
+
+-- fst
+(\ p . p (\ x y . x))
+
+-- snd
+(\ p . p (\ x y . y))
diff --git a/tests/examples/pairs-snd.out b/tests/examples/pairs-snd.out
new file mode 100644
index 0000000..ebfb43b
--- /dev/null
+++ b/tests/examples/pairs-snd.out
@@ -0,0 +1 @@
+(\pair . \fst . \snd . snd (pair a b)) (\x . \y . \f . f x y) (\p . p (\x . \y . x)) (\p . p (\x . \y . y))
diff --git a/tests/examples/weak-head-normal-form.lam b/tests/examples/weak-head-normal-form.lam
new file mode 100644
index 0000000..6b8c0e0
--- /dev/null
+++ b/tests/examples/weak-head-normal-form.lam
@@ -0,0 +1,6 @@
+-- normal form              N
+-- weak normal form         Y
+-- head normal form         Y
+-- weak head normal form    Y
+
+\f . f ((\x . x x) (\x . x x))
diff --git a/tests/examples/weak-head-normal-form.out b/tests/examples/weak-head-normal-form.out
new file mode 100644
index 0000000..6b4a7fc
--- /dev/null
+++ b/tests/examples/weak-head-normal-form.out
@@ -0,0 +1 @@
+\f . f ((\x . x x) (\x . x x))
diff --git a/tests/examples/weak-normal-form.lam b/tests/examples/weak-normal-form.lam
new file mode 100644
index 0000000..8d80a75
--- /dev/null
+++ b/tests/examples/weak-normal-form.lam
@@ -0,0 +1,6 @@
+-- normal form              N
+-- weak normal form         Y
+-- head normal form         N
+-- weak head normal form    Y
+
+\f . (\x . x x) (\x . x x)
diff --git a/tests/examples/weak-normal-form.out b/tests/examples/weak-normal-form.out
new file mode 100644
index 0000000..54963a1
--- /dev/null
+++ b/tests/examples/weak-normal-form.out
@@ -0,0 +1 @@
+\f . (\x . x x) (\x . x x)
diff --git a/tests/examples/y.lam b/tests/examples/y.lam
new file mode 100644
index 0000000..996802d
--- /dev/null
+++ b/tests/examples/y.lam
@@ -0,0 +1,7 @@
+-- normal form              N
+-- weak normal form         Y
+-- head normal form         N
+-- weak head normal form    Y
+
+-- Y combinator
+\ f . (\ x . f (x x)) (\ x . f (x x))
diff --git a/tests/examples/y.out b/tests/examples/y.out
new file mode 100644
index 0000000..afe09a5
--- /dev/null
+++ b/tests/examples/y.out
@@ -0,0 +1 @@
+\f . (\x . f (x x)) (\x . f (x x))
diff --git a/tests/runtests.sh b/tests/runtests.sh
new file mode 100755
index 0000000..75f1f3c
--- /dev/null
+++ b/tests/runtests.sh
@@ -0,0 +1,179 @@
+#!/usr/bin/env bash
+
+PLC="nix run"
+
+globallog=runtests.log
+rm -f $globallog
+error=
+keep=
+
+# Destination directory for generated files (log excepted)
+mkdir -p out
+
+# Set time limit
+ulimit -t 5
+
+Usage() {
+    echo "Usage: runtests.sh [options] [files]"
+    echo "-k    Keep intermediate files"
+    echo "-h    Print this help"
+    exit 1
+}
+
+# NoteGen <filename>
+# Remember that the given filename was generated so we can clean up
+NoteGen() {
+  generatedfiles="$generatedfiles $1"
+}
+
+SignalError() {
+    if [ -z "$error" ] ; then
+        echo "FAILED"
+        error=1
+    fi
+    echo "  $1"
+}
+
+# Compare <outfile> <reffile> <difffile>
+# Compares the outfile with reffile.  Differences, if any, written to difffile
+Compare() {
+    NoteGen "$3"
+    if ! [ -f "$2" ] ; then
+      SignalError "$2 not found"	
+      echo "$2 not found" 1>&2
+    else
+	echo diff -b $1 $2 ">" $3 1>&2
+	diff -b "$1" "$2" > "$3" 2>&1 || {
+	    SignalError "$1 differs"
+	    echo "FAILED $1 differs from $2" 1>&2
+	    cat $3 >&2
+	}
+    fi
+}
+
+# Run <args>
+# Report the command, run it, and report any errors
+Run() {
+    echo $* 1>&2
+    eval $* || {
+	SignalError "failed: $*"
+	return 1
+    }
+}
+
+# RunFail <args>
+# Report the command, run it, and expect an error
+RunFail() {
+    echo $* 1>&2
+    eval $* && {
+	SignalError "failed: $* did not report an error"
+	return 1
+    }
+    return 0
+}
+
+# Run the parser on the given file
+Check() {
+    error=
+    basename=`basename $1 | sed 's/[.][^.]*$//'`
+    reffile=`echo $1 | sed 's/[.][^.]*$//'`
+    basedir=`dirname $1`
+
+    echo -n "$basename..."
+
+    echo 1>&2
+    echo "###### Testing $basename" 1>&2
+
+    generatedfiles=
+
+    # Run the parser
+    result="out/${basename}.out"
+    reference="${reffile}.out"
+    diff="out/${basename}.diff"
+    NoteGen "${result} ${diff}"
+    
+    Run $PLC "<" "$1" ">" "${result}" &&
+    Compare "${result}" "${reference}" "${diff}"
+
+    if [ -z "$error" ] ; then
+	if [ -z "$keep" ] ; then
+	    rm -f $generatedfiles
+	fi
+	echo "OK"
+	echo "###### SUCCESS" 1>&2
+    else
+	echo "###### FAILED" 1>&2
+	globalerror=$error
+    fi
+}
+
+# Run the compiler and expect an error
+CheckFail() {
+    error=
+    basename=`basename $1 | sed 's/[.][^.]*$//'`
+    reffile=`echo $1 | sed 's/[.][^.]*$//'`
+    basedir=`dirname $1`
+
+    echo -n "$basename..."
+
+    echo 1>&2
+    echo "###### Testing failure $basename" 1>&2
+
+    generatedfiles=
+
+    # Run the parser
+
+    parsed="out/${basename}.lam"
+    difffile="out/${basename}.diff"
+    NoteGen "${parsed} ${difffile}"
+    RunFail $PLC "<" "$1" ">" "${parsed}" "2>" "${errfile}" &&
+    Compare "${errfile}" "${reffile}.err" "${difffile}"
+
+    # Report the status and clean up the generated files
+
+    if [ -z "$error" ] ; then
+	if [ -z "$keep" ] ; then
+	    rm -f $generatedfiles
+	fi
+	echo "OK"
+	echo "###### SUCCESS" 1>&2
+    else
+	echo "###### FAILED" 1>&2
+	globalerror=$error
+    fi
+}
+
+while getopts kh c; do
+    case $c in
+	k) # Keep intermediate files
+	    keep=1
+	    ;;
+	h) # Help
+	    Usage
+	    ;;
+    esac
+done
+
+shift `expr $OPTIND - 1`
+
+if [ $# -ge 1 ]
+then
+    files=$@
+else
+    files="examples/*.lam"
+fi
+
+for file in $files
+do
+  case "$file" in
+    *-fail.lam)
+	  CheckFail "$file" 2>> $globallog
+	  ;;
+    *)
+	  Check "$file" 2>> $globallog
+	  ;;
+  esac    
+done
+
+exit $globalerror
+