computation.spad

)if false
\documentclass{article}
\usepackage{axiom}
\usepackage{url}
\begin{document}
\title{computation related mathematical structures}
\author{Martin J Baker}
\maketitle
\begin{abstract}
In this pamphlet are implementations of various mathematical
structures related to computation and type theory. These are:
\begin{itemize}
\item lambda.spad
\item ski.spad
\item ILogic.spad
\end{itemize}

The aim here is to model and study abstract models of computing such
as lambda-calculus, combinators and intuitionistic logic. These abstract
mathematical structures, which were discovered before modern computers,
are worthy of study in their own right.

We are less interested in using these domains to do actual computing
than to study the structures and their relationships to each
other. If we only wanted to evaluate a lambda function then there are
many other programs that could you that. So, in these domains such as
lambda, we do not attempt to reduce as soon as it is constructed
(although redux can be called if explicitly required). Instead we
leave it as a structure to be combined, transformed, compared and
studied.

Computing is often defined in terms of physical quantities such as
'information' and 'entropy' but here we are discussing computing in
mathematical terms [see 11]. In the 1930s, Kurt Godel, Alonzo Church,
Emil Post, and Alan Turing independently gave formal notions of
computation in terms of specific mathematical structures.
\begin{itemize}
\item Godel defined computation in terms of the evaluations of
recursive functions.
\item Church defined computation in terms of the evaluations of
lambda expressions,
\item Post defined computation as series of strings successively
rewritten according to a given rule set.
\item Turing defined computation in terms of the Turing machine,
the sequence of states of an abstract machine (usually explained
in terms of a physical machine with a control unit and a tape).
\end{itemize}
Can we abstract away from these specific structures to get a
more general definition?
A possible computational model is representation-transformation.
Provided that we can transform a given representation in a
sufficiently rich way (that is : Turing complete) then it can
represent any computation that is possible. There are limits to
what computations are possible as shown by applying Godel's
incompleteness theorems to computation. This gives rise to the
concept of undecidable problems.

So a 'representation' may for example be a string, but since
the string may contain brackets we can represent tree structures
and many other structures. Tree structures do seem to be a very
good representation for modeling many computations in an efficient
way.

Our 'transformation' may be a sequence of steps, or an algorithm,
or a function.

We are also interested in the relationship to logic, this approach
is based on the ideas of Philip Wadler [1] and others.
A program that uses this approach is Djinn [2]

The arguments of these 'computation' domains are functions and
combinators and the operation is usually function application,
although other operations such as function composition and
cartesian product may also be supported.

For combinators the number of arguments is variable and so function
application is non-associative hence it is represented by binary
tree structure.

For Lambda calculus function application is the opposite process
to the lambda function, that is lambda creates a function with
a bound variable and function application removes the bound variable.
Since we have bound and unbound variables so again non-associative
and represented by binary tree structure.

I am also working on a framework for function composition.
\url{http://www.euclideanspace.com/prog/scratchpad/mycode/discrete/homset/}
Function composition is associative and so can be
represented by a list structure. It therefore has different
mathematical properties to the structures studied here but they
can be related to closed cartesian categories.

These domains all represent systems of logic and are constructed from
tree structures and act on tree structures. These 'tree logics' seem
to 'generate' other algebras, for instance, below, we see that
this lambda structure:

\begin{verbatim}
\x.\y.y x
\end{verbatim}

can be converted to this SKI structure:

\begin{verbatim}
S(K(SI))(S(KK)I)
\end{verbatim}

This allows us to 'abstract' the definition, in that it takes a
definition in terms of arbitrary variables and it converts to a
definition without arbitrary variables. So these structures are
equivalent and they both reverse two operands. That is they generate
an $n$-ary to $n$-ary function, in this case:
\begin{verbatim}
(x, y) -> (y, x)
\end{verbatim}

This seems to be a 'monad' and it would be interesting to see if
these domains could be implemented as instances of a monad (a
monad in category theory terms, not the current FriCAS monad
category).

For more details see:
\url{http://www.euclideanspace.com/prog/scratchpad/mycode/computation/}
\begin{itemize}
\item Tutorial for lambda calculus:
  \url{http://www.euclideanspace.com/prog/scratchpad/mycode/computation/lambda/}
\item Tutorial for SKI calculus:
  \url{http://www.euclideanspace.com/prog/scratchpad/mycode/computation/ski/}
\item Tutorial for Intuitionistic Logic
  \url{http://www.euclideanspace.com/prog/scratchpad/mycode/discrete/logic/intuitionistic/}
\item Tutorial for utilities to coerce between computation domains
  \url{http://www.euclideanspace.com/prog/scratchpad/mycode/computation/utility/}
\item Tutorial for FriCAS source code generation
  \url{http://www.euclideanspace.com/prog/scratchpad/mycode/computation/codeGen/}
\end{itemize}
\end{abstract}
\eject
\tableofcontents
\eject
\section{To Do}

There are improvements and corrections required for later versions
of this software.

\begin{enumerate}

\item Overall architecture:
     Investigate possibility of basing implementation on Kernel or
     SExpression domains. Or we could extend some non-associative or
     binary tree structure class?

\item Possible generalisations:
  \begin{itemize}
  \item I am working on a function composition (hom-set) domain
     \url{http://www.euclideanspace.com/prog/scratchpad/mycode/discrete/homset/}
     and it would be interesting to implement these
     as a special (non-associative) version of that.
  \item It would be interesting to see if these domains could be implemented
     as instances of a monad.
  \item I would also like to extend this to investigate abstract structures
     such as 'tree automata'.
  \end{itemize}

\item Need to improve and correct intuitionistic logic domain.
   \begin{itemize}
   \item investigate change of meaning of '=' for intuitionistic logic to
     represent equivalence rather than equality.
   \item implement more complete algorithm to decide if two (quantifier-free)
     intuitionistic formulas are equivalent.
   \item make sure we have all simplifications for implies, /\, \/ and ~.
   \end{itemize}

\end{enumerate}
\section{Notation}

It would be useful to be able to use unicode, at the moment we can't
for compatibility reasons. When the restrictions on using unicode are
lifted then the following would be useful:

\begin{itemize}
\item lambda symbol
\item alpha (as in alpha-substitution)
\item beta (as in beta-equivalence)
\item bottom symbol for \verb'_|_'
\end{itemize}

Currently for logic symbols we use notation:

\verb'T, _|_, /\, \/, ~'

as opposed to other possibilities such as:
\begin{itemize}
\item \verb'true, false, and or'
\item \verb'0, 1, &, |'
\item \verb'join, meet, -'
\end{itemize}
This is because \verb'/\, \/, ~' are built-in
operators in FriCAS and are already used by Logic category.

Also this emphasizes the lattice-like structure of the intuitionistic
logic domain.  Also some systems of logic seem to treat
\verb'_|_' as a logical contradiction rather than
false. The aim is to use symbols that are compatible with both logic and
lattice terminology.

Implication is notated by -> to suggest its link to 'function'
although perhaps this should be changed to more standard =>.

In lambda calculus the elements are functions. Function application
and composition is notated by space, that is

f g represents f(g)

In lisp notation this would be (f g). Although we can use brackets
they are only used to indicate precedence and not to specify a function
since all variables are assumed functions.

I have used the term 'function application' for the following form:
f : A->B g : A = f g : B
and the term 'function composition' for the following form:
f : B->C g : A->B = f g : A->C
\section{Related Structures}

If we want to cover the full range of mathematical structures related
to computing then we should really include Finite State Machines and
Automata. These are coalgebra-like structures which are related to the
algebra structures already included.

I was thinking about how to convert a finite state machine into a
instance of Lambda, then I realised this is just about implementing
stateful code in a pure functional language and Haskell has already
solved that problem - use monads (from my limited knowledge of
Haskell I get the impression, whatever the problem, the answer is to
use monads).

Perhaps FriCAS should have a lattice structure which could then be
extended into intuitionistic logic domain. I don't think partially
ordered set (setorder.spad.pamphlet) would be in the right form to
extend logic domains.

Also graph structures, for instance:
\begin{itemize}
\item A deductive system is a graph where the nodes are formulas and
the arrows are deductions or proofs.
\item The category of small graphs is a concrete category.
\end{itemize}
Many of the domains in this document are also tree structures.

\section{Category Theory}

Lambek and Scott 1988 [10] show that typed lambda-calculi and
cartesian closed categories are essentially the same and
intuitionistic logic is closely related to topos theory.

Also the discussion of monads above tends to indicate that they
need to be used here.

All of this suggests to me that all the code in this document would
benefit from being put into a wider framework based on category
theory.

\section{Variables}
Before we get on to the main domains we have some code to represent
variables in Lambda and Ski domains.
Since we are working in terms of functions then a variable will be a
function (possibly a constant function).

There is a category to represent these function variables and there are
two implementations of this category so far:
\begin{description}
\item[Untyped] Untyped represents an untyped variable in Lambda and Ski
            domains, a variable has a name represented by a String.
\item[Typed] Typed represents an typed variable in Lambda and Ski
          domains, a variable has a name represented by a String
          and a type represented by intuitionistic logic.
\end{description}
\section{Variables Tutorial}
The two implementations : Untyped and Typed which can be constructed as
follows:

\begin{verbatim}
(1) -> var("x")$Untyped
   (1)  x
                                                             Type: Untyped
(2) -> var("x",proposition("a"))$Typed
   (2)  x:a
                                                               Type: Typed
(3) -> parseVar("x:(a->b)")$Typed
   (3)  x:(a->b)
                                                               Type: Typed
(4) -> parseVar("x:(a/\b)")$Typed
   (4)  x:(a/\b)
                                                               Type: Typed
(5) -> parseVar("x:(a\/b)")$Typed
   (5)  x:(a\/b)
                                                               Type: Typed
\end{verbatim}
(1) shows an untyped variable.

(2) shows a typed variable with a simple type "a"

In (3 to 5) we are entering a variable with a more complicated compound
types so it is easier to use parseVar to construct from
a string although this could have been built from raw types.

Note that the \verb': ' binds more tightly than \verb'->' so we need to put
brackets around \verb'a->b' so that its read as a type.

There are 3 ways to build up compound types:
\begin{itemize}
\item (3) shows \verb'a->b' which represents a function from a to b
\item (4) shows \verb'a/\b' which represents a type like Record(a, b)
\item (5) shows \verb'a\/b' which represents a type like Union(a, b)
\end{itemize}
We can nest these compound types to build up more complex types.

Variables are not usually constructed directly by the user but instead
are used by lambda and ski domains.
\section{Types}
There are various ways to interpret the concept of 'type' in the study
of both computation and in pure mathematical terms, for example:
\begin{itemize}
\item types as sets
\item types as abstractions (Reynolds)
\item types as relations (Wadler)
\item propositions as types (Curry-Howard)
\end{itemize}
We need to be able to model type theory and to do this flexibly.
We must build our own type domains rather than use the types used by
SPAD (although a possible future enhancement would be to support SPAD
types as a special case but not the general concept of type).

I am trying to develop an abstract model of general mathematical
structures here, not a sub-language within FriCAS, so I don't want to
over specify this. However I think it would be good to specify a model
which is as general as possible and can be expanded to model these
things.

So we need various levels of support for types depending on the
situation:
\begin{itemize}
\item untyped
\item simply typed - types are fixed and don't depend on anything else,
all we can do is check that types match up correctly.
\item extended types - we can refine simple types by using some or all
of the following extensions (level of support for these can be shown
graphically by a diagram known as the lambda cube)
\begin{itemize}
\item Type Operator (types depend on types) - For example : function types
or cartesian products.
\item Polymorphism (terms depend on types) - For example : we can define
functions which can be applied to parameters with different types.
\item Dependant Types (types depend on terms)
\end{itemize}
\end{itemize}
Initially, not all of these options are supported by this framework and
there are other issues, still to be resolved:
\begin{enumerate}
\item How do we handle (and should we handle) subtypes and the various
flavors of polymorphism? I was thinking of an additional type domain
within this category whose representation is a list of sub-types,
which in turn may have sub-sub-types. In other words a tree structure.
Most of the structures in this computation framework are already tree
structures so this fits the pattern.
\item How do we handle (and should we handle) compounded types such as
'List over String'?
\item It would be interesting to have a type domain in this category where
the types were SPAD types. This would be an exception, usually I
would prefer an abstract type model, but it may be possible to do
interesting things by mapping FriCAS to an abstract type model.
\item Could these type models be used outside of the computation
framework? For instance a set whose elements may be assigned different
types.
\end{enumerate}

One of the most important flavors to support is simply typed with
function types. This is because:
\begin{itemize}
\item It has enough power to represent most computations (although it
is not Turing complete - we would need fixpoint operator for that)
\item At this level there is an equivalence between Lambda calculus,
intuitionistic logic and closed cartesian categories which makes this
interesting.
\item We can infer types by using the Hindley-Milner type inference
algorithm.
\end{itemize}
\section{simply typed with type operator for function types
and cartesian products}
We can write formation rules for well typed terms (WTT) using the
following notation:
\begin{itemize}
\item x, y... (lower case) = variables
\item A, B ... (upper case, beginning alphabet) = types
\item M, N ... (upper case, middle alphabet) = metavariables for terms
\end{itemize}
Using this terminology the rules are:
\begin{itemize}
\item every variable x : A is a WTT.
\item Function creation:
if x : A is a variable and M : B is a WTT then \lambda x : A.M : A->B is a WTT
\item Function application:
if M : A -> B is a WTT and N : A is a WTT then M N : B is a WTT
\item Product creation:
if M : A is a WTT and N : B is a WTT then <M, N>: A \times B is a WTT
\item Product removal (first component):
if M : A \times B is a WTT then fst(M) : A is a WTT
\item Product removal (second component):
if M : A \times B is a WTT then snd(M) : B is a WTT
\end{itemize}

Now we will implement variables:

First a common category for the various variable types:
\section{category VARCAT VarCat}
)endif

)abbrev category VARCAT VarCat
++ Author: Martin Baker
++ Date Created: April 2011
++ Basic Operations:
++ Related Constructors: lambda, ski
++ Also See:
++ AMS Classifications:
++ Keywords:
++ References:
++ http://www.euclideanspace.com/prog/scratchpad/mycode/computation/
++ Description: VarCat represents a variable in Lambda and Ski domains.
++ Since we are working in terms of functions then a variable will be a
++ function (possibly a constant function)
++ a variable has a name represented by a String. If the Lambda or Ski
++ calculus is typed then the variable will also have a type.

VarCat() : Category == Join(Type, CoercibleTo(OutputForm)) with
  var : (n : String) -> %
    ++ constructs variable with a name but no type.
  var : (n : String, t : ILogic) -> %
    ++ constructs variable with a name and also a type.
  getName : (v : %) -> String
    ++ returns the name of the variable.
  getType : (v : %) -> ILogic
    ++ returns the type of the variable. This may be a compound type, for
    ++ instance ["a","b"] represents a->b a function from type a to type b
    ++ untyped implementations return []
  toString : (v : %) -> String
    ++ returns the name and the type in string form.
  parseVar : (t1 : String)-> %
    ++ construct a variable by parsing a string
  parseVarTerm : (t1 : String, pin : NonNegativeInteger)-> Record(rft : %, pout : NonNegativeInteger)
    ++ construct a variable by parsing a string
    ++ pin is index to string at start of parse
    ++ pout is index to string at end of parse
  "=":(x:%, y:%) -> Boolean
    ++ return true if equal, that is names are equal and if there is
    ++ a type then they must also be equal
  coerce : (n : %) -> OutputForm
    ++ output


)if false

Next an implementation of the above category which is intended to work with
untyped variables:

\section{domain UNTYPED Untyped}
)endif

)abbrev domain UNTYPED Untyped
++ Author: Martin Baker
++ Date Created: April 2011
++ Basic Operations:
++ Related Constructors: lambda, ski
++ Also See:
++ AMS Classifications:
++ Keywords:
++ References:
++ http://www.euclideanspace.com/prog/scratchpad/mycode/computation/
++ Description: Untyped represents an untyped variable in Lambda and Ski
++ domains, a variable has a name represented by a String.

Untyped() : Exports == Implementation where

  NNI==> NonNegativeInteger
  PR ==> Record(rft : %, pout : NNI)
    ++ parse result includes string returned and new index

  Exports ==> Join(VarCat(), CoercibleTo(OutputForm))

  Implementation ==> add

    Rep := Record(nme : String)
      ++ At the moment an untyped variable is represented by a string
      ++ representing the name of the variable.
      ++ So why wrap it in a Record structure.
      ++ The main reason is because I am planning to expand this as
      ++ explained in the text part of this pamphlet.
      ++ Also it seems like a good idea to keep a similar structure to
      ++ typed variables.
      ++ Also I could not get it to work unwrapped. I vaguely recall that
      ++ I couldn't get the constructor to return an unwrapped value, but
      ++ it may have been some other issue and that's not the main reason.

    -- constructs variable with a name but no type
    var(n : String) : % ==
      [n]

    -- since this is an untyped implementation the type value
    -- is ignored
    var(n : String, t : ILogic) : % ==
      [n]

    -- returns the name of the variable.
    getName(v : %) : String ==
      v.nme

    -- returns the type of the variable.
    -- Since this is an untyped variable it will always return an
    -- empty string.
    getType(v : %) : ILogic ==
      logicT()

    -- returns the name and the type in string form.
    toString(v : %) : String ==
      v.nme

    -- construct a variable by parsing a string
    -- pin is index to string at start of parse
    -- pout is index to string at end of parse
    parseVarTerm(t1 : String, pin : NNI) : PR ==
        vnm:String := ""
        pt : NNI := pin
        ch := qelt(t1, pt)
        --print(message "st ch=" << ch)
        while alphanumeric?(ch) repeat
            vnm := concat(vnm, ch)
            pt := pt + (1::NNI)
            if pt > maxIndex(t1) then
                return [var(vnm), pt]
            ch := qelt(t1, pt)
        if ch = char(":") then
            -- read type
            --print(message "st ch=" << ch)
            r : Record(rft : ILogic, pout : NNI) := parseIL2(t1, pt)$ILogic
            pt := r.pout
          -- since this instance is untyped we ignore result
        [var(vnm), pt]

    -- construct a variable by parsing a string
    parseVar(t1 : String) : % ==
      r : PR := parseVarTerm(t1, 1::NNI)
      r.rft

    -- return true if equal, that is names are equal (since there are
    -- no types that is all that is required) in the case of typed
    -- implementations then they would also have to be equal.
    x = y ==
      x.nme = y.nme

    -- output - display without quotes
    coerce(n : %) : OutputForm ==
        message(n.nme)

)if false

Next an implementation of the VarCat category which is intended to work with
typed variables:

\section{domain TYPED Typed}
)endif

)abbrev domain TYPED Typed
++ Author: Martin Baker
++ Date Created: April 2011
++ Basic Operations:
++ Related Constructors: lambda, ski
++ Also See:
++ AMS Classifications:
++ Keywords:
++ References:
++ http://www.euclideanspace.com/prog/scratchpad/mycode/computation/
++ Description: Typed represents an typed variable in Lambda and Ski
++ domains, a variable has a name represented by a String and a type
++ represented by intutionistic logic.

