compUtil UT¶

macro to simplify output

coerce: Lambda UT -> SKICombinators UT: coerce Lambda term to SKI combinators. this process is known as abstraction elimination. it is done by applying the following rules until all lambda terms have been eliminated. rule LS1: Lam[x] => x rule LS2: Lam[(E1 E2)] => (Lam[E1] Lam[E2]) rule LS3: Lam[\x.E] => (K Lam[E]) (if x does not occur free in E) rule LS4: Lam[\x.x] => I rule LS5: Lam[\x.y.E] => Lam[\x.Lam[y.E]] (if x occurs free in E) rule LS6: Lam[\x.(E1 E2)] => (S Lam[\x.E1] Lam[\x.E2])

coerce: SKICombinators UT -> ILogic: coerce combinators to intuitionistic logic this is known as the Curry-Howard isomorphism it uses the following rules: rule SI1: Ski[Kab] => a -> (b -> a), rule SI2: Ski[Sabc] => (a -> (b -> c)) -> ((a -> b) -> (a -> c)), rule SI3: Ski[a a->b] => b the last rule is function application (modus ponens)

coerce: SKICombinators UT -> Lambda UT: coerce SKI combinators to Lambda term. this conversion is done by applying the following rules rule SL1: Ski[I] = \x.0 rule SL2: Ski[K] = \x.y.1 rule SL3: Ski[S] = \x.y.\z.(2 0 (1 0)) rule SL4: Ski[(E1 E2)] = (Ski[E1] Ski[E2])