77 lines
1.5 KiB
Haskell
77 lines
1.5 KiB
Haskell
--------------------
|
|
-- Slides
|
|
--------------------
|
|
|
|
data Term =
|
|
Nat Integer
|
|
| Abs String Term -- EAbs Abstraction
|
|
| Inv Term Term -- EApp Invocation (a.k.a. Application) of a function
|
|
| Var String -- EVar a variable
|
|
| Add
|
|
|
|
pretty x = case x of
|
|
(Abs name term) -> "L" ++ name ++ "." ++ pretty term
|
|
(Inv func param) -> "(" ++ pretty func ++ " " ++ pretty param ++ ")"
|
|
(Var name) -> name
|
|
Add -> "Add"
|
|
|
|
-- example
|
|
-- >>> pretty (Abs "x" $ Abs "y" $ Inv (Inv Add (Var "x")) (Var "y"))
|
|
-- "Lx.Ly.((Add x) y)"
|
|
|
|
--------------------
|
|
-- Exercise 1
|
|
--------------------
|
|
-- Ja
|
|
-- Nein
|
|
-- Ja
|
|
-- Nein
|
|
|
|
--------------------
|
|
-- Exercise 2
|
|
--------------------
|
|
-- Rule 1: Function bodies in (L{param}.{body}) span as much as possible:
|
|
-- Lx.A B C == Lx.(A B C)
|
|
-- Rule 2: Function invocations (application) are left bound
|
|
-- A B C == ((A B) C)
|
|
|
|
-- ((Lx.(x z)) (Ly.(x y)))
|
|
-- ((Lx.(x z)) (Ly.(w (Lw.(((w y) z) x)))))
|
|
-- (Lx.((x y) (Lx.(y x))))
|
|
|
|
--------------------
|
|
-- Exercise 3
|
|
--------------------
|
|
-- (Lx.((x *z*) (Ly.(x y))))
|
|
-- ((Lx.(x *z*)) Ly.(*w* (Lw.(((w y) *z*) *x*))))
|
|
-- Lx.((x "y") (Lx.("y" x)))
|
|
|
|
--------------------
|
|
-- Exercise 4
|
|
--------------------
|
|
----------
|
|
-- 1.)
|
|
----------
|
|
-- (((Lz.z) (Ly.yy)) (Lx.xa))
|
|
-- ((Ly.yy) (Lx.xa))
|
|
-- (Lx.xa (Lx.xa))
|
|
-- (Lx.xa) a
|
|
-- (a a)
|
|
|
|
----------
|
|
-- 2.)
|
|
----------
|
|
-- (Lx.(x x))(Ly.(y x)) z
|
|
-- (Ly.(y x)) (Ly.(y x)) z
|
|
-- ((Ly.(y x)) x) z
|
|
-- (x x) z
|
|
-- x x z
|
|
|
|
----------
|
|
-- 3.)
|
|
----------
|
|
-- ((Lx.(x x))(Ly.y))(Ly.y)
|
|
-- ((Ly.y Ly.y))(Ly.y)
|
|
-- (Ly.y)(Ly.y)
|
|
-- (Ly.y)
|