Typed() : Exports == Implementation where

  NNI==> NonNegativeInteger
  PR ==> Record(rft : %, pout : NNI)
    ++ parse result includes string returned and new index

  Exports ==> Join(VarCat(), CoercibleTo(OutputForm))

  Implementation ==> add

    Rep := Record(nme : String, typ : ILogic)
      ++ name of variable
      ++ and type of variable

    -- constructs variable with a name but no type
    var(n : String) : % ==
      [n, logicT()]

    -- in this constructor both name and type are supplied
    var(n : String, t : ILogic) : % ==
      [n, t]

    -- returns the name of the variable.
    getName(v : %) : String ==
      v.nme

    -- returns the type of the variable. This may be a compound type, for
    -- instance ["a","b"] represents a->b a function from type a to type b
    getType(v : %) : ILogic ==
      v.typ

    -- returns the name and the type in string form. This may be a compound
    -- type, for instance ["a","b"] represents a->b a function from type a
    -- to type b
    toString(v : %) : String ==
      s:String := concat([v.nme,":",toString(v.typ)])
      s

    -- construct a variable by parsing a string
    -- pin is index to string at start of parse
    -- pout is index to string at end of parse
    parseVarTerm(t1 : String, pin : NNI) : PR ==
      vnm:String := ""
      pt : NNI := pin
      ch := qelt(t1, pt)
      --print(message "st ch=" << ch)
      while alphanumeric?(ch) repeat
        vnm := concat(vnm, ch)
        pt := pt + (1::NNI)
        if pt > maxIndex(t1) then
          return [var(vnm), pt]
        ch := qelt(t1, pt)
      if ch = char(":") then
        -- read type
        --print(message "st ch=" << ch)
        pt := pt + (1::NNI)
        if pt > maxIndex(t1) then
          return [var(vnm), pt]
        r : Record(rft : ILogic, pout : NNI) := parseIL2(t1, pt)$ILogic
        pt := r.pout
        return [var(vnm, r.rft), pt]
      [var(vnm), pt]

    -- construct a variable by parsing a string
    parseVar(t1 : String) : % ==
      r : PR := parseVarTerm(t1, 1::NNI)
      r.rft

    -- return true if equal, that is names are equal (since there are
    -- no types that is all that is required) in the case of typed
    -- implementations then they would also have to be equal.
    x = y ==
      (x.nme = y.nme) and (x.typ = y.typ)

    -- output -
    coerce(n : %) : OutputForm ==
      hconcat([message (n.nme),message ":",(n.typ)::OutputForm])$OutputForm

)if false

\section{lambda-Calculus}
for more details see:
\url{http://www.euclideanspace.com/prog/scratchpad/mycode/computation/lambda/}

\section{Notation}

Externally a fairly standard notation is used, as may be familiar to
someone using a textbook to study lambda-calculus, or as close as we can get
without using unicode. I have used the \verb'\' symbol to stand for lambda. At
some stage in the future it may be possible to use unicode lambda symbol
but not yet due to compatibility issues.

Internally the domain stores bound variables using De Bruijn index,
in most cases this should not concern the user as I/O uses string
names for variables. Converting bound variables internally to index
values means that the same variable name can be used, in different
lambda terms, without ambiguity and without the need for
alpha-substitution.

De Bruijn index which is a integer where
\begin{verbatim}
    0 = inside current (inner) lambda term
    1= next outer lambda term
    2= next outer and so on
    ...
\end{verbatim}

We will see how this works in the tutorial below.

So internally the lambda-calculus is stored as a binary tree structure
using the following syntax:
\begin{verbatim}
<term> : := "\" var "."<term> | n | <term><term> | "("<term>")"

where:

    \ = lambda
    n = De Bruijn index which is a integer where,
        0 = inside inner lambda term,
        1= next outer lambda term,
        2= next outer and so on.
    var = a string representation of variable (this form is used for
          unbound variables)
    brackets can be used around whole terms.
\end{verbatim}

\section{Tutorial}

On this page we will be working with 'untyped' variables so we create
an instance called UNTYP to simplify notation:
\begin{verbatim}
(1) -> UNTYP := Lambda Untyped
   (1)  Lambda(Untyped)
                                                           Type: Type
\end{verbatim}

\section{Constructors}

First we can enter some variables, at the moment they are not inside
a lambda-term so they can't yet be bound, but later we can put them into
a lambda-term.

A numeric name is interpreted as a De Bruijn index when put inside
a lambda-term, although we don't need this notation for I/O unless we are
trying to avoid some ambiguity, because free and bound variables can
be constructed by giving the variable name as a string. So in (4) is
not yet a valid term on its own but it will be when put inside a
lambda-term, when this is done it will be given the name of the bound
variable rather than "0".

Internally a string name will be converted to a De Bruijn index when
put inside a matching lambda-term, otherwise it will be interpreted as a
free variable.
\begin{verbatim}
(2) -> v1 := lambda(var("x")$Untyped)$UNTYP
   (2)  x
                                                    Type: Lambda(Untyped)
(3) -> v2 := lambda(var("y")$Untyped)$UNTYP
   (3)  y
                                                    Type: Lambda(Untyped)
(4) -> v3 := lambda(0)$UNTYP
   (4)  0
                                                    Type: Lambda(Untyped)
\end{verbatim}

This can be built up into more complex lambda terms by using compound
terms (as in (5)) and the lambda-term itself (as in (6)).

Each lambda-term can only have one bound variable, if more than one bound
variable is required then lambda-terms can be nested. lambda-term requires that
the bound variable be given a name.
\begin{verbatim}
(5) -> n1 := lambda(v1, v2)$UNTYP
   (5)  (x y)
                                                    Type: Lambda(Untyped)
(6) -> n2 := lambda(n1,var("x")$Untyped)$UNTYP
   (6)  (\x.(x y))
                                                    Type: Lambda(Untyped)
\end{verbatim}

In (7) \verb'x' is a the bound variable and so, when the lambda-term was created,
this will be converted to De Bruijn index, in (7) we call toString to
see the internal representation:

In (8) we see that when entered as a numeric index the bound variable
will still be displayed as a string.

In (9) and (10) we can see that the \verb'unbind' function can be used to
unbind the bound variable \verb'x' that is, although \verb'x' has the same string
value as the lambda term, it is treated as though it were different.
We can see this because the toString output does not have a index value.
In (11) we call \verb'bind' to re-bind it.
\begin{verbatim}
(7) -> toString(n2)$UNTYP
   (7)  "(\x.(0 y))"
                                                             Type: String
(8) -> n3 := lambda(v3,var("x")$Untyped)$UNTYP
   (8)  (\x.x)
                                                    Type: Lambda(Untyped)
(9) -> u2 := unbind(n2)$UNTYP
   (9)  (\x.(x y))
                                                    Type: Lambda(Untyped)
(10) -> toString(u2)$UNTYP
   (10)  "(\x.(x y))"
                                                             Type: String
(11) -> toString(bind(u2))$UNTYP
   (11)  "(\x.(0 y))"
                                                             Type: String
\end{verbatim}

So we can already construct any type of lambda term, however its a bit
tedious to construct complex lambda terms in this way, an easier way is
to use \verb'parseLambda' to construct the lambda term from a string. Again
we can enter variables as either alpha or numeric characters depending
on whether we want to specify the index value directly or allow the
code to generate it.

In (14) we can see the use of numeric terms to avoid the ambiguity
caused by nested lambda-terms with the same name.
\begin{verbatim}
(12) -> n4 := parseLambda("\x.\y. y x")$UNTYP
   (12)  (\x.(\y.(x y)))
                                                    Type: Lambda(Untyped)
(13) -> toString(n4)$UNTYP
   (13)  "(\x.(\y.(0 1)))"
                                                             Type: String
(14) -> n4a := parseLambda("\x.\x. 0 1")$UNTYP
   (14)  (\x.(\x'.(x x')))
                                                    Type: Lambda(Untyped)
