compUtil UTΒΆ

computation.spad line 2260

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])