2 files changed, 162 insertions, 0 deletions
diff --git a/LambdaCalc.hs b/LambdaCalc.hs
new file mode 100644
index 0000000..c733617
--- /dev/null
+++ b/LambdaCalc.hs
@@ -0,0 +1,158 @@
+module LambdaCalc where
+
+import Data.Char (isSpace)
+
+data Term = Variable String
+          | Abstraction Term Term
+          | Application Term Term
+          deriving (Eq)
+
+instance Show Term where
+  show (Variable s) = s
+
+  show (Abstraction varName body) = '\x03BB':show varName ++ '.':show body
+
+  show (Application x y) = x' ++ ' ':y'
+    where
+      x' = if isAbstraction x then '(':show x ++ ")" else show x
+      y' = if isVariable y then show y else '(':show y ++ ")"
+
+var :: String -> Term
+var "" = error "cannot name a variable with an empty string"
+var s
+  | any ( \c -> isSpace c || c `elem` "().\x03BB") s = error "name has forbidden characters"
+  | otherwise = Variable s
+
+lambda :: String -> Term -> Term
+lambda s t = Abstraction (var s) t
+
+apply :: Term -> Term -> Term
+apply = Application
+
+infixl 6 <+>
+(<+>) :: Term -> Term -> Term
+(<+>) = apply
+
+-- same as apply or <+>, but also beta reduces the result
+infixl 6 <++>
+(<++>) :: Term -> Term -> Term
+x <++> y = betaReduce $ x <+> y
+
+isVariable :: Term -> Bool
+isVariable (Variable _) = True
+isVariable _            = False
+
+isAbstraction :: Term -> Bool
+isAbstraction (Abstraction _ _) = True
+isAbstraction _                 = False
+
+isApplication :: Term -> Bool
+isApplication (Application _ _) = True
+isApplication _                 = False
+
+isNormal :: Term -> Bool
+isNormal (Variable _) = True
+isNormal (Abstraction _ b) = isNormal b
+isNormal (Application x y) = not (isAbstraction x) && isNormal x && isNormal y
+
+betaStep :: Term -> Term
+betaStep (Variable v)         = Variable v
+betaStep (Abstraction v body) = Abstraction v $ betaStep body
+betaStep (Application x y)
+  | isAbstraction x           = deAbstract x y
+  | otherwise                 = Application (betaStep x) (betaStep y)
+
+betaPath :: Term -> [Term]
+betaPath e
+  | isNormal e = [e]
+  | otherwise  = e:betaPath (betaStep e) 
+
+betaReduce :: Term -> Term
+betaReduce = last . betaPath
+
+deAbstract :: Term -> Term -> Term
+deAbstract (Abstraction v body) arg = go body
+  where
+    go v'@(Variable _)
+      | v == v'          = arg
+      | otherwise        = v'
+    go a@(Abstraction v' body')
+      | v == v'          = a
+      | otherwise        = Abstraction v' $ go body'
+    go (Application x y) = Application (go x) (go y)
+deAbstract _ _ = error "deAbstract: first argument must an abstraction"
+
+{- Common combinators -}
+
+combI :: Term
+combI = lambda "x" $ var "x"
+
+identity :: Term
+identity = combI
+
+combK :: Term
+combK = lambda "a" $ lambda "b" $ var "a"
+
+constant :: Term
+constant = combK
+
+combKI :: Term
+combKI = lambda "a" $ lambda "b" $ var "b"
+
+combB :: Term
+combB = lambda "f" $ lambda "g" $ lambda "a" body
+  where
+    body = var "f" <+> (var "g" <+> var "a")
+
+compose :: Term
+compose = combB
+
+combC :: Term
+combC = lambda "f" $ lambda "a" $ lambda "b" $ var "f" <+> var "b" <+> var "a"
+
+{- Boolean values and operations -}
+
+-- assumes valid input
+fromBool :: Term -> Bool
+fromBool e = case e <++> var "_TRUE" <++> var "_FALSE" of
+  Variable "_TRUE"  -> True
+  Variable "_FALSE" -> False
+  _                 -> error "could not recognize lambda expression as boolean"
+
+bTrue :: Term
+bTrue = lambda "x" $ lambda "y" $ var "x"
+
+bFalse :: Term
+bFalse = lambda "x" $ lambda "y" $ var "y"
+
+bNot :: Term
+bNot = lambda "b" $ var "b" <++> bFalse <++> bTrue
+
+bOr :: Term
+bOr = lambda "p" $ lambda "q" body
+  where
+    body = var "p" <++> var "p" <++> var "q"
+
+bAnd :: Term
+bAnd = lambda "p" $ lambda "q" body
+  where
+    body = var "p" <++> var "q" <++> var "p"
+
+bEq :: Term
+bEq = lambda "p" $ lambda "q" body
+  where
+    body = var "p" <++> var "q" <++> (bNot <++> var "q")
+
+bXor :: Term
+bXor = lambda "p" $ lambda "q" body
+  where
+    body = var "p" <++> (bNot <++> var "q") <++> var "q"
+
+bImplies :: Term
+bImplies = lambda "p" $ lambda "q" body
+  where
+    body = var "p" <++> var "q" <++> bTrue
+
+bConverse :: Term
+bConverse = combC <++> bImplies
+
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..8339740
--- /dev/null
+++ b/README.md
@@ -0,0 +1,4 @@
+# A Lambda Calculus implementation in Haskell
+
+What it says on the tin.
+