Logic Utility Package

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.

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:

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.

This process is known as abstraction elimination. it is done by applying the following rules until all lambda terms have been eliminated.

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.

This is known as the Curry–Howard isomorphism it uses the following rules:

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

 


metadata block
see also:
Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.