compUtil UTΒΆ

computation.spad line 2265 [edit on github]

The compUtil package provides utilities to convert between the computational domains: Lambda, Ski and ILogic. Both Lambda are Ski are Turing complete and can be coerced to each other. Lambda and Ski are not equal and they are only isomorphic up to beta-equivalence and beta-equivalence is undecidable so there is not a direct correspondence between the nodes in their trees. Also the names of bound variables and other such constructions may be lost in Lambda -> Ski -> Lambda round trip. An element of ILogic cannot be coerced to the other types. However ILogic can be used to produce a theory which can be concerted to/from the other domains using Curry-Howard isomorphism.

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