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