(15) -> toString(n4a)$UNTYP
   (15)  "(\x.(\x.(0 1)))"
                                                             Type: String
(16) -> unbind(n4a)$UNTYP
   (16)  (\x.(\x'.(x x)))
                                                    Type: Lambda(Untyped)
\end{verbatim}

\section{beta-substitution}

The command: \verb'subst : (n, a, b)' substitutes \verb'a' for \verb'b'
in \verb'n' as follows:
\begin{verbatim}
(17) -> subst(n2, v2, v1)$UNTYP
   (17)  (\x.(x y))
                                                    Type: Lambda(Untyped)
(18) -> subst(n2, v1, v2)$UNTYP
   (18)  (\x.(x x))
                                                    Type: Lambda(Untyped)
\end{verbatim}

\section{Issues}

I realise that Axiom/FriCAS already has a way to create anonymous
functions using \verb'+->' in a lambda-calculus sort of way. But the aim here
is to represent lambda-calculus as a pure mathematical structure so that
we can experiment with the properties of this structure without the
messy features that are required for a practical computer language.
I also need a domain structure which is related to SKI combinators
and IntuitionisticLogic domain and can be coerced to and from these
other domain types as demonstrated on this page.

I also realise that this is written in SPAD which is written in
Lisp which is based on lambda-Calculus (perhaps it could later be
optimized by having direct calls to Lisp?)
Relationship to Other Domains

\section{Relationship to Other Domains}

lambda-calculus can be coerced to and from SKI combinators. For a tutorial
about how to coerce to/from this algebra see below.

\section{domain LAMBDA Lambda}
)endif

)abbrev domain LAMBDA Lambda
++ Author: Martin Baker
++ Date Created: March 2011
++ Basic Operations:
++ Related Constructors:
++ Also See:
++ AMS Classifications:
++ Keywords:
++ References:
++ http://www.euclideanspace.com/prog/scratchpad/mycode/computation/lambda/
++ An implementation of untyped lambda-calculus

