Studieren Sie das Aufgaben-Papier zum Lambda-Kalkül und lösen Sie die dort enthaltenen Aufgaben.
> module LambdaCalculus where
> import Data.List
> data Lambda =
> Var String
> |App Lambda Lambda
> |L String Lambda
> deriving (Show,Eq)
> id = L "x" (Var "x")
> true = L "x" (L "y" (Var "x"))
> false = L "x" (L "y" (Var "y"))
> wenn = L "c"$L"a_1"$L "a_2"$ App (App (Var "c")(Var "a_1"))(Var "a_2")
> app = foldl1 App
> w1 = app [wenn,true,Var "x",Var "y"]
> w2 = app [wenn,false,Var "x",Var "y"]
> class ToLaTeX a where
> toLaTeX :: a -> String
> instance ToLaTeX Lambda where
> toLaTeX (Var x) = x
> toLaTeX (App e1 e2) = "("++toLaTeX e1++"$ $ "++toLaTeX e2++")"
> toLaTeX (L x e) = "\n\\lambda "++x++".$ $"++toLaTeX e
> instance (ToLaTeX a) => ToLaTeX [a] where
> toLaTeX es
> = "\n\\tiny "++intercalate "\n\n " ["$"++toLaTeX e++"$\\\\\n"|e<-es]
> ++"\n\\normalsize "
> freeVars :: Lambda -> [String]
> freeVars l = []
> sub x1 arg v@(Var x2)
> |x1==x2 = arg
> |otherwise = v
> sub x arg (App e1 e2) = App (sub x arg e1)(sub x arg e2)
> sub x1 arg l@(L x2 body)
> |x1==x2 = l
> |x2 `elem` (freeVars arg)
> = let (newVar:_) = freshVars (App body arg)
> in L newVar (sub x1 arg (sub x2 (Var newVar) body))
> |otherwise = (L x2 (sub x1 arg body))
> allVars = ["x_{"++show n++"}"|n<-[1,2..]]
> freshVars e = [v|v<-allVars,not (v `elem` freeVars e)]
> reduce :: Lambda -> (Bool, Lambda)
> reduce l@(App (L x body) arg) = (False,l)
> reduce l@(App e1 e2) = (False,l)
> reduce l@(L x body) = (False,l)
> reduce l@(Var x) = (False,l)
> reduction e = map snd$takeWhile fst$iterate (reduce.snd) (True,e)
> normalForm = last.reduction
> n0= L "f"$L "x" (Var "x")
> n1= L "f"$L "x" (App (Var "f")(Var "x"))
> n2= L "f"$L "x" (App (Var "f")(App (Var "f")(Var "x")))
> n3= L "f"$L "x" (App (Var "f")(App (Var "f")(App (Var "f")(Var "x"))))
> n n= L "f"$L "x" $numberApp n
> numberApp 0 = Var "x"
> numberApp n = App (Var "f")(numberApp (n-1))
> isZero :: Lambda
> isZero = (Var "n")
> succc :: Lambda
> succc = (Var "n")
> predd :: Lambda
> predd = (Var "n")
> add :: Lambda
> add = (Var "n")
> mult :: Lambda
> mult = (Var "n")
> y :: Lambda
> y = Var "x"
> facAux =
> L"h"$L"n"$
> app [wenn
> ,App isZero (Var "n")
> ,n 1
> ,app [mult,Var "n",App (Var "h") (App predd (Var "n"))]]
> factorial = App y facAux
> ex = writeFile "example.tex" $toLaTeX $reduction (App factorial n2)
Subato
