-- Uebungen zur Gleichungslogik, WS 2006,07
-- Loesung für Uebungsblatt 10, Aufgabe 4
--
-- 14.12.2006 N.S

--
-- Bitte ergaenzen Sie die fehlenden Programmstuecke
--

--
-- Mengenoperationen auf Listen
--

member x [] = False
member x (y:ys) = ((x == y) || member x ys)

ins xs x = if member x xs then xs else (x:xs)
remove xs x  = filter (\y -> x /= y) xs
 
union xs ys = foldl ins xs ys

--
-- variant x xs: liefert eine Variante des Strings x die nicht in der
-- Menge xs vorkommt.
--

variant :: String -> [String] -> String
variant x xs  = head [x'| x' <- iterate (\x -> x ++ "'") x, not (member x' xs)]

--
-- Lambda Terme
--
data Term = Const String | Var String | Appl Term Term | Abs String Term

--
-- frees t: Die freien Variablen in Term t
--
frees :: Term -> [String] 

--
-- subst x t u: Substitution von Variable x durch Term t in Term u
--
subst :: String -> Term -> Term -> Term

--
-- eval t: Auswertung von Term t
--   
eval :: Term -> Term




--
-- Beispiele
--
f x = Appl (Const "f") x

x = Var "x"
y = Var "y"
z = Var "z"

c = Const "c"
d = Const "d"
e = Const "e"


 
self = (Abs "x" (Appl x x))
omega = Appl self self
i = Abs "x" x
k = Abs "x" (Abs "y" x)
s = Abs "x" (Abs "y" (Abs "z" (Appl (Appl x z) (Appl y z))))


t1 = Appl (Abs "x" (Abs "y" x)) y
t2 = Appl (Abs "x" (Appl (Var "x") (Var "x'"))) (Var "x")
t3 = Appl (Appl k c) omega
-- Warum terminiert eval t3 obwohl eval omega nicht terminiert?

t4 = Appl (Abs "x" (Appl (f x) x)) (Const "5")
t5 = Appl (Abs "x" x) (Abs "x" x)
t6 = Appl x (Abs "y" y)
t7 = Appl self (Abs "x" (f x)) 
t8 = Appl (Appl (Appl s k) x) y
t9 = Appl (Appl (Appl s k) k) x
t10 = Appl (Abs "x" (Abs "y" (Appl x i))) (Abs "y" (Appl x y))
t11= Appl (Abs "x" (Appl (Abs "y" (Appl x y)) c)) (Appl i d)