Lambda(UT) : Exports == Implementation where

 UT : VarCat
 NNI==> NonNegativeInteger
 PR ==> Record(rft : %, pout : NNI)
   ++ parse result includes term returned and new index
 x<<y ==> hconcat(x::OutputForm,y::OutputForm)
   ++ macro to simplify output

 Exports == CoercibleTo(OutputForm) with
  lambda : (deBruijn : NNI) -> %
    ++ Constructs a reference to a bound variable from its deBruijn
    ++ index
  lambda : (varNme : UT) -> %
    ++ Constructs a reference to a free variable
  lambda : (x : %, y : %) -> %
    ++ Constructs a node containing multiple terms
  lambda : (x : %, t1 : UT) -> %
    ++ Constructs lambda term and bind any variables with the name provided
  parseLambda : (t1 : String) -> %
    ++ Constructs nested lambda terms from a string
    ++ notation assumes format like this:
    ++ <term> : := "\" var "."<term> | n | <term><term> | "("<term>")"
    ++ where:
    ++ \ = lambda (I would like to use unicode lambda symbol but
    ++             I would also like to keep maximum compatibility
    ++             with non-unicode versions of Lisp)
    ++ n = De Bruijn index which is a integer where, 1=inside inner
    ++             lambda term, 2= next outer lambda term, 3= next
    ++             outer and so on.
    ++ brackets can be used around whole terms.
  parseTerm : (t1 : String, pin : NNI) -> PR
    ++ parseTerm is used by parseLambda. It would rarely be called
    ++ externally but it is here to allow it to call parseLambda
    ++ that is to allow circular calls
  atom? : (n : %) -> Boolean
    ++ returns true if this is an atom, that is free or bound variable
    ++ otherwise return false if this is a compound or lambda definition
  isCompound? : (n : %) -> Boolean
    ++ introspection: returns true if this is a compound term containing
    ++ two nodes
  isLambda? : (n : %) -> Boolean
    ++ introspection: returns true if this is a lambda definition
  isBoundNode? : (n : %) -> Boolean
    ++ introspection: returns true if this is a bound leaf node
  isFreeNode? : (n : %) -> Boolean
    ++ introspection: returns true if this is a unbound leaf node
  getBoundValue : (n : %) -> NNI
    ++ introspection: returns deBruijn index of bound variable in bound
    ++ leaf node
  getVariable : (n : %) -> UT
    ++ introspection: returns value of unbound variable in unbound leaf
    ++ node or bound variable in lambda term
  free? : (n : %) -> Boolean
    ++ if this is a lambda term then is it free, that is does
    ++ its variable appear in its expression
  getChildren : (n : %) -> List %
    ++ returns 2 child nodes if this is a compound term
    ++ returns 1 child node if this is a lamda term
    ++ otherwise returns []
  subst : (n : %, a : %, b : %) -> %
    ++ substitution of 'a' for 'b' in 'n'
  bind : (n : %) -> %
    ++ if this is a lambda term then replace string name in sub-nodes
    ++ with De Bruijn index
  unbind : (n : %) -> %
    ++ if this is a lambda term then replace De Bruijn index in sub-nodes
    ++ with string name
  redux : (n : %) -> %
    ++ beta reduction - apply beta reduction recusivly to all subnodes
  "=":(x:%, y:%) -> Boolean
    ++ return true if equal (deep search) that is: all terms
    ++ at all levels in tree must be alpha-equivalent to return true
    ++ That is the names, but not the deBruijn index, of the
    ++ bound variables can be different.
    ++ beta-equivalence is not implemented because it is not decidable.
  toStringConven : (n : %, boundL : List String) -> String
    ++ return string representation using conventional notation, that is
    ++ deBruijn index is replaced by name using String value for bound variables.
    ++ notation assumes association to the left, in the absence of
    ++ brackets, the term to the left binds more tightly than the
    ++ one on the right.
  toString : (n : %) -> String
    ++ return string representation using deBruijn index for
    ++ bound variables.
    ++ notation assumes association to the left, in the absence of
    ++ brackets, the term to the left binds more tightly than the
    ++ one on the right.
  coerce : (n : %) -> OutputForm
    ++ output

 Implementation == add

  Rep := Union(_
         boundTerm : Record(varBound : NNI), _
         freeTerm : UT, _
         compoundTerm : Record(c1 : %, c2 : %), _
         lambdaTerm : Record(c3 : %, nm : UT)_
         )
    ++ this allows us to represent potentially nested lambda
    ++ expressions as a tree structure where the nodes are
    ++ one of:
    ++ 1) boundTerm: Record(varBound: NNI)
    ++    This represents a bound variable using De Bruijn index.
    ++       varBound = De Bruijn index which is a integer where,
    ++             1=inside inner lambda term
    ++             2= next outer lambda term,
    ++             3= next outer and so on.
    ++
    ++ 2) freeTerm: UT
    ++    This represents an unbound variable so De Bruijn index
    ++    is not used.
    ++
    ++ 3) compoundTerm: Record(c1: %, c2: %)
    ++   Adjacent nodes represent function application
    ++
    ++ 4) lambdaTerm: Record(c3: %, nm: UT)
    ++    when used the outer term should be a lambdaTerm although
    ++    lambda terms may also be nested within the tree structure
    ++    c3 holds the subnodes
    ++    nm is the bound term for this lambda node
    ++   There is only one bound term for each lambda node, if more
    ++   are required then lambda nodes can be nested.

  -- Constructs a reference to a bound variable from its deBruijn
  -- index
  lambda(n1 : NNI) : % == [[n1]]

  -- Constructs a reference to a free variable from its name
  lambda(var : UT) : % == [var]

  -- Constructs a node containing multiple terms
  lambda(x : %, y : %) : % == [[x, y]]

  -- Constructs lambda term and bind any variables with the name provided
  lambda(x : %, t1 : UT) : % ==
    lt : % := [[x, t1]]
    --print(message "creating lambda(" << toString(x) << _
    --  message "," << t1 << message ") giving:" << toString(lt))
    --print(message "bound ver=" << toString(bind(lt)))
    bind(lt)

  -- returns 2 child nodes if this is a compound term
  -- returns 1 child node if this is a lambda term
  -- otherwise returns []
  getChildren(n : %) : List % ==
    if atom?(n) then return []
    if n case compoundTerm then
      return [n.compoundTerm.c1, n.compoundTerm.c2]
    if n case lambdaTerm then
      return [n.lambdaTerm.c3]
    []

  -- returns true if this is an atom, that is free or bound variable
  -- otherwise return false if this is a compound or lambda definition
  atom?(n : %) : Boolean == (n case boundTerm) or (n case freeTerm)

  -- introspection:  returns true if this is a compound term containing
  -- two nodes
  isCompound?(n : %) : Boolean == (n case compoundTerm)

  -- introspection:  returns true if this is a lambda definition
  isLambda?(n : %) : Boolean == (n case lambdaTerm)

  -- introspection: returns true if this is a bound leaf node
  isBoundNode?(n : %) : Boolean == (n case boundTerm)

  -- introspection: returns true if this is a unbound leaf node
  isFreeNode?(n : %) : Boolean == (n case freeTerm)

  -- introspection: returns deBruijn index of bound variable in bound
  -- leaf node
  getBoundValue(n : %) : NNI ==
    if n case boundTerm then
      return n.boundTerm.varBound
    0::NNI

  -- introspection: returns value of unbound variable in unbound leaf
  -- node or bound variable in lambda term
  getVariable(n : %) : UT ==
    if n case freeTerm then
      return n.freeTerm
    if n case lambdaTerm then
      return n.lambdaTerm.nm
    var("error")$UT

  -- does s not appear in n
  freeVariable?(n : %, s : UT) : Boolean ==
    if n case freeTerm then
      if n.freeTerm = s then return false
    if n case lambdaTerm then
      if not freeVariable?(n.lambdaTerm.c3, s) then return false
    if n case compoundTerm then
      if not freeVariable?(n.compoundTerm.c1, s) or _
         not freeVariable?(n.compoundTerm.c2, s) then return false
    true

  -- return false if any bound terms
  freeVariable?(n : %, i : NNI) : Boolean ==
    if n case boundTerm then
      if n.boundTerm.varBound = i then return false
    if n case lambdaTerm then
      if not freeVariable?(n.lambdaTerm.c3, (i+1)::NNI) then return false
    if n case compoundTerm then
      if (not freeVariable?(n.compoundTerm.c1, i)) or _
         (not freeVariable?(n.compoundTerm.c2, i)) then return false
    true

  -- if this is a lambda term then is it free, that is does
  -- its variable appear in its expression
  free?(n : %) : Boolean ==
    if n case lambdaTerm then
      --s1: String := name(n.lambdaTerm.nm)$UT
      return freeVariable?(n.lambdaTerm.c3, 0::NNI)
    print(message "warning free called on non-lambda term" << n)
    false

  parseLambdaTerm(t1 : String, pin : NNI) : PR ==
    --print(message "parseLambdaTerm(" << t1 << " << ",string(pin) << ")")
    p1 := pin
    ch := qelt(t1, p1)
    if not (ch = char("\")) then
      error "lambda term must start with \"
      return [[[0::NNI]], p1]
    p1 := p1 + (1::NNI)
    if p1 > maxIndex(t1) then
      error "lambda term not complete"
      return [[[0::NNI]], p1]
    r := parseVarTerm(t1, p1)$UT
    p1 := r.pout
    ch := qelt(t1, p1)
    --print(message "parseLambdaTerm'(" << t1 << "," << string(p1) << ")")
    if not (ch = char(".")) then
      error "lambda term must have ."
      return [[[0::NNI]], p1]
    p1 := p1 + (1::NNI)
    --print(message "parseLambdaTerm''(" << t1 << "," << string(p1) << ")")
    if p1 > maxIndex(t1) then
      error "lambda term must contain something"
      return [[[0::NNI]], p1]
    --print(message "parseLambdaTerm'''(" << t1 << "," << string(p1) << ")")
    r2 := parseTerm(t1, p1)
    ex : % := r2.rft
    p1 := r2.pout
    [lambda(ex, r.rft), p1]

  parseBracketTerm(t1 : String, pin : NNI) : PR ==
    p1 := pin
    ch := qelt(t1, p1)
    if not (ch = char("(")) then
      error "bracket term must start with ("
      return [[[0::NNI]], p1]
    p1 := p1 + (1::NNI)
    if p1 > maxIndex(t1) then
      error "opening but no closing bracket"
      return [[[0::NNI]], p1]
    r2 := parseTerm(t1, p1)
    trm := r2.rft
    p1 := r2.pout
    ch := qelt(t1, p1)
    if not (ch = char(")")) then
      error "can't find closing bracket"
      return [[[0::NNI]], p1]
    p1 := p1 + (1::NNI)
    [trm, p1]

  parseVariableTerm(t1 : String, pin : NNI) : PR ==
    p1 := pin
    inx : NNI := 0 -- holds De Bruijn index while its being read
    ch := qelt(t1, p1)
    --print(message "pv ch=" << ch)
    while digit?(ch) repeat
      if ch = char("0") then inx := inx*10
      if ch = char("1") then inx := inx*10 + 1
      if ch = char("2") then inx := inx*10 + 2
      if ch = char("3") then inx := inx*10 + 3
      if ch = char("4") then inx := inx*10 + 4
      if ch = char("5") then inx := inx*10 + 5
      if ch = char("6") then inx := inx*10 + 6
      if ch = char("7") then inx := inx*10 + 7
      if ch = char("8") then inx := inx*10 + 8
      if ch = char("9") then inx := inx*10 + 9
      p1 := p1 + (1::NNI)
      if p1 > maxIndex(t1) then return [lambda(inx), p1]
      ch := qelt(t1, p1)
    [lambda(inx), p1]

  parseTerm(t1 : String, pin : NNI) : PR ==
    p1 := pin
    res : % := [[0::NNI]]
    ch := qelt(t1, p1)
    --print(message "parseTerm ch=" << ch << " p1=" << string(p1))
    -- first remove leading spaces
    while ch = char(" ") repeat
      p1 := p1 + (1::NNI)
      if p1 > maxIndex(t1) then
        --print(message "parseTerm(" << t1 << ") 1 giving:" << _
        --  toString(res))
        return [res, p1]
      ch := qelt(t1, p1)
    r : PR := [res, p1]
    if ch = char("\") then r := parseLambdaTerm(t1,p1)
    if ch = char("(") then r := parseBracketTerm(t1,p1)
    if digit?(ch) then r := parseVariableTerm(t1, p1)
    res := r.rft
    p1 := r.pout
    if alphabetic?(ch) then
      r2 := parseVarTerm(t1, p1)$UT
      res := lambda(r2.rft)
      p1 := r2.pout
    -- now check for compound term
    if p1 > maxIndex(t1) then
      --print(message "parseTerm(" << t1 << ") 2 giving:" << _
      --  toString(res))
      return [res, p1]
    ch := qelt(t1, p1)
    if ch = char(" ") then
      p1 := p1 + (1::NNI)
      if p1 > maxIndex(t1) then
        --print(message "parseTerm(" << t1 << ") 3 giving:" << _
        --  toString(res))
        return [res, p1]
      r := parseTerm(t1, p1)
      p1 := r.pout
      res := lambda(res, r.rft)
    --print(message "parseTerm(" << t1 << ") 4 giving:" << _
    --  toString(res))
    [res, p1]

  -- Constructs nested lambda terms from a string
  -- notation assumes format like this:
  -- <term> : := "\" var "."<term> | n | <term><term> | "("<term>")"
  -- where:
  -- \ = lambda (I would like to use unicode lambda symbol but
  --             I would also like to keep maximum compatibility
  --             with non-unicode versions of Lisp)
  -- n = De Bruijn index which is a integer where, 1=inside inner
  --             lambda term, 2= next outer lambda term, 3= next
  --             outer and so on.
  -- brackets can be used around whole terms.
  parseLambda(t1 : String) : % ==
    r := parseTerm(t1, minIndex(t1)::NNI)
    --print(message "parseLambda(" << t1 << ") giving:" << _
    --  toString(tm))
    r.rft

  -- return string representation using conventional notation, that is
  -- deBruijn index is replaced by name using String value for bound variables.
  -- notation assumes association to the left, in the absence of
  -- brackets, the term to the left binds more tightly than the
  -- one on the right.
  toStringConven(n : %, boundL : List String) : String ==
    s:String := ""
    --print(message "toStringConven(" << toString(n) << message ")")
    if n case boundTerm then
      i : NNI := n.boundTerm.varBound + 1
      --print(message "toStringConven(" << toString(n) << ") i=" << _
      --  string(i) << " #boundL=" << string(#boundL))
      if i > 0 and i <= #boundL then return boundL.i
      s := string(n.boundTerm.varBound)
    if n case freeTerm then
      s := getName(n.freeTerm)$UT
    if n case compoundTerm then
      s := concat(["(",toStringConven(n.compoundTerm.c1,boundL)," ",toStringConven(n.compoundTerm.c2,boundL),")"])
    if n case lambdaTerm then
      -- variable node so print name
      varName : String := getName(n.lambdaTerm.nm)$UT
      while member?(varName, boundL) repeat
        varName := concat(varName,"'")
      boundL2 : List String := concat(boundL, varName)
      s := concat(["(\",varName,".",toStringConven(n.lambdaTerm.c3,boundL2),")"])
    s

  -- return string representation using deBruijn index for
  -- bound variables.
  -- notation assumes association to the left, in the absence of
  -- brackets, the term to the left binds more tightly than the
  -- one on the right.
  toString(n : %) : String ==
    s:String := ""
    if n case boundTerm then
      s := string(n.boundTerm.varBound)
    if n case freeTerm then
      s := toString(n.freeTerm)$UT
    if n case compoundTerm then
      s := concat(["(",toString(n.compoundTerm.c1)," ",toString(n.compoundTerm.c2),")"])
    if n case lambdaTerm then
      -- variable node so print name
      s := concat(["(\",toString(n.lambdaTerm.nm)$UT,".",toString(n.lambdaTerm.c3),")"])
    s

  -- substitution of 'a' for 'b' in 'n'
  subst(n : %, a : %, b : %) : % ==
    if n = b then return a
    if (n case compoundTerm) then
      return lambda(subst(n.compoundTerm.c1, a, b), subst(n.compoundTerm.c2, a, b))
    if (n case lambdaTerm) then
      return lambda(subst(n.lambdaTerm.c3, a, b), n.lambdaTerm.nm)
    n

  -- used by bind to replace a given string name in sub-nodes
  -- with De Bruijn index
  bindTerm(n : %, i : NNI, s : UT) : % ==
    --print(message "bindTerm(" << toString(n) << " map:" << _
    --  string(i) << " to " << (name(s)$UT) << ")")
    if n case boundTerm then
      return lambda(n.boundTerm.varBound)
    if n case freeTerm then
      if n.freeTerm = s then
        --print(message "convert:" << (name(s)$UT) << _
        --  " to " << string(i))
        return lambda(i)
      return lambda(n.freeTerm)
    if n case lambdaTerm then
      --print(message "bindTerm generating lambda(" << _
      --  toString(bindTerm(n.lambdaTerm.c3,i+1,s)) << "," << _
      --  (name(n.lambdaTerm.nm)$UT) << ")")
      return [[bindTerm(n.lambdaTerm.c3, i+1, s), n.lambdaTerm.nm]]
    if n case compoundTerm then
      return lambda(bindTerm(n.compoundTerm.c1, i, s), _
                    bindTerm(n.compoundTerm.c2, i, s))
    n

  -- if this is a lambda term then replace string name in sub-nodes
  -- with De Bruijn index
  bind(n : %) : % ==
    --print(message "bind(" << toString(n) << ")")
    if (n case lambdaTerm) then
      return [[bindTerm(n.lambdaTerm.c3, 0, n.lambdaTerm.nm), n.lambdaTerm.nm]]
    n

  -- used by unbind to replace a given De Bruijn index in sub-nodes
  -- with string name
  unbindTerm(n : %, i : NNI, s : UT) : % ==
    --print(message "unbindTerm(" << toString(n) << " map:" << _
    --   string(i) << " to " << (name(s)$UT) << ")")
    if n case boundTerm then
      if n.boundTerm.varBound = i then
        --print(message "convert:" << string(i) << _
        -- message " to " << (name(s)$UT))
        return lambda(s)
      return lambda(n.boundTerm.varBound)
    if n case freeTerm then
      return lambda(n.freeTerm)
    if n case lambdaTerm then
      --print(message "unbindTerm generating lambda(" << _
      --  toString(unbindTerm(n.lambdaTerm.c3,i+1,s)) << "," << _
      --  name(n.lambdaTerm.nm) << message ")")
      return [[unbindTerm(n.lambdaTerm.c3, i+1, s), n.lambdaTerm.nm]]
    if n case compoundTerm then
      return lambda(unbindTerm(n.compoundTerm.c1, i, s), _
                    unbindTerm(n.compoundTerm.c2, i, s))
    n

  -- if this is a lambda term then replace De Bruijn index in sub-nodes
  -- with string name
  unbind(n : %) : % ==
    --print(message "unbind(" << toString(n) << message ")")
    if (n case lambdaTerm) then
      return [[unbindTerm(n.lambdaTerm.c3, 0, n.lambdaTerm.nm), n.lambdaTerm.nm]]
    n

  -- beta reduction - apply beta reduction recursively to all subnodes
  redux(n : %) : % ==
    if atom?(n) then return n -- atom cant be reduced
    if n case compoundTerm then
      -- we are looking for a compound term where the first term is
      -- a lambda expression being applied to the second term.
      term1 : % := n.compoundTerm.c1
      term2 : % := n.compoundTerm.c2
      if isLambda?(term1) then
        -- apply term1 to term2
        boundVarName : String := getName(term1.lambdaTerm.nm)$UT
        return subst(term1, term2, lambda(0::NNI))
      return lambda(redux(term1), redux(term2))
    if n case lambdaTerm then
      return lambda(redux(n.lambdaTerm.c3), n.lambdaTerm.nm)
    n

  -- return true if equal (deep search) that is: all terms
  -- at all levels in tree must be alpha-equivalent to return true
  -- That is the names, but not the deBruijn index, of the
  -- bound variables can be different.
  x = y ==
    if (x case boundTerm) and (y case boundTerm) then
      -- boundTerm so compare deBruijn index
      if x.boundTerm.varBound = y.boundTerm.varBound then return true
      return false
    if (x case freeTerm) and (y case freeTerm) then
      -- freeTerm so compare variables
      if x.freeTerm = y.freeTerm then return true
      return false
    if (x case compoundTerm) and (y case compoundTerm) then
      -- compoundTerm so compare both terms
      if (x.compoundTerm.c1 = y.compoundTerm.c1) and_
         (x.compoundTerm.c2 = y.compoundTerm.c2) then return true
      return false
    if (x case lambdaTerm) and (y case lambdaTerm) then
      -- lambdaTerm only compare body not variable name
      if x.lambdaTerm.c3 = y.lambdaTerm.c3 then return true
      return false
    false


  -- return OutputForm using conventional notation, that is
  -- deBruijn index is replaced by name using String value for bound variables.
  -- notation assumes association to the left, in the absence of
  -- brackets, the term to the left binds more tightly than the
  -- one on the right.
  toOutputFormConven(n : %, boundL:List(String)) : OutputForm ==
      s:OutputForm := empty()$OutputForm
      --print(message "toOutputFormConven(" << toString(n) << ")")
      if n case boundTerm then
          i : NNI := n.boundTerm.varBound + 1
          --print(message "toOutputFormConven(" << toString(n) << _
          --   ") i=" << string(i) << " #boundL=" << string(#boundL))
          -- if index is within range use it to lookup String value
          -- convert it to Symbol first to avoid displaying quotes.
          if i > 0 and i <= #boundL then return message(boundL.i)
          -- otherwise display bound term as NNI (deBruijn index)
          s := (n.boundTerm.varBound)::OutputForm
      if n case freeTerm then
          s := (n.freeTerm)::OutputForm
      if n case compoundTerm then
          s := hconcat([message("("),
                        toOutputFormConven(n.compoundTerm.c1, boundL),
                        message(" "),
                        toOutputFormConven(n.compoundTerm.c2, boundL),
                        message(")")])$OutputForm
      if n case lambdaTerm then
          -- variable node so print name
          varName : String := getName(n.lambdaTerm.nm)$UT
          while member?(varName, boundL) repeat
              varName := concat(varName,"'")
          boundL2 : List String := concat(boundL, varName)
          s := hconcat([message("(\"),
                        message(varName),
                        message("."),
                        toOutputFormConven(n.lambdaTerm.c3, boundL2),
                        message(")")])$OutputForm
      s

  -- output
  coerce(n : %) : OutputForm == toOutputFormConven(n,[])

)if false

\section{SKI Combinators}
for more details see:
\url{http://www.euclideanspace.com/prog/scratchpad/mycode/computation/ski/}

Ski combinators were introduced by Moses Schoenfinkel and Haskell
Curry with the aim of eliminating the need for variables in
mathematical logic. It is equivalent to lambda calculus but
it can be used for doing, without variables, anything that
would require variables in other systems.

The structure is a self-modifying binary tree.
\section{Tutorial}

On this page we will be working with 'untyped' SKI combinators
so we create an instance called UNTYP to simplify notation:

\begin{verbatim}
(1) -> UNTYP := SKICombinators Untyped

   (1)  SKICombinators(Untyped)
                                                           Type : Type
\end{verbatim}

\section{Constructing SKI combinators}

SKI combinators consist of a binary tree structure where the leaves
of the tree are either $I$, $K$ or $S$ combinators or variables.

The $I$, $K$ and $S$ combinators can be constructed by using the $I()$,
$K()$ and $S()$ functions.

Variables (representing functions) can be constructed by
\verb'var("x")$Untyped', where \verb'x' is the name of the variable, we can
then pass this variable to a ski constructor to create a SKI term:
\begin{verbatim}
(2) -> m1 := I()$UNTYP

   (2)  I
                                      Type: SKICombinators(Untyped)
(3) -> m2 := K()$UNTYP

   (3)  K
                                      Type: SKICombinators(Untyped)
(4) -> m3 := S()$UNTYP

   (4)  S
                                      Type: SKICombinators(Untyped)
(5) -> v1 := ski(var("x")$Untyped)$UNTYP

   (5)  x
                                      Type: SKICombinators(Untyped)
\end{verbatim}
Compound combinator terms can be constructed by \verb'ski(node1, node2)' where
\verb'node1' and \verb'node2' are other combinator terms. Internally
combinators are stored as a binary tree. The notation assumes association
to the left, in the absence of brackets, the term to the left binds more
tightly than the one on the right. So, in the following, we can see that:
\begin{itemize}
\item In n2 the second term is an atom so brackets are not required.
\item In n3 the second term is compound so brackets are required.
\end{itemize}
\begin{verbatim}
(6) -> n1 := ski(m1, m2)$UNTYP

   (6)  IK
                                      Type: SKICombinators(Untyped)
(7) -> n2 := ski(n1, m3)$UNTYP

   (7)  IKS
                                      Type: SKICombinators(Untyped)
(8) -> n3 := ski(m3, n1)$UNTYP

   (8)  S(IK)
                                      Type: SKICombinators(Untyped)
\end{verbatim}
In addition, to avoid having to build up this node by node, there is a
quicker way to construct SKI combinators. We can construct the whole
binary tree from a single string using the \verb'parseSki' constructor as
follows. Again the notation assumes association to the left, in the
absence of brackets, the term to the left binds more tightly than the
one on the right.

When we are using parseSki and we have two variables next to each other
(such as \verb'x y') then we must put a space between the variables, this is
so that we can gave a variable a name consisting of multiple characters.
So \verb'xy' is a single variable but \verb'x y' is two variables. All variables
must start with a lower case letter. The combinators $I$, $K$, and $S$ do not
need to be separated with a space since they always consist of 1
character.
\begin{verbatim}
(9) -> n4 := parseSki("IKS")$UNTYP

   (9)  IKS
                                      Type: SKICombinators(Untyped)
(10) -> n5 := parseSki("S(IK)")$UNTYP

   (10)  S(IK)
                                      Type: SKICombinators(Untyped)
\end{verbatim}
\section{redux}

Now that we have constructed our SKI combinator we can apply the
combinators using the redux function. This allows us to apply the
self-modifying binary tree.

The first combinator to investigate is $I$. This is a do nothing
combinator:
\begin{verbatim}
(11) -> s1 := parseSki("Ix")$UNTYP

   (11)  I x
                                      Type: SKICombinators(Untyped)
(12) -> redux(s1)$UNTYP
   x

   (12)  x
                                      Type: SKICombinators(Untyped)
\end{verbatim}
The next combinator to investigate is $K$. This removes the final
variable:
\begin{verbatim}
(13) -> s2 := parseSki("Kx y")$UNTYP

   (13)  K x y
                                      Type: SKICombinators(Untyped)
(14) -> redux(s2)$UNTYP
   x

   (14)  x
                                      Type: SKICombinators(Untyped)
\end{verbatim}
The next combinator to investigate is $S$ This applies the first two
functions to the third:
\begin{verbatim}
(15) -> s3 := parseSki("Sx y z")$UNTYP

   (15)  S x y z
                                      Type: SKICombinators(Untyped)
(16) -> redux(s3)$UNTYP
   x z(y z)

   (16)  x z(y z)
                                      Type: SKICombinators(Untyped)
\end{verbatim}
\section{Secondary Combinators}

Any calculation can be done by some combination of $K$ and $S$. However
some sequences occur frequently so it is worth assigning them special
letters:

\begin{tabular}{lll}
Operator&        What it does&    SKI equivalent (normal form)\\
$I$ &      Identity (leave unchanged)  &     $I$ or $SKK$ or $SKS$\\
$B$ &      Function composition        &    $S(KS)K$\\
$B'$&      Reverse function composition&\\
$C$ &      Swap functions              &    $S(K(SI))K$\\
$K$ &      Form constant function      &    $K$\\
$S$ &      Generalized composition     &    $S$\\
$W$ &      Doubling or diagonalizing   &\\
\end{tabular}

So we can see in the 3 examples below :

    In 17 that $SKKxy$ is equivalent to $xy$, that is $SKK$ is identity,
equivalent to I
    In 19 that $S(K(SI))Kxy$ is equivalent to $yx$, so "S(K(SI))K"
reverses its operands.
\begin{verbatim}
(17) -> redux(parseSki("SKKx y")$UNTYP)$UNTYP
   K x(K x) y
   x y

   (17)  x y
                                      Type: SKICombinators(Untyped)
(18) -> redux(parseSki("S(KS)x y")$UNTYP)$UNTYP
   KS y(x y)
   S(x y)

   (18)  S(x y)
                                      Type: SKICombinators(Untyped)
(19) -> redux(parseSki("S(K(SI))Kx y")$UNTYP)$UNTYP
   K(SI) x(K x) y
   I y(K x y)
   y x

   (19)  y x
                                      Type: SKICombinators(Untyped)
\end{verbatim}
SKI combinators can be coerced to and from lambda-calculus and
intuitionistic logic. For a tutorial about how to coerce to/from these
algebras see this page.
\section{To Do}

These are issues to think about for longer term development of this domain.
\begin{itemize}
\item Issue 1

Currently this only works with variables, this means that:
\begin{verbatim}
    redux applied to 'SKKx y' gives 'x y'
    but redux applied to 'SKK' does not give 'I'
\end{verbatim}

That is, I am looking for a way to 'lift' from working in terms operators
acting on variables to working in terms of operators only.
\item Issue 2

It would be good to be able to use these combinators to operate on
Axiom/FriCAS functions.

\item See also

I also have Axiom/FriCAS coding for lambda-calculus, as explained on this
page, where there is explanation and tutorial.
\end{itemize}

\section{domain SKICOMB SKICombinators}
)endif

)abbrev domain SKICOMB SKICombinators
++ Author: Martin Baker
++ Date Created: March 2011
++ Basic Operations:
++ Related Constructors:
++ Also See:
++ AMS Classifications:
++ Keywords:
++ References:
++ http://www.euclideanspace.com/prog/scratchpad/mycode/computation/ski/

SKICombinators(UT) : Exports == Implementation where

 UT : VarCat
 NNI==> NonNegativeInteger
 PR ==> Record(rft : %, pout : NNI)
   ++ parse result includes term returned and new index

 Exports == SetCategory with
  ski : (x : %, y : %) -> %
    ++ Constructs a node combinator over combinators
  ski : (t1 : UT) -> %
    ++ Constructs variable combinator
  I : () -> %
    ++ Constructs a I combinator
  K : () -> %
    ++ Constructs a K combinator
  S : () -> %
    ++ Constructs a S combinator
  parseSki : (t1 : String) -> %
    ++ Constructs combinators from a string
  parseTerm : (t1 : String, pin : NNI) -> PR
    ++ parseTerm is used by parseSki. It would rarely be called
    ++ externally but it is here to allow it to call parseSki
    ++ that is to allow circular calls
  getChildren : (n : %) -> List %
    ++ returns child nodes if this is a compound term
    ++ otherwise returns []
  atom? : (n : %) -> Boolean
    ++ returns true if this is an atom, that is a leaf node
    ++ otherwise return false if this is a compound term
  variable? : (n : %) -> Boolean
    ++ returns true if this is an variable
  isI? : (n : %) -> Boolean
    ++ returns true if this is an I combinator node
  isK? : (n : %) -> Boolean
    ++ returns true if this is a K combinator node
  isS? : (n : %) -> Boolean
    ++ returns true if this is a S combinator node
  getVariable : (n : %) -> UT
    ++ returns the variable, if this is not a
    ++ variable then return I
  freeVariable? : (n : %, s : UT) -> Boolean
    ++ the variable indicated by 's' is free if it does
    ++ not appear in node 'n' or any of its subnodes.
  redux : (n : %) -> %
    ++ weak reduction - apply this combinator to rearrange its
    ++ subnodes then apply recursively to its subnodes.
  "=":(x:%, y:%) -> Boolean
    ++ return true if equal (deep search) that is: all terms
    ++ at all levels in tree must be equal to return true
    ++ all terms must be exactly equal, not just equivalent, that is
    ++ SKK=I will return false even though 'SKK' and 'I' have the
    ++ same effect
  toString : (n : %) -> String
    ++ output
  coerce : (n : %) -> OutputForm
    ++ output

 Implementation == add

  Rep := Union(_
         lf : Symbol, _
         nd : Record(c1 : %, c2 : %), _
         vr : UT_
         )
    ++ this allows us to represent a combinator expression
    ++ as a tree structure where the nodes are one of:
    ++
    ++ 1) lf: Symbol
    ++     This node contains the combinator terms themselves currently
    ++     coded as:
    ++     I combinator = "I"::Symbol
    ++     K combinator = "K"::Symbol
    ++     S combinator = "S"::Symbol
    ++
    ++ 2) Record(c1: %, c2: %)
    ++     This represents a branch in the tree.  Adjacent nodes
    ++     represent function application.
    ++
    ++ 3) UT
    ++     this represents a variable (function)
    ++

  -- Constructs a node combinator over another combinators
  ski(x : %, y : %) : % == [[x, y]]

  -- Constructs variable combinator
  ski(t1 : UT) : % ==
    [t1]

  -- Constructs a I combinator
  I() : % == ["I"::Symbol]

  -- Constructs a K combinator
  K() : % == ["K"::Symbol]

  -- Constructs a S combinator
  S() : % == ["S"::Symbol]

  parseBracketTerm(t1 : String, pin : NNI) : PR ==
    p1 := pin
    ch := qelt(t1, p1)
    if not (ch = char("(")) then
      error "bracket term must start with ("
      return [["I"::Symbol],p1]
    p1 := p1 + (1::NNI)
    if p1 > maxIndex(t1) then
      error "opening but no closing bracket"
      return [["I"::Symbol],p1]
    r2 := parseTerm(t1, p1)
    trm := r2.rft
    p1 := r2.pout
    ch := qelt(t1, p1)
    if not (ch = char(")")) then
      error "can't find closing bracket"
      return [["I"::Symbol],p1]
    p1 := p1 + (1::NNI)
    [trm, p1]

  -- t1 is string term to be parsed
  -- pin is an integer pointer to the first character in t1 to be
  -- parsed
  parseCombinatorTerm(t1 : String, pin : NNI) : PR ==
    p1 := pin
    ch := qelt(t1, p1)
    if ch = char("I") then
      return [["I"::Symbol],p1 + (1::NNI)]
    if ch = char("K") then
      return [["K"::Symbol],p1 + (1::NNI)]
    if ch = char("S") then
      return [["S"::Symbol],p1 + (1::NNI)]
    error "invalid combinator"
    [["I"::Symbol],p1 + (1::NNI)]

  -- t1 is string term to be parsed
  -- pin is an integer pointer to the first character in t1 to be
  -- parsed
  parseOneTerm(t1 : String, pin : NNI) : PR ==
    p1 := pin
    res:% := ["I"::Symbol]
    ch := qelt(t1, p1)
    --print(message "parseTerm ch=" << ch << _
    --  message " p1=" << string(p1))
    -- first remove leading spaces
    while ch = char(" ") repeat
      p1 := p1 + (1::NNI)
      if p1 > maxIndex(t1) then
        --print(message "parseTerm(" << t1 << _
        --  message ") 1 giving:" << toString(res))
        return [res, p1]
      ch := qelt(t1, p1)
    if alphabetic?(ch) then
      if upperCase?(ch) then
        r := parseCombinatorTerm(t1, p1)
        res := r.rft
        p1 := r.pout
        --print(message "parseTerm(" << t1 << _
        --  ") 4 giving:" << toString(res))
      if lowerCase?(ch) then
        --print(message "parseTerm(" << t1 << _
        --  message ") 4 giving:" << toString(res))
        r2 := parseVarTerm(t1, p1)$UT
        res := ski(r2.rft)
        p1 := r2.pout
    if ch = char("(") then
      r := parseBracketTerm(t1, p1)
      res := r.rft
      p1 := r.pout
    [res, p1]

  parseTerm(t1 : String, pin : NNI) : PR ==
    p1 := pin
    r := parseOneTerm(t1, p1)
    res : % := r.rft
    p1 := r.pout
    -- now check for compound term
    if p1 > maxIndex(t1) then
      --print(message "parseTerm(" << t1 << _
      --  message ") 2 giving:" << toString(res))
      return [res, p1]
    ch := qelt(t1, p1)
    stck : List % := []
      ++ in order to get association to the left we will put terms
      ++ in a list
    while alphabetic?(ch) or ch = char(" ") or ch = char("(") repeat
      r := parseOneTerm(t1, p1)
      p1 := r.pout
      stck := concat(stck, r.rft)
      --print(message "parseTerm(" << t1 << _
      --  message ") 4 giving:" << toString(res))
      if p1 > maxIndex(t1)
        then ch := char("*")
        else ch := qelt(t1, p1)
    for i in 1..#stck repeat
      res := ski(res, stck.i)
    [res, p1]


  -- Constructs combinators from a string
  -- notation assumes association to the left, in the absence of
  -- brackets, the term to the left binds more tightly than the
  -- one on the right.
  parseSki(t1 : String) : % ==
    r := parseTerm(t1, minIndex(t1)::NNI)
    --print(message "parseSki(" << t1 << _
    --  message ") giving:" << toString(tm))
    r.rft

  -- returns child nodes if this is a compound term
  -- otherwise returns []
  getChildren(n : %) : List % ==
    if atom?(n) then return []
    [n.nd.c1, n.nd.c2]

  -- returns true if this is an atom, that is a leaf node
  -- otherwise return false if this is a compound term
  atom?(n : %) : Boolean == (n case lf) or (n case vr)

  -- returns true if this is an variable
  variable?(n : %) : Boolean == (n case vr)

  -- returns true if this is an I combinator node
  isI?(n : %) : Boolean ==
    if not (n case lf) then return false
    if n.lf = "I"::Symbol then return true
    false

  -- returns true if this is a K combinator node
  isK?(n : %) : Boolean ==
    if not (n case lf) then return false
    if n.lf = "K"::Symbol then return true
    false

  -- returns true if this is a S combinator node
  isS?(n : %) : Boolean ==
    if not (n case lf) then return false
    if n.lf = "S"::Symbol then return true
    false

  -- introspection: returns the variable, if this is not a
  -- variable node then return " "
  getVariable(n : %) : UT ==
    if n case vr then
      return n.vr
    var(" ")$UT

  -- the variable indicated by 's' is free if it does
  -- not appear in node 'n' or any of its subnodes.
  freeVariable?(n : %, s : UT) : Boolean ==
    if n case vr then
      if n.vr = s then return false
    if n case nd then
      if not freeVariable?(n.nd.c1, s) or _
         not freeVariable?(n.nd.c2, s) then return false
    true

  -- return string representation
  -- notation assumes association to the left, in the absence of
  -- brackets, the term to the left binds more tightly than the
  -- one on the right.
  toString(n : %) : String ==
    s:String := ""
    if n case lf then
      -- leaf node so print I, K or S
      if n.lf = "I"::Symbol then s := "I"
      if n.lf = "K"::Symbol then s := "K"
      if n.lf = "S"::Symbol then s := "S"
    if n case nd then
      -- binary node which has two subnodes c1 and c2
      if atom?(n.nd.c2) then
        if variable?(n.nd.c2)
          then
            s := concat([s,toString(n.nd.c1)," ",toString(n.nd.c2)])
          else
            s := concat([s, toString(n.nd.c1), toString(n.nd.c2)])
      else
        s := concat([s,toString(n.nd.c1),"(",toString(n.nd.c2),")"])
    if n case vr then
      -- variable node so print name
      s := toString(n.vr)$UT
    s

  -- weak reduction - apply this combinator to rearrange its
  -- subnodes then apply recursively to its subnodes
  redux1(n : %) : % ==
    if n case nd then
      -- binary node which has two subnodes c1 and c2
      left := redux1(n.nd.c1)
      right := redux1(n.nd.c2)
      --print(message "left=" << toString(left) << _
      --      message " right=" << toString(right))
      if isI?(left) then return right
      if not (left case nd) then return ski(left, right)
      leftleft := left.nd.c1
      leftright := left.nd.c2
      --print(message "leftleft=" << toString(leftleft) << _
      --                    " leftright=" << toString(leftright))
      if isK?(leftleft) then return leftright
      if not (leftleft case nd) then return ski(left, right)
      leftleftleft := leftleft.nd.c1
      leftleftright := leftleft.nd.c2
      --print(message "leftleftleft=" << toString(leftleftleft) << _
      --                    " leftleftright=" << toString(leftleftright))
      if isS?(leftleftleft) then
        return ski(ski(leftleftright, right), ski(leftright, right))
      return ski(left, right)
    n

  -- weak reduction - apply this combinator to rearrange its
  -- subnodes then apply recursively to its subnodes
  redux(n : %) : % ==
    lastResult := ["I"::Symbol]
    thisResult := redux1(n)
    triesLeft : NNI := 20::NNI -- limit tries in case of loop
    while (lastResult ~= thisResult) and (triesLeft > (1::NNI)) repeat
      lastResult := thisResult
      thisResult := redux1(lastResult)
      triesLeft := (triesLeft - 1)::NNI
      print(lastResult::OutputForm)
    thisResult

  -- return true if equal (deep search) that is: all terms
  -- at all levels in tree must be equal to return true
  -- all terms must be exactly equal, not just equivalent, that is
  -- SKK=I will return false even though 'SKK' and 'I' have the
  -- same effect
  x = y ==
    if (x case lf) and (y case lf) then
      -- leaf node so compare I, K or S
      if x.lf = y.lf then return true
      return false
    if (x case vr) and (y case vr) then
      -- variable node so compare names
      if x.vr = y.vr then return true
      return false
    if (x case nd) and (y case nd) then
      -- binary node which has two subnodes c1 and c2
      if (x.nd.c1 = y.nd.c1) and (x.nd.c2 = y.nd.c2) then return true
      return false
    false

  -- output
  coerce(n : %) : OutputForm ==
      s : OutputForm := empty()$OutputForm
      if n case lf then
          -- leaf node so print I, K or S
          s := (n.lf)::OutputForm
      if n case nd then
          -- binary node which has two subnodes c1 and c2
          if atom?(n.nd.c2) then
              if variable?(n.nd.c2) then
                  s := hconcat([s,_
                                (n.nd.c1)::OutputForm,_
                                message(" "),_
                                (n.nd.c2)::OutputForm])$OutputForm
              else
                  s := hconcat([s, (n.nd.c1)::OutputForm,
                                (n.nd.c2)::OutputForm])$OutputForm
          else
              s := hconcat([s,(n.nd.c1)::OutputForm,message("("),_
             (n.nd.c2)::OutputForm,message(")")])$OutputForm
      if n case vr then
          -- variable node so print name
          s := (n.vr)::OutputForm
      s


)if false

\section{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 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
\verb'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.
\section{Tutorial}
First make sure this package is exposed.

(1) -> )expose COMPUTIL

   compUtil is now explicitly exposed in frame frame1

On this page we will be working with 'untyped' variables
in lambda and SKI terms so we create instances called LU and
SU to simplify notation:
\begin{verbatim}
(1) -> LU := Lambda Untyped

   (1)  Lambda(Untyped)
                                                         Type: Type
(2) -> SU := SKICombinators Untyped

   (2)  SKICombinators(Untyped)
                                                         Type: Type
\end{verbatim}
\section{SKI combinators to lambda functions}

We can then create SKI combinators and convert them to lambda functions.

    For a tutorial about working with SKI combinators see:
\url{http://www.euclideanspace.com/prog/scratchpad/mycode/computation/ski/}

    For a tutorial about working with lambda functions see:
\url{http://www.euclideanspace.com/prog/scratchpad/mycode/computation/lambda/}

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 conversion then remove the
parameters just added.
\begin{verbatim}
(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)
\end{verbatim}

In the following examples the combinators are provided with the required
parameters. This conversion works by applying the following rules:
\begin{verbatim}
    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])
\end{verbatim}

So here are some examples:
\begin{verbatim}
(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 (v5 (v6 v5)))))) (\v8.v8))))

     (
       ((\v9.(\v10.(\v11.(v11 (v9 (v10 v9))))))
         ((\v12.(\v13.v13)) (\v14.(\v15.v15))))
        (\v16.v16))
     )
                                              Type: Lambda(Untyped)
