zhaw-fup/Exercises/exercise-7/Lambda.hs

90 lines
1.9 KiB
Haskell

import Data.Set (Set, empty, delete, union, singleton)
--------------------
-- 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 param term) -> "L" ++ param ++ "." ++ pretty term
(Inv func param) -> "(" ++ pretty func ++ " " ++ pretty param ++ ")"
(Var name) -> name
Add -> "Add"
Nat value -> show value
-- example
-- >>> pretty (Abs "x" $ Abs "y" $ Inv (Inv Add (Var "x")) (Var "y"))
-- "Lx.Ly.((Add x) y)"
freeVars :: Term -> Set String
freeVars x = case x of
(Abs param term) -> delete param (freeVars term)
(Inv func param) -> freeVars func `union` freeVars param
(Var name) -> singleton name
_ -> empty
-- example
-- >>> freeVars (Inv (Var "y") $ Abs "x" Add)
-- fromList ["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)