Adding LambdaCalculator library and Parser

This code was stored locally and now is available on this GitHub repo

LambdaCalculus.hs

@@ -0,0 +1,10 @@
+module LambdaCalculus where
+
+infixl 2 :@
+
+type Symb = String 
+
+data Expr = Var Symb
+          | Expr :@ Expr
+          | Lam Symb Expr
+          deriving (Eq)

Main.hs

@@ -0,0 +1,12 @@
+module Main where
+
+
+import LambdaCalculus
+import Methods
+import Parser
+
+
+
+main :: IO ()
+main = do
+    putStrLn "Lambda calculator"

Methods.hs

@@ -0,0 +1,54 @@
+module Methods where
+
+
+import LambdaCalculus
+import Data.List
+
+infix  1 `alphaEq`
+infix  1 `betaEq`
+
+freeVars :: Expr -> [Symb]
+freeVars (Var v)   =  [v]
+freeVars (left :@ right)  = freeVars left `union` freeVars right
+freeVars (Lam var expr) = freeVars expr \\ [var]
+
+makeUnique :: Symb -> [Symb] -> [Symb] -> Symb
+makeUnique s symb1 symb2 | elem s symb1 || elem s symb2 = makeUnique (s ++ ['\'']) symb1 symb2
+                         | otherwise = s
+
+subst :: Symb -> Expr -> Expr -> Expr
+subst s e var@(Var v) | s == v = e
+                      | otherwise = var
+subst s e (left :@ right) = subst s e left :@ subst s e right
+subst s e lam@(Lam var expr) | var == s = lam
+                             | otherwise = if var `elem` freeVars e
+                                           then Lam l (subst s e (subst var (Var l) expr))
+                                           else Lam var (subst s e expr)
+                                             where l = makeUnique var (freeVars e) (freeVars expr)
+
+alphaEq :: Expr -> Expr -> Bool
+alphaEq (Var v1) (Var v2) = v1 == v2
+alphaEq (left1 :@ right1)  (left2 :@ right2)  = (left1 `alphaEq` left2) && (right1 `alphaEq` right2)
+alphaEq (Lam v1 e1) (Lam v2 e2) | v1 == v2 = e1 `alphaEq` e2
+                                | otherwise = notElem v1 (freeVars e2) && (e1 `alphaEq` subst v2 (Var v1) e2)
+alphaEq _ _ = False
+
+
+reduceOnce :: Expr -> Maybe Expr
+reduceOnce (Var _) = Nothing
+reduceOnce ((Lam v e) :@ right) = Just (subst v right e)
+reduceOnce (left :@ right) = case reduceOnce left of
+     Nothing -> case reduceOnce right of
+          Nothing -> Nothing
+          Just right' -> Just (left :@ right')
+     Just left' -> Just (left' :@ right)
+reduceOnce (Lam v e) = case reduceOnce e of
+     Nothing -> Nothing
+     Just e' -> Just (Lam v e')
+
+
+nf :: Expr -> Expr
+nf e = maybe e nf $ reduceOnce e
+
+betaEq :: Expr -> Expr -> Bool
+betaEq e1 e2 = nf e1 `alphaEq` nf e2

Parser.hs

@@ -0,0 +1,63 @@
+module Parser where
+
+import LambdaCalculus
+import Text.ParserCombinators.Parsec
+
+instance Show Expr where
+    show (Var v) = v
+    show (Var v1 :@ Var v2) = v1 ++ " " ++ v2
+    show (Var v :@ e) = v ++ " (" ++ show e ++ ")"
+    show (e1 :@ e2) = "(" ++ show e1 ++ ") (" ++ show e2 ++ ")"
+    show (Lam v e) = "\\" ++ v ++ " -> " ++ show e
+
+instance Read Expr where
+    readsPrec _ s = case parseStr s of
+        Left _  -> undefined
+        Right v -> [(v, "")]
+
+parseStr :: String -> Either ParseError Expr
+parseStr = parse (do
+    expr <- parseExpr
+    eof
+    return expr) ""
+
+parseId :: Parser String
+parseId = do
+    l <- letter
+    dig <- many alphaNum
+    _ <- spaces
+    return (l : dig)
+
+parseVar :: Parser Expr
+parseVar = Var <$> parseId
+
+parseExprInBrackets :: Parser Expr
+parseExprInBrackets = do
+    _ <- char '(' >> spaces
+    expr <- parseExpr
+    _ <- char ')' >> spaces
+    return expr
+
+parseExpr :: Parser Expr
+parseExpr = try parseTerm <|> try parseAtom
+
+parseAtom :: Parser Expr
+parseAtom = try parseLam <|> try parseVar <|> try parseExprInBrackets
+
+parseTerm :: Parser Expr
+parseTerm = parseAtom `chainl1` return (:@)
+
+parseLam :: Parser Expr
+parseLam = do
+    _ <- char '\\' >> spaces
+    ids <- many1 parseId
+    _ <- string "->" >> spaces
+    expr <- parseExpr
+    return $ foldr Lam expr ids
+
+{-
+(read "\\x1 x2 -> x1 x2 x2" :: Expr) == Lam "x1" (Lam "x2" (Var "x1" :@ Var "x2" :@ Var "x2"))
+
+cY = let {x = Var "x"; f = Var "f"; fxx = Lam "x" $ f :@ (x :@ x)} in Lam "f" $ fxx :@ fxx
+read (show cY) == cY
+-}