# compUtil UTΒΆ

computation.spad line 2259 [edit on github]

UT: VarCat

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`

])