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 equivalent upto beta-equivalence and beta-equivalence is undecidable so there is not a direct correspondance 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.
Tutorial
If you are working with a version of FriCAS before 1.1.3 then all the computational domains need to be installed on your system, for later versions its already installed. The source code is in a file called computation.spad, which is available here:
https://github.com/martinbaker/multivector/
Download and compile in the usual way.
(1) -> )library VTYP
VarTyp is now explicitly exposed in frame frame1
VarTyp will be automatically loaded when needed from
/home/martin/VTYP.NRLIB/VTYP
(1) -> )library VARCAT
VarCat is now explicitly exposed in frame frame1
VarCat will be automatically loaded when needed from
/home/martin/VARCAT.NRLIB/VARCAT
(1) -> )library UNTYPED
Untyped is now explicitly exposed in frame frame1
Untyped will be automatically loaded when needed from
/home/martin/UNTYPED.NRLIB/UNTYPED
(1) -> )library ILOGIC
ILogic is now explicitly exposed in frame frame1
ILogic will be automatically loaded when needed from
/home/martin/ILOGIC.NRLIB/ILOGIC
(1) -> )library LAMBDA
Lambda is now explicitly exposed in frame frame1
Lambda will be automatically loaded when needed from
/home/martin/LAMBDA.NRLIB/LAMBDA
(1) -> )library SKICOMB
Ski is now explicitly exposed in frame frame1
Ski will be automatically loaded when needed from
/home/martin/SKI.NRLIB/SKI
(1) -> )library COMPUTIL
compUtil is now explicitly exposed in frame frame1
compUtil will be automatically loaded when needed from
/home/martin/COMP.NRLIB/COMP
|
Make sure it is exposed since Axiom/FriCAS was started. On this page we will be working with 'untyped' variables in λ and SKI terms so we create instances called LU and SU to simplify notation:
(1) -> )expose COMPUTIL
compUtil is now explicitly exposed in frame frame1
(1) -> LU := Lambda Untyped
(1) Lambda(Untyped)
Type: Type
(2) -> SU := Ski Untyped
(2) Ski(Untyped)
Type: Type |
SKI combinators to λ functions
We can then create SKI combinators and convert them to λ functions.
- For a tutorial about working with SKI combinators see this page.
- For a tutorial about working with λ functions see this page.
If the combinators don't have the required parameters then you will get a warning as follows. The code will attempt to add parameters as required but this will not work in complicated situations.
Ideally when working with 'abstract' combinatiors we need to add the required number of parameters, do the convertion then remove the parameters just added.
(3) -> I()$SU::LU
util coerce rule SL1: Ski[I] = \v0.0
(3) (\v0.v0)
Type: Lambda(Untyped)
(4) -> K()$SU::LU
util coerce rule SL2: Ski[K] = \v0.\v1.1
(4) (\v0.(\v1.v1))
Type: Lambda(Untyped)
(5) -> S()$SU::LU
util coerce rule SL3: Ski[S] = \v0.\v1.\v2.(2 0 (1 0))
(5) (\v0.(\v1.(\v2.(v2 (v0 (v1 v0))))))
Type: Lambda(Untyped) |
In the following examples the combinators are provided with the reqired parameters. This conversion works 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])
So here are some examples:
(6) -> parseSki("Ia")$SU::LU
util coerce apply rule SL1 in:I a
util coerce pass unbound variable a unchanged
(6) a
Type: Lambda(Untyped)
(7) -> parseSki("Ka b")$SU::LU
util coerce apply rule SL2 in:K a b
util coerce pass unbound variable a unchanged
(7) a
Type: Lambda(Untyped)
(8) -> parseSki("K(a b)c")$SU::LU
util coerce apply rule SL2 in:K(a b) c
util coerce rule SL4: Ski[(a b)] = (Ski[a] Ski[b])
util coerce pass unbound variable a unchanged
util coerce pass unbound variable b unchanged
(8) (a b)
Type: Lambda(Untyped)
(9) -> parseSki("Sa b c")$SU::LU
util coerce apply rule SL3 in:S a b c
util coerce pass unbound variable a unchanged
util coerce pass unbound variable c unchanged
util coerce pass unbound variable b unchanged
util coerce pass unbound variable c unchanged
(9) ((a c) (b c))
Type: Lambda(Untyped)
(10) -> parseSki("S(K(SI))(S(KK)I)")$SU::LU
util coerce rule SL4: Ski[(S(K(SI)) S(KK)I)] = (Ski[S(K(SI))] Ski[S(KK)I])
util coerce rule SL4: Ski[(S K(SI))] = (Ski[S] Ski[K(SI)])
util coerce rule SL3: Ski[S] = \v0.\v1.\v2.(2 0 (1 0))
util coerce rule SL4: Ski[(K SI)] = (Ski[K] Ski[SI])
util coerce rule SL2: Ski[K] = \v3.\v4.1
util coerce rule SL4: Ski[(S I)] = (Ski[S] Ski[I])
util coerce rule SL3: Ski[S] = \v5.\v6.\v7.(2 0 (1 0))
util coerce rule SL1: Ski[I] = \v8.0
util coerce rule SL4: Ski[(S(KK) I)] = (Ski[S(KK)] Ski[I])
util coerce rule SL4: Ski[(S KK)] = (Ski[S] Ski[KK])
util coerce rule SL3: Ski[S] = \v9.\v10.\v11.(2 0 (1 0))
util coerce rule SL4: Ski[(K K)] = (Ski[K] Ski[K])
util coerce rule SL2: Ski[K] = \v12.\v13.1
util coerce rule SL2: Ski[K] = \v14.\v15.1
util coerce rule SL1: Ski[I] = \v16.0
(10)
"(((\v0.(\v1.(\v2.(v2 (v0 (v1 v0)))))) ((\v3.(\v4.v4)) ((\v5.(\v6.(\v7.(v7 (v
5 (v6 v5)))))) (\v8.v8)))) (((\v9.(\v10.(\v11.(v11 (v9 (v10 v9)))))) ((\v12.(
\v13.v13)) (\v14.(\v15.v15)))) (\v16.v16)))"
Type: Lambda(Untyped) |
λ functions to SKI combinators
We can then create λ functions and convert them to SKI combinators.
- For a tutorial about working with SKI combinators see this page.
- For a tutorial about working with λ functions see this page.
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])
Here are some examples:
(11) -> parseLambda("x")$LU::SU
util coerce rule LS1 applied to:x giving x
(11) x
Type: Ski(Untyped)
(12) -> parseLambda("x y")$LU::SU
util coerce rule LS2 applied to:(x y) giving (x y)
util coerce rule LS1 applied to:x giving x
util coerce rule LS1 applied to:y giving y
(12) x y
Type: Ski(Untyped)
(13) -> parseLambda("\x.1")$LU::SU
util coerce rule LS3 applied to:(\x.1) giving K 1
util coerce rule LS1 applied to:1 giving 1
(13) K 1
Type: Ski(Untyped)
(14) -> parseLambda("\x.0")$LU::SU
util coerce warning could not match any rule to:(\x.x)
(14) I
Type: Ski(Untyped)
(15) -> parseLambda("\x.\y.0 1")$LU::SU
util coerce rule LS5 applied to:(\x.(\y.(0 1))) giving \x.(\y.(0 x))
util coerce rule LS6 applied to:(\y.(0 x)) giving S \y.y \y.x
util coerce rule LS1 applied to:y giving y
util coerce rule LS4' applied to: \y.y giving I
util coerce rule LS1 applied to:x giving x
util coerce rule LS3' applied to: \y.x giving K x
util coerce rule LS5' applied to: \x.SI(Kx) giving S \x.SI \x.Kx
util coerce rule LS3' applied to: \x.SI giving K \x.S \x.I
util coerce rule LS5' applied to: \x.Kx giving S \x.K \x.x
util coerce rule LS3' applied to: \x.K giving K K
util coerce rule LS4' applied to: \x.x giving I
(15) S(K(SI))(S(KK)I)
Type: Ski(Untyped) |
SKI combinators to Intuitionistic Logic
We can then create SKI combinators and convert them to intuitionistic logic.
- For a tutorial about working with SKI combinators see this page.
- For a tutorial about working with intuitionistic logic see this page.
This is known as the Curry–Howard isomorphism it uses the following rules:
- rule SI1: Ski[Ka b] => a -> (b -> a)
- rule SI2: Ski[Sa b c] => (a -> (b -> c)) -> ((a -> b) -> (a -> c))
- rule SI3: Ski[a a->b] => b
The last rule is function application (modus ponens). Here are some examples:
(16) -> parseSki("Ia")$SU::ILogic
util coerce apply rule SI1 in:I a
warning I does not have a parameter to act on
creating x
(16) ((x->x)->(x->x))
Type: ILogic
(17) -> parseSki("Ka b")$SU::ILogic
util coerce apply rule SI2 in:K a b
(17) (b->(a->b))
Type: ILogic
(18) -> parseSki("K(a b)c")$SU::ILogic
util coerce apply rule SI2 in:K(a b) c
(18) (c->((a\/b)->c))
Type: ILogic
(19) -> parseSki("Sa b c")$SU::ILogic
util coerce apply rule SI3 in:S a b c
(19) ((c->(b->a))->((c->b)->(c->a)))
Type: ILogic |
Next
Modeling Computation