\end{verbatim}

\section{lambda functions to SKI combinators}

We can then create lambda functions and convert them to SKI combinators.

    For a tutorial about working with SKI combinators see this page.
    For a tutorial about working with lambda 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.
\begin{verbatim}
    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])
\end{verbatim}

Here are some examples:
\begin{verbatim}
(11) -> parseLambda("x")$LU::SU
   util coerce rule LS1 applied to:x giving x

   (11)  x
                                      Type: SKICombinators(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: SKICombinators(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: SKICombinators(Untyped)
(14) -> parseLambda("\x.0")$LU::SU
   util coerce warning could not match any rule to:(\x.x)

   (14)  I
                                      Type: SKICombinators(Untyped)
(15) -> parseLambda("\x.\y.0 1")$LU::SU
   util coerce rule LS5 applied to:(\x.(\y.(x y))) giving \x.(\y.(y x))
   util coerce rule LS6 applied to:(\y.(y 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(K x) giving S \x.SI \x.K x
   util coerce rule LS3' applied to: \x.SI giving K \x.S \x.I
   util coerce rule LS5' applied to: \x.K x 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: SKICombinators(Untyped)
\end{verbatim}
\section{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:
http://www.euclideanspace.com/prog/scratchpad/mycode/computation/ski/
    For a tutorial about working with intuitionistic logic see:
\url{http://www.euclideanspace.com/prog/scratchpad/mycode/discrete/logic/intuitionistic/}


This is known as the Curry-Howard isomorphism it uses the following rules:
\begin{verbatim}
    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
\end{verbatim}

The last rule is function application (modus ponens). Here are some
examples:
\begin{verbatim}
(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
parseSki("Ka b")$SU::ILogic
   util coerce apply rule SI2 in:K a b

   (17)  (b->(a->b))
                                                       Type: ILogic
parseSki("K(a b)c")$SU::ILogic
   util coerce apply rule SI2 in:K(a b) c

   (18)  (c->((a\/b)->c))
                                                       Type: ILogic
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
\end{verbatim}

\section{package COMPUTIL compUtil}
)endif

)abbrev package COMPUTIL compUtil
++ Author: Martin Baker
++ Date Created: April 2011
++ Basic Operations:
++ Related Constructors:
++ Also See:
++ AMS Classifications:
++ Keywords:
++ References:
++ http://www.euclideanspace.com/prog/scratchpad/mycode/computation/utility/
++ Description:
++ 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.

compUtil(UT) : Exports == Implementation where

 UT : VarCat
 LU ==> Lambda UT
 SU ==> SKICombinators UT
 NNI==> NonNegativeInteger
 x<<y ==> hconcat(x::OutputForm,y::OutputForm)
   ++ macro to simplify output

 Exports ==> with
    coerce : (s : SU) -> LU
      ++ 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])
    coerce : (lam : LU) -> SU
      ++ 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 : (s : SU) -> 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)

 Implementation ==> add

  import OutputForm

  -- Keeps count of index number of variables created in Ski2Lambda.
  -- I am wary of defining a variable outside of a function but
  -- can't find another non-messy way to update it from several
  -- functions.
  varNum : NNI := 0::NNI

  -- used by coerce SKI combinators to Lambda term.
  Ski2Lambda(s : SU) : LU ==
    -- if s is an atom then this means that there are no
    -- parameters for this combinator. If there had been
    -- they would have been found when this was called on
    -- the nodes above it.
    -- print(message "util coerce called for:" << s))
    if atom?(s)$SU then
      --print(message "util coerce atom:" << s)
      if isI?(s)$SU then
        strVar:String := concat("v",string(varNum))
        print(message "util coerce rule SL1: Ski[I] = \" << message strVar
              << message ".0")
        varNum := varNum +1
        return parseLambda(concat["\",strVar,".0"])$LU
      if isK?(s)$SU then
        strVar1:String := concat("v",string(varNum))
        strVar2:String := concat("v",string(varNum+1))
        print(message "util coerce rule SL2: Ski[K] = \" << message strVar1
              << message ".\" << message strVar2 << message ".1")
        varNum := varNum +2
        return parseLambda(concat["\",strVar1,".\",strVar2,".1"])$LU
      if isS?(s)$SU then
        strVar1:String := concat("v",string(varNum))
        strVar2:String := concat("v",string(varNum+1))
        strVar3:String := concat("v",string(varNum+2))
        print(message "util coerce rule SL3: Ski[S] = \" << message strVar1
              << message ".\" << message strVar2 << message ".\" <<
              message strVar3 << message ".(2 0 (1 0))")
        varNum := varNum +3
        return parseLambda(concat["\",strVar1,".\",strVar2,".\",strVar3,".(2 0 (1 0))"])$LU
      print(message "util coerce pass unbound variable " << _
        (message getName(getVariable(s)$SU)$UT) << message " unchanged")
      return lambda(getVariable(s)$SU)$LU
    subnodes : List SU := getChildren(s)$SU
    c1 : SU := first subnodes
    c2 : SU := second subnodes
    s1 : String := toString(c1)$SU
    s2 : String := toString(c2)$SU
    -- print(message "util coerce c1=" << (toString(c1)$SU) << " c2=" <<
    --       toString(c2))
    -- look for I x, if found translate x
    if isI?(c1)$SU then
      print(message "util coerce apply rule SL1 in:" << s)
      return Ski2Lambda(c2)
    if atom?(c1)$SU then
      print(message "util coerce rule SL4: Ski[(" << message s1 << message" "
            << message s2 << message ")] = (Ski[" << message s1 <<
            message "] Ski[" << message s2 << message "])")
      return lambda(Ski2Lambda(c1), Ski2Lambda(c2))$LU
    -- look for K x y, if found translate x
    subsubnodes : List SU := getChildren(c1)$SU
    c11 : SU := first subsubnodes
    c12 : SU := second subsubnodes
    --print(message "util coerce c1=" << (toString(c1)$SU) << _
    --  message " c2=" << (toString(c2)$SU) << " c11=" << _
    --  (toString(c11)$SU) << " c12=" << (toString(c12)$SU))
    if isK?(c11)$SU then
      s12 : String := getName(getVariable(c12)$SU)$UT
      print(message "util coerce apply rule SL2 in:" << s)
      return Ski2Lambda(c12)
    if atom?(c11)$SU then
      print(message "util coerce rule SL4: Ski[(" << message s1 << _
        message " " << message s2 << message ")] = (Ski[" << message s1 << _
        message "] Ski[" << message s2 << message "])")
      return lambda(Ski2Lambda(c1), Ski2Lambda(c2))$LU
    -- look for S x y z, if found translate (x z)(y z)
    subsubnodes2 : List SU := getChildren(c11)$SU
    c111 : SU := first subsubnodes2
    c112 : SU := second subsubnodes2
    --print(message "util coerce c11=" << (toString(c11)$SU) << _
    --  message " c12=" << (toString(c12)$SU) << " c111=" << _
    --  (toString(c111)$SU) << " c112=" << (toString(c112)$SU))
    -- look for K x y, if found translate x
    if isS?(c111)$SU then
      s2 : String := getName(getVariable(c2)$SU)$UT
      s12 : String := getName(getVariable(c12)$SU)$UT
      s112 : String := getName(getVariable(c112)$SU)$UT
      print(message "util coerce apply rule SL3 in:" << s)
      return lambda(lambda(Ski2Lambda(c112), Ski2Lambda(c2))$LU, lambda(Ski2Lambda(c12), Ski2Lambda(c2))$LU)$LU
    print(message "util coerce rule SL4: Ski[(" << message s1 << message " "
          << message s2 << message ")] = (Ski[" << message s1 <<
          message "] Ski[" << message s2 << message "])")
    lambda(Ski2Lambda(c1), Ski2Lambda(c2))$LU

  -- 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])
  coerce(s : SU) : LU ==
    varNum := 0
    term : LU := Ski2Lambda(s)
    term

  -- when we are coercing Lambda to Ski and we apply rule LS5
  -- we call this
  lambdaOverSki(var : UT, sk : SU) : SU ==
    --print(message "gives \" << (toString(var)$UT) << _
    --  message "." << toString(sk))
    if atom?(sk) then
      if freeVariable?(sk, var)$SU then
        print(message "util coerce rule LS3' applied to: \" << _
          var << message "." << sk << _
          message " giving K " << sk)
        return ski(K(), sk)
      print(message "util coerce rule LS4' applied to: \" << _
        var << message "." << sk << message " giving I")
      return I()$SU
    ch : List SU := getChildren(sk)$SU
    left : SU := first ch
    right : SU := second ch
    --print(message "left=" << toString(left) << _
    --      message " right=" << toString(right))
    if freeVariable?(sk, var)$SU then
      print(message "util coerce rule LS3' applied to: \" << _
        var << message "." << sk << _
        message " giving K \" << var << message "." << _
        left << message " \" << var << _
        message "." << right)
      return ski(K(), ski(left, right))
    print(message "util coerce rule LS5' applied to: \" << _
      var << message "." << sk << _
      message " giving S \" << var << _
      message "." << left << message " \" << _
      var << message "." << right)
    return ski(ski(S()$SU, lambdaOverSki(var, left)), lambdaOverSki(var, right))

  -- 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(lam : LU) : SU ==
    -- test for rule 1
    if atom?(lam)$LU then
      print(message "util coerce rule LS1 applied to:" << _
        lam << message " giving " << lam)
      return ski(var(toString(lam)$LU)$UT)$SU
    if isCompound?(lam)$LU then
      ch : List LU := getChildren(lam)$LU
      c1 : LU := first ch
      c2 : LU := second ch
      print(message "util coerce rule LS2 applied to:" << _
        lam << message " giving (" << c1 << _
        message " " << c2 << message ")")
      return ski(c1::SU, c2::SU)$SU
    if isLambda?(lam)$LU then
      lamUn : LU := unbind(lam)$LU
      c3 : LU := first getChildren(lamUn)$LU
      s3 : UT := getVariable(lam)$LU
      if atom?(c3)$LU then
        if toString(c3)$LU="0" then
          print(message "util coerce rule LS4 applied to:" << _
            lam << message " giving I")
          return I()$SU
      if free?(lam)$LU then
        print(message "util coerce rule LS3 applied to:" << _
          lam << message " giving K " << c3)
        return ski(K(), c3::SU)$SU
      if isLambda?(c3)$LU then
        c33 : LU := first getChildren(c3)$LU
        cxx : LU := lambda(c33, getVariable(c3)$LU)$LU
        print(message "util coerce rule LS5 applied to:" << _
          lam << message " giving \" << s3 << message "." << cxx)
        return lambdaOverSki(s3, cxx::SU)
      if isCompound?(c3) then
        ch3 : List LU := getChildren(c3)$LU
        c31 : LU := first ch3
        c32 : LU := second ch3
        print(message "util coerce rule LS6 applied to:" << _
          lam << message " giving S \" << _
          s3 << message "." << _
          c31 << message " \" << _
          s3 << message "." << c32)
        return ski(ski(S()$SU, lambdaOverSki(s3, c31::SU)), lambdaOverSki(s3, c32::SU))$SU
    print(message "util coerce warning could not match any rule to:" << lam)
    I()$SU

  -- coerce combinators to intuitionistic logic
  -- this is known as the Curry-Howard isomorphism
  -- it uses the following rules:
  -- rule SI1: Ski[Ia] => a -> a,
  -- rule SI2: Ski[Kab] => a -> (b -> a),
  -- rule SI3: Ski[Sabc] => (a -> (b -> c)) -> ((a -> b) -> (a -> c)),
  -- rule SI4: Ski[a a->b] => b
  -- the last rule is function application (modus ponens)
  coerce(s : SU) : ILogic ==
    -- if s is an atom then this means that there are no
    -- parameters for this combinator. If there had been
    -- they would have been found when this was called on
    -- the nodes above it.
    -- I don't know the best way to handle this, really we
    -- need to add the required number of parameters, do
    -- the conversion then remove the parameters just added.
    -- print(message "util coerce called for:" << (toString(s)$SU))
    if atom?(s) then
      --print(message "util coerce atom:" << toString(s)$SU)
      if isI?(s) then
        print(message "warning I does not have a parameter to act on")
        print(message "creating x")
        a :ILogic  := proposition("x")
        return implies(a, a)
      if isK?(s) then
        print(message "warning K does not enough parameters to act on")
        print(message "creating x and y")
        a :ILogic  := proposition("x")
        b :ILogic  := proposition("y")
        return implies(a, implies(b, a))
      if isS?(s) then
        print(message "warning S does not enough parameters to act on")
        print(message "creating x,y and z")
        a :ILogic  := proposition("x")
        b :ILogic  := proposition("y")
        c :ILogic  := proposition("z")
        ab : ILogic  := implies(a, b)
        ac : ILogic  := implies(a, c)
        bc : ILogic  := implies(b, c)
        return implies(implies(a, bc), implies(ab, ac))
      return proposition(getName(getVariable(s)$SU)$UT)
    subnodes : List SU := getChildren(s)$SU
    c1 : SU := first subnodes
    c2 : SU := second subnodes
    --print(message "util coerce c1=" << c1 << message " c2=" << c2)
    -- look for I x, if found translate x
    if isI?(c1) then
      print(message "util coerce apply rule SI1 in:" << s)
      a : ILogic  := c1::ILogic
      return implies(a, a)
    if atom?(c1) then return _\_/(c1::ILogic, c2::ILogic)
    -- look for K x y, if found translate x
    subsubnodes : List SU := getChildren(c1)
    c11 : SU := first subsubnodes
    c12 : SU := second subsubnodes
    --print(message "util coerce c1=" << c1 << _
    --  message " c2=" << c2 << message " c11=" << _
    --  c11 << message " c12=" << c12)
    if isK?(c11) then
      print(message "util coerce apply rule SI2 in:" << s)
      a : ILogic  := c2::ILogic
      b : ILogic  := c12::ILogic
      return implies(a, implies(b, a))
    if atom?(c11) then return _\_/(c1::ILogic, c2::ILogic)
    -- look for S x y z, if found translate (x z)(y z)
    subsubnodes2 : List SU := getChildren(c11)
    c111 : SU := first subsubnodes2
    c112 : SU := second subsubnodes2
    --print(message "util coerce c11=" << c11 << message " c12=" << _
    --       c12 << message " c111=" << c111 << message " c112=" << c112)
    -- look for K x y, if found translate x
    if isS?(c111) then
      print(message "util coerce apply rule SI3 in:" << s)
      a : ILogic  := c2::ILogic
      b : ILogic  := c12::ILogic
      c : ILogic  := c112::ILogic
      ab : ILogic  := implies(a, b)
      ac : ILogic  := implies(a, c)
      bc : ILogic  := implies(b, c)
      return implies(implies(a, bc), implies(ab, ac))
    _\_/(c1::ILogic, c2::ILogic)


)if false

\section{Code Generation Package}
For more information about this package see:
\url{http://www.euclideanspace.com/prog/scratchpad/mycode/computation/codeGen/}

Maps abstract computational structures to real-world FriCAS code.

compCode is a package in the computation framework that allows FriCAS
source code to be created from the abstract structures in the framework.
This is done by the following functions:

\section{writePackage}

'writePackage' creates source code for a FriCAS package from a list of
lambda structures over typed variables. This is reasonably easy to do
since functions in a FriCAS package have a similar structure to lambda
functions.

Parameters are:
\begin{itemize}
  \item list of lambda structures
  \item filename
  \item short name
  \item long name
  \item category name
\end{itemize}

\section{writeCategory}

'writeCategory' creates source code for a FriCAS package from a list of
ILogic structures. This relies on the Curry-Howard isomorphism between
intuitionistic logic and types in a computation.

Parameters are:
\begin{itemize}
  \item list of intuitionistic logic structures
  \item filename
  \item short name
  \item long name
\end{itemize}

Example

In intuitionistic logic if we know 'a' and we know 'a->b' then we can
deduce b (by modus ponens) that is:

\begin{verbatim}
(a /\ (a -> b) ) -> b
\end{verbatim}

Curry-Howard isomorphism relates this intuitionistic logic to types
in a computation so given types 'a' and 'a->b' then we can create
any of these function types without using additional information
(other functions or constants):

\begin{verbatim}
    func1 : (a, a->b) -> a
    func2 : (a, a->b) -> (a->b)
    func3 : (a, a->b) -> b
\end{verbatim}

func3 is more interesting since func1 and func2 can be created by
passing on one of its parameters and throwing away the other.

So how can we implement this? From the original (a /\ (a -> b) )
we need to expand out to (a /\ (a -> b) /\ b) containing all factors.

By the Curry-Howard isomorphism we can coerce to the
intuitionisticLogic from Lambda. This gives an isomorphism where
theorems in intuitionistic logic correspond to type signatures in
combinatory logic and programs in intuitionistic logic correspond
to the proofs of those theorems in combinatory logic.

As an example of this in Haskell see "Djinn, a theorem prover in
Haskell" [2]

see also : Philip Wadler - Theorems for free! [1]
\section{Code Generation Package - Tutorial}
First we may need to expose the required code such as ILOGIC and COMPCODE
\begin{verbatim}
(1) -> )expose COMPCODE
(1) -> )expose ILOGIC
\end{verbatim}
We can generate the source code for a FriCAS package from lambda
expressions. To start we will create some typed variables and lambda
terms to work with:
\begin{verbatim}
(1) -> vx := var("x",proposition("String"))$Typed

   (1)  x:String
                                                        Type: Typed
(2) -> vy := var("y",proposition("String"))$Typed

   (2)  y:String
                                                        Type: Typed
(3) -> nx := lambda(vx)

   (3)  x:String
                                                Type: Lambda(Typed)
(4) -> ny := lambda(vy)

   (4)  y:String
                                                Type: Lambda(Typed)
\end{verbatim}
Now we create some lambda expressions to be converted to source code:
\begin{verbatim}
(5) -> pacEx1 : Lambda Typed := lambda(nx, vx)$Lambda Typed

   (5)  (\x.x)
                                                Type: Lambda(Typed)
(6) -> pacEx2 : Lambda Typed := lambda(pacEx1, vy)$Lambda Typed

   (6)  (\y.(\x.y))
                                                Type: Lambda(Typed)
(7) -> pacEx3 : Lambda Typed := lambda(lambda(nx, ny), vy)$Lambda Typed

   (7)  (\y.(x:String y))
                                                Type: Lambda(Typed)
\end{verbatim}
Now we generate the source code using the writePackage function where:
\begin{itemize}
  \item testComp1.spad is the filename
  \item TESTCCP is the short name
  \item TestCCP is the long name
  \item Type is the category name
\end{itemize}
\begin{verbatim}
(8) -> writePackage([pacEx1,pacEx2,pacEx3],"testGeneratedCode.spad","TESTCCP","TestCCP","Type")
                                                                   Type: Void
\end{verbatim}
When we look at the testComp1.spad file we can see the code that has
been generated:
\begin{verbatim}

)abbrev package TESTCCP TestCCP

TestCCP() : Exports == Implementation where

 Exports ==> Type with

 Implementation ==> add

  fn1(x : String) : String == x
  fn2(y : String) : String ==  x+->(y)
  fn3(y : String) : String ==  x(y)

@
\end{verbatim}
This code may have to be tweaked by hand before it can be used.

Now we can move on to generate the source code for a FriCAS category
from intuitionistic logic expressions. To start we will create some
intuitionistic logic terms as examples:
\begin{verbatim}
(9) -> catEx1:ILogic := implies(proposition("a"),proposition("b"))/\proposition("a")

   (9)  ((a->b)/\a)
                                                       Type: ILogic
(10) -> catEx2:ILogic := proposition("a")/\proposition("b")

   (10)  (a/\b)
                                                       Type: ILogic
\end{verbatim}
Now we generate the source code using the writeCategory function where:
\begin{itemize}
  \item testComp2.spad is the filename
  \item TESTCC is the short name
  \item TestCC is the long name
\end{itemize}
\begin{verbatim}
(11) -> writeCategory([catEx1,catEx2],"testGeneratedCode2.spad","TESTCCP","TestCCP")
                                                                   Type: Void
\end{verbatim}
When we look at the testComp2.spad file we can see the code that has
been generated:
\begin{verbatim}

)abbrev category TESTCC TestCC

TestCC() : Category == Type with


  fn1 : (a->b, a) -> b
  fn2 : (a, b) -> a

@
\end{verbatim}
In fn1 type 'b' was generated from 'a->b' and 'a' (by modus ponens). If
two or more deductions were made then only the first would be used.
In fn2 no additional deductions could be made, in this case the first
parameter is used as the deduction.
\section{package COMPCODE compCode}
)endif

)abbrev package COMPCODE compCode
++ Author: Martin Baker
++ Date Created: June 2011
++ Basic Operations:
++ Related Constructors:
++ Also See:
++ AMS Classifications:
++ Keywords:
++ References:
++ http://www.euclideanspace.com/prog/scratchpad/mycode/computation/codeGen/
++ Description:
++ Maps abstract computational structures to real-world FriCAS code
++
++ This allows FriCAS domains to be created from an instance of
++ Lambda it also allows FriCAS categories to be created from an
++ instance of intuitionisticLogic.
++
++ So by the Curry-Howard isomorphism we can coerce to the
++ intuitionisticLogic from Lambda. This gives an isomorphism where
++ theorems in intuitionistic logic correspond to type signatures in
++ combinatory logic and programs in intuitionistic logic correspond
++ to the proofs of those theorems in combinatory logic.
++
++ As an example of this in Haskell
++ see "Djinn, a theorem prover in Haskell, for Haskell" here:
++ http://lambda-the-ultimate.org/node/1178
++
++ see also: Philip Wadler - Theorems for free!
++ http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html

compCode() : Exports == Implementation where

 NNI==> NonNegativeInteger
 LC ==> Lambda Typed

 Exports ==> with
  writeCategory : (content : List ILogic, filename : String, shortName : String, longName : String) -> Void
    ++ writes a category to a file.
  writePackage : (content : List LC, _
                filename : String, _
                shortName : String, _
                longName : String, _
                catName : String) -> Void
    ++ writes a package to a file.

 Implementation ==> add

  import from Typed
  import from ILogic
  import from List(LC)

  -- used by writeCategory to generate the start of the file
  genCatHeader(shortName : String, longName : String) : List String ==
    [concat([")abbrev category ",shortName," ",longName]),_
     "",_
     concat([longName,"() : Category == Type with"]),_
     "",_
     ""]

  -- used by writeCategory to generate an individual function
  -- declaration
  -- content is the intuitionistic logic expression to be used to
  --      create the function declaration
  -- numb is an integer value that will be used to generate a
  --      unique function name
  genFuncDeclar(content : ILogic, numb : NNI) : List String ==
    fac : List ILogic := factor(content)
    if empty?(fac) then return [concat(["  -- error",_
             toString(content)])]
    deduct : List ILogic := deductions(fac)
    if empty?(deduct) then deduct := fac
    resType : ILogic := first deduct
    resStr : String := concat(["  fn",string(numb),":("])
    notfst : Boolean := false()
    for thisTerm in fac repeat
      if notfst then resStr := concat(resStr,",")
      resStr := concat(resStr, toStringUnwrapped(thisTerm))
      notfst := true()
    resStr := concat([resStr,") -> ",toStringUnwrapped(resType)])
    [resStr]

  -- used by writeCategory to generate the end of the file
  genCatFooter() : List String ==
    ["","@"]

  -- used by writePackage to generate the start of the file
  genPackageHeader(shortName : String, longName : String, catName : String) : List String ==
    [concat([")abbrev package ",shortName," ",longName]),_
     "",_
     concat([longName,"(): Exports == Implementation where"]),_
     "",_
     concat([" Exports ==> ",catName," with"]),_
     "",_
     " Implementation ==> add",_
     ""]

  -- return string representation using conventional notation, that is
  -- deBruijn index is replaced by name using String value for bound variables.
  -- notation assumes association to the left, in the absence of
  -- brackets, the term to the left binds more tightly than the
  -- one on the right.
  genLambdaTerm(n : LC, boundL : List String) : String ==
    s:String := ""
    --print(message "genLambdaTerm(" << toString(n) << ")")
    if isBoundNode?(n) then
      -- convert deBruijn index
      i : NNI := getBoundValue(n) + 1
      if i > 0 and i <= #boundL then return boundL.i
      s := string(i-1)
    if isFreeNode?(n) then
      s := getName(getVariable(n))$Typed
    if isCompound?(n) then
      ch := getChildren(n)
      s := concat([" ",genLambdaTerm(first ch,boundL),"(",genLambdaTerm(second ch,boundL),")"])
    if isLambda?(n) then
      -- nested lambda term so use +->
      varName : String := getName(getVariable(n))$Typed
      while member?(varName, boundL) repeat
        varName := concat(varName,"'")
      boundL2 : List String := concat(boundL, varName)
      ch := getChildren(n)
      s := concat([" ",varName,"+->(",genLambdaTerm(first ch,boundL2),")"])
    s

  -- used by writePackage to generate the function definitions
  -- content is the lambda expression to be used to
  --      create the function definition
  -- numb is an integer value that will be used to generate a
  --      unique function name
  genFuncDefn(content : LC, numb : NNI) : List String ==
    sl := [""]
    if isLambda?(content) then
      var := getVariable(content)
      lhs : String := toString(var)
      lhsn : String := getName(var)
      lhst : String := toStringUnwrapped(getType(var))
      return [concat(["  fn",string(numb),"(",lhs,"):",lhst," == ",_
        genLambdaTerm(first getChildren(content), [lhsn])_
        ])$String]
    sl

  -- used by writePackage to generate the end of the file
  genPackageFooter() : List String ==
    ["","@"]

  -- writes a category to a file.
  writeCategory(content : List ILogic, _
                filename : String, _
                shortName : String, _
                longName : String) : Void ==
    f1:TextFile := open(filename::FileName,"output")
    lines := genCatHeader(shortName, longName)
    -- fnNum is integer used to generate a unique function name
    fnNum : NNI := 1::NNI
    for thisEq in content repeat
      lines := concat(lines, genFuncDeclar(thisEq, fnNum))
      fnNum := fnNum + 1
    lines := concat(lines, genCatFooter())
    for line in lines repeat
      writeLine!(f1, line)
    close! f1

  -- writes a domain to a file.
  writePackage(content : List LC, _
                filename : String, _
                shortName : String, _
                longName : String, _
                catName : String) : Void ==
    f1:TextFile := open(filename::FileName,"output")
    lines := genPackageHeader(shortName, longName, catName)
    -- fnNum is integer used to generate a unique function name
    fnNum : NNI := 1::NNI
    for thisEq in content repeat
      --print(message "writePackage(" << toString(thisEq) << ")")
      lines := concat(lines, genFuncDefn(thisEq, fnNum))
      fnNum := fnNum + 1
    lines := concat(lines, genPackageFooter())
    for line in lines repeat
      writeLine!(f1, line)
    close! f1

--Copyright (c) 2011-2016, Martin J Baker.
--All rights reserved.
--
--Redistribution and use in source and binary forms, with or without
--modification, are permitted provided that the following conditions are
--met:
--
--    - Redistributions of source code must retain the above copyright
--      notice, this list of conditions and the following disclaimer.
--
--    - Redistributions in binary form must reproduce the above copyright
--      notice, this list of conditions and the following disclaimer in
--      the documentation and/or other materials provided with the
--      distribution.
--
--    - Neither the name of Martin J Baker. nor the
--      names of its contributors may be used to endorse or promote products
--      derived from this software without specific prior written permission.
--
--THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
--IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
--TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
--PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
--OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
--EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
--PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
--PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
--LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
--NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
--SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

)if false
\eject
\begin{thebibliography}{99}
For more details see:
[1] Philip Wadler 1989 - Theorems for free!
http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html
[2] "Djinn, a theorem prover in Haskell, for Haskell" here:
http://lambda-the-ultimate.org/node/1178
[3] Roy Dyckhoff 1992 - Contraction-free sequent calculi for intuitionistic logic
[4] http://www.euclideanspace.com/prog/scratchpad/mycode/computation/
[5] Tutorial for lambda calculus:
http://www.euclideanspace.com/prog/scratchpad/mycode/computation/lambda/
[6] Tutorial for SKI calculus:
http://www.euclideanspace.com/prog/scratchpad/mycode/computation/ski/
[7] Tutorial for Intuitionistic Logic
http://www.euclideanspace.com/prog/scratchpad/mycode/discrete/logic/intuitionistic/
[8] Tutorial for utilities to coerce between computation domains
http://www.euclideanspace.com/prog/scratchpad/mycode/computation/utility/
[9] Tutorial for FriCAS source code generation
http://www.euclideanspace.com/prog/scratchpad/mycode/computation/codeGen/
[10] J. Lambek, P. J. Scott 1988
     Introduction to Higher-Order Categorical Logic ISBN : 0521356539
     This book shows the relationship between mathematical logic and category
     theory. Although this is not used in the current code, it suggests
     a promising generalisation.
[11] Peter J. Denning, 2010
Discussion of "What is computing?"
\end{thebibliography}
\end{document}
)endif