add homework material

80 files changed, 1286 insertions, 0 deletions

diff --git a/.envrc b/.envrc
new file mode 100644
index 0000000..3550a30
--- /dev/null
+++ b/.envrc
@@ -0,0 +1 @@
+use flake
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..82d9aa7
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,5 @@
+.direnv
+result
+*.pdf
+tests/runtests.log
+tests/out
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..9195860
--- /dev/null
+++ b/README.md
@@ -0,0 +1,66 @@
+# Lambda Calculus Expressions
+
+## Building
+
+Use the Haskell Tool Stack [https://www.haskellstack.org]
+
+`stack build`
+
+## Testing
+
+```
+cd tests
+./runtests.sh
+beta1...OK
+beta2...OK
+beta3...OK
+```
+
+## Use
+
+```
+stack ghci
+ghci> parse "x y z"
+x y z
+ghci> parse "(\\ n . pred n) 3"
+(\n . pred n) 3
+ghci> parse "x (y z)"
+x (y z)
+ghci> parse "(x y) z"
+x y z
+ghci> parse "\\x.y z"
+\x . y z
+ghci> parse "\\x y z . x (y z)"
+\x . \y . \z . x (y z)
+ghci> parse "\\x.x (\\z . z)"
+\x . x (\z . z)
+ghci> parse "(\\x.x) (\\z . z)"
+(\x . x) (\z . z)
+ghci> :i Expr
+type Expr :: *
+data Expr = Var String | Lam String Expr | App Expr Expr
+instance Show Expr
+ghci> Lam "a" (App (Var "b") (Var "c"))
+\a . b c
+```
+
+# Syntax
+
+```
+<expr>  ::= <id>                  -- variable
+          | `\' <id>+ `.' <expr>  -- lambda abstraction
+          | <expr> <expr>         -- application
+          | `(' <expr> `)'        -- grouping
+```
+
+Variable identifiers are any sequence of characters excluding
+`\`, `.`, `(`, `)`, `-`, and whitespace
+
+Lambda abstractions are at the lowest precedence;
+application binds left-to-right
+
+Space is needed to separate identifiers but is optional elsewhere
+
+Single-line comments start with `--`
+
+Multi-line comments are between `{-` and `-}' and may nest
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
index 0000000..9a994af
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 0000000..fe99fdd
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,83 @@
+{
+  "nodes": {
+    "flake-parts": {
+      "inputs": {
+        "nixpkgs-lib": [
+          "nixpkgs"
+        ]
+      },
+      "locked": {
+        "lastModified": 1680392223,
+        "narHash": "sha256-n3g7QFr85lDODKt250rkZj2IFS3i4/8HBU2yKHO3tqw=",
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "rev": "dcc36e45d054d7bb554c9cdab69093debd91a0b5",
+        "type": "github"
+      },
+      "original": {
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1681358109,
+        "narHash": "sha256-eKyxW4OohHQx9Urxi7TQlFBTDWII+F+x2hklDOQPB50=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "96ba1c52e54e74c3197f4d43026b3f3d92e83ff9",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "nixpkgs-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs_2": {
+      "locked": {
+        "lastModified": 1680945546,
+        "narHash": "sha256-8FuaH5t/aVi/pR1XxnF0qi4WwMYC+YxlfdsA0V+TEuQ=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "d9f759f2ea8d265d974a6e1259bd510ac5844c5d",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-parts": "flake-parts",
+        "nixpkgs": "nixpkgs",
+        "treefmt-nix": "treefmt-nix"
+      }
+    },
+    "treefmt-nix": {
+      "inputs": {
+        "nixpkgs": "nixpkgs_2"
+      },
+      "locked": {
+        "lastModified": 1681115235,
+        "narHash": "sha256-VCETW6vOzNlByc0A5gTJoFE9L/ikP91rX6XynBUgIno=",
+        "owner": "numtide",
+        "repo": "treefmt-nix",
+        "rev": "f3dd071be31528261034022020fc7e4c010f7179",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "treefmt-nix",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000..b32c2ca
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,33 @@
+{
+  inputs = {
+    nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable";
+    flake-parts = { url = "github:hercules-ci/flake-parts"; inputs.nixpkgs-lib.follows = "nixpkgs"; };
+    treefmt-nix.url = "github:numtide/treefmt-nix";
+  };
+
+  outputs = inputs:
+    inputs.flake-parts.lib.mkFlake { inherit inputs; } {
+      systems = [ "x86_64-linux" ];
+      imports = [
+        inputs.treefmt-nix.flakeModule
+      ];
+
+      perSystem = { pkgs, ... }: {
+        packages.default = pkgs.haskellPackages.callCabal2nix "example" ./. { };
+
+        devShells.default = pkgs.haskellPackages.shellFor {
+          packages = ps: [ ];
+          buildInputs = with pkgs.haskellPackages; [
+            cabal-install
+            haskell-language-server
+	    megaparsec
+          ];
+        };
+        treefmt = {
+          projectRootFile = "flake.nix";
+          programs.nixpkgs-fmt.enable = true;
+          programs.cabal-fmt.enable = true;
+        };
+      };
+    };
+}
diff --git a/lambda.cabal b/lambda.cabal
new file mode 100644
index 0000000..68d5068
--- /dev/null
+++ b/lambda.cabal
@@ -0,0 +1,49 @@
+cabal-version:      1.12
+
+-- This file has been generated from package.yaml by hpack version 0.35.1.
+--
+-- see: https://github.com/sol/hpack
+
+name:               lambda
+version:            0.1.0.0
+author:             John Hui, Stephen Edwards
+maintainer:         sedwards@cs.columbia.edu
+copyright:          2023 John Hui and Stephen Edwards
+license:            BSD3
+build-type:         Simple
+extra-source-files: README.md
+
+library
+  exposed-modules:
+    AST
+    HW
+    Parse
+
+  other-modules:    Paths_lambda
+  hs-source-dirs:   src
+  ghc-options:
+    -Wall -Wcompat -Widentities -Wincomplete-record-updates
+    -Wincomplete-uni-patterns -Wmissing-export-lists
+    -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints
+
+  build-depends:
+      base        >=4.7 && <5
+    , containers
+    , megaparsec
+
+  default-language: Haskell2010
+
+executable plc
+  main-is:          Main.hs
+  other-modules:    Paths_lambda
+  hs-source-dirs:   plc
+  ghc-options:
+    -Wall -Wcompat -Widentities -Wincomplete-record-updates
+    -Wincomplete-uni-patterns -Wmissing-export-lists
+    -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints
+
+  build-depends:
+      base    >=4.7 && <5
+    , lambda
+
+  default-language: Haskell2010
diff --git a/package.yaml b/package.yaml
new file mode 100644
index 0000000..deb4306
--- /dev/null
+++ b/package.yaml
@@ -0,0 +1,36 @@
+name:                lambda
+version:             0.1.0.0
+license:             BSD3
+author:              "John Hui, Stephen Edwards"
+maintainer:          "sedwards@cs.columbia.edu"
+copyright:           "2023 John Hui and Stephen Edwards"
+
+extra-source-files:
+- README.md
+
+dependencies:
+- base >= 4.7 && < 5
+
+ghc-options:
+- -Wall
+- -Wcompat
+- -Widentities
+- -Wincomplete-record-updates
+- -Wincomplete-uni-patterns
+- -Wmissing-export-lists
+- -Wmissing-home-modules
+- -Wpartial-fields
+- -Wredundant-constraints
+
+library:
+  source-dirs: src
+  dependencies:
+  - megaparsec
+  - containers
+  
+executables:
+  plc:
+    main: Main.hs
+    source-dirs: plc
+    dependencies:
+    - lambda
diff --git a/plc/Main.hs b/plc/Main.hs
new file mode 100644
index 0000000..9e8a7b8
--- /dev/null
+++ b/plc/Main.hs
@@ -0,0 +1,8 @@
+module Main (main) where
+
+import Parse
+
+main :: IO ()
+main = do
+  s <- getContents
+  print $ parse s
diff --git a/src/AST.hs b/src/AST.hs
new file mode 100644
index 0000000..456338e
--- /dev/null
+++ b/src/AST.hs
@@ -0,0 +1,28 @@
+-- | Abstract syntax tree for the untyped lambda calculus, plus some helpers.
+module AST (
+  Expr (..)
+) where
+
+-- | Lambda Expressions
+data Expr
+  = Var String
+  | Lam String Expr
+  | App Expr Expr
+  deriving (Eq, Ord)
+
+
+-- https://www.haskellforall.com/2020/11/pretty-print-syntax-trees-with-this-one.html
+showLam, showApp, showVar :: Expr -> String
+showLam (Lam i e) = "\\" ++ i ++ " . " ++ showLam e
+showLam e = showApp e
+
+showApp (App e1 e2) = showApp e1 ++ " " ++ showVar e2
+showApp e = showVar e
+
+showVar (Var i) = i
+showVar e = "(" ++ showLam e ++ ")"
+
+instance Show Expr where
+  show e = showLam e
+
+
diff --git a/src/HW.hs b/src/HW.hs
new file mode 100644
index 0000000..88fb1c2
--- /dev/null
+++ b/src/HW.hs
@@ -0,0 +1,50 @@
+module HW
+  ( fv
+  , subst
+  , normalstep
+  , pickFresh
+  , repeatedly 
+  , printnormal
+  ) where
+
+import AST
+import qualified Data.Set as Set
+import Parse (parse)
+
+-- | Return the free variables in an expression
+fv :: Expr -> Set.Set String
+fv _ = Set.singleton "UNIMPLEMENTED" -- Replace with your solution to problem 1
+
+
+
+-- | Substitute n for x in e, avoiding name capture
+--    subst n x e     e[x := n]
+subst :: Expr -> String -> Expr -> Expr
+subst _ _ _ = Var "UNIMPLEMENTED" -- Replace with your solution to problem 2
+
+
+
+-- | Take a single step in normal order reduction or return Nothing
+normalstep :: Expr -> Maybe Expr
+normalstep _ = Just (Var "UNIMPLEMENTED") -- Replace with your solution to problem 3
+
+
+
+
+-- | Return a "fresh" name not already in the set.
+-- Tries x' then x'', etc.
+pickFresh :: Set.Set String -> String -> String
+pickFresh s = pickFresh'
+  where pickFresh' n | n `Set.notMember` s = n
+        pickFresh' n                       = pickFresh' $ n ++ "'"
+               
+-- | Repeatedly apply a function to transform a value, returning the list
+-- of steps it took.  The result list starts with the given initial value
+repeatedly :: (a -> Maybe a) -> a -> [a]
+repeatedly f = repeatedly'
+  where repeatedly' x = x : case f x of Nothing -> []
+                                        Just y -> repeatedly' y
+
+-- | Print out the series of normal order reduction steps
+printnormal :: String -> IO ()
+printnormal = mapM_ print . repeatedly normalstep . parse
diff --git a/src/Parse.hs b/src/Parse.hs
new file mode 100644
index 0000000..748bd98
--- /dev/null
+++ b/src/Parse.hs
@@ -0,0 +1,91 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# OPTIONS_GHC -Wno-unused-top-binds #-}
+
+-- | Parser for the untyped lambda calculus, whose AST is defined in "AST".
+module Parse (parse, tryParse) where
+
+import qualified AST as A
+
+import Text.Megaparsec (
+  MonadParsec (..),
+  Parsec,
+  errorBundlePretty,
+  noneOf,
+  runParser,
+  some,
+  (<?>),
+  (<|>),
+  between
+ )
+import Text.Megaparsec.Char( space1 )
+import qualified Text.Megaparsec.Char.Lexer as L
+
+import Control.Monad (void)
+import Data.Bifunctor (Bifunctor (..))
+import Data.Void (Void)
+
+-- * Exposed functions
+
+-- | Parse a Lambda expression; throw an exception over an error
+parse :: String -> A.Expr
+parse = either error id . tryParse
+
+-- | Parse some code 'String' into an 'L.Expr' or an error message.
+tryParse :: String -> Either String A.Expr
+tryParse = first errorBundlePretty .
+           runParser (pSpace >> pExpr <* eof) "<input>"
+
+{- * Expression parser
+
+Note that Megaparsec allows us to label tokens with 'label' or '(<?>)', which
+helps it produce human-readable error messages.
+-}
+
+-- | Entry point for parser.
+pExpr :: Parser A.Expr
+pExpr = pBody <?> "expression"
+
+-- | Parse expressions at the lowest level of precedence, i.e., lambdas.
+pBody :: Parser A.Expr
+pBody = pLam <|> pApp
+ where
+  pLam = do
+    pToken "\\"
+    bs <- some pIdent <?> "lambda binders"
+    pToken "."
+    body <- pBody <?> "lambda body"
+    return $ foldr A.Lam body bs
+
+-- | Parse juxtaposition as application.
+pApp :: Parser A.Expr
+pApp = foldl1 A.App <$> some pAtom <?> "term application"
+
+-- | Parse expressions at the highest precedence, including parenthesized terms
+pAtom :: Parser A.Expr
+pAtom = A.Var <$> pVar <|> pParens pExpr
+ where
+  pVar = pIdent <?> "variable"
+
+-- * Megaparsec boilerplate and helpers
+
+-- | Parsing monad.
+type Parser = Parsec Void String
+
+-- | Parse an identifier, possible surrounded by spaces
+pIdent :: Parser String
+pIdent = L.lexeme pSpace (some $ noneOf ['\\','.','(',')',' ','\n','\r','\t','-'])
+
+-- | Consume a token defined by a string, possibly surrounded by spaces
+pToken :: String -> Parser ()
+pToken = void . L.symbol pSpace
+
+-- | Parse some element surrounded by parentheses.
+pParens :: Parser a -> Parser a
+pParens = between (pToken "(") (pToken ")")
+
+-- | Consumes whitespace and comments.
+pSpace :: Parser ()
+pSpace = label "whitespace" $ L.space
+    space1
+    (L.skipLineComment "--")
+    (L.skipBlockCommentNested "{-" "-}")
diff --git a/stack.yaml b/stack.yaml
new file mode 100644
index 0000000..47f8c24
--- /dev/null
+++ b/stack.yaml
@@ -0,0 +1,67 @@
+# This file was automatically generated by 'stack init'
+#
+# Some commonly used options have been documented as comments in this file.
+# For advanced use and comprehensive documentation of the format, please see:
+# https://docs.haskellstack.org/en/stable/yaml_configuration/
+
+# Resolver to choose a 'specific' stackage snapshot or a compiler version.
+# A snapshot resolver dictates the compiler version and the set of packages
+# to be used for project dependencies. For example:
+#
+# resolver: lts-3.5
+# resolver: nightly-2015-09-21
+# resolver: ghc-7.10.2
+#
+# The location of a snapshot can be provided as a file or url. Stack assumes
+# a snapshot provided as a file might change, whereas a url resource does not.
+#
+# resolver: ./custom-snapshot.yaml
+# resolver: https://example.com/snapshots/2018-01-01.yaml
+resolver:
+  url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/20/13.yaml
+
+# User packages to be built.
+# Various formats can be used as shown in the example below.
+#
+# packages:
+# - some-directory
+# - https://example.com/foo/bar/baz-0.0.2.tar.gz
+#   subdirs:
+#   - auto-update
+#   - wai
+packages:
+- .
+# Dependency packages to be pulled from upstream that are not in the resolver.
+# These entries can reference officially published versions as well as
+# forks / in-progress versions pinned to a git hash. For example:
+#
+# extra-deps:
+# - acme-missiles-0.3
+# - git: https://github.com/commercialhaskell/stack.git
+#   commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a
+#
+# extra-deps: []
+
+# Override default flag values for local packages and extra-deps
+# flags: {}
+
+# Extra package databases containing global packages
+# extra-package-dbs: []
+
+# Control whether we use the GHC we find on the path
+# system-ghc: true
+#
+# Require a specific version of Stack, using version ranges
+# require-stack-version: -any # Default
+# require-stack-version: ">=2.9"
+#
+# Override the architecture used by Stack, especially useful on Windows
+# arch: i386
+# arch: x86_64
+#
+# Extra directories used by Stack for building
+# extra-include-dirs: [/path/to/dir]
+# extra-lib-dirs: [/path/to/dir]
+#
+# Allow a newer minor version of GHC than the snapshot specifies
+# compiler-check: newer-minor
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
+