computation5.patch

From 4c1adeacdcf45f145ad8ab47a5283bccc96c359e Mon Sep 17 00:00:00 2001
From: martinbaker <ax87438@martinb.com>
Date: Wed, 21 Sep 2016 17:28:05 +0100
Subject: [PATCH 5/5] documentation changes only

---
 src/algebra/computation.spad | 721 ++++++++++++++-----------------------------
 1 file changed, 234 insertions(+), 487 deletions(-)

diff --git a/src/algebra/computation.spad b/src/algebra/computation.spad
index fdf75ea..0731cf4 100644
--- a/src/algebra/computation.spad
+++ b/src/algebra/computation.spad
@@ -259,217 +259,6 @@ 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{Intuitionistic Logic}
-The intuitionisticLogic domain implements a Heyting algebra implied
-by intuitionistic logic similar to boolean algebra.
-
-Intuitionistic or constructive logic is similar to classical logic
-but where the law of excluded middle is not used.
-
-The implementation starts with a 'free logic algebra' that is an
-algebra where each combination of inputs to /\ , \/ and - generates
-a new element. So an expression like T /\ T is just T /\ T and does
-not simplify.
-
-Then by adding "simplification rules" (should I have called them
-relators?) then other logic algebras can be implemented (intuitional,
-ternary, many-valued, boolean) just by adding the "rules".
-
-These "rules" are hardcoded into the /\ , \/ and - implementations
-(rather than implementing a true rule based system).
-
-Simplification rules :
-
-    ~T -> _|_
-    ~(~T) -> T
-    ~x /\ x -> _|_
-    x /\ ~x -> _|_
-    x /\ x -> x
-    _|_ /\ x -> _|_
-    x /\ _|_ -> _|_
-    T \/ x -> T
-    x \/ T -> T
-    x \/ x -> x
-    x /\ T -> x
-    T /\ x -> x
-    x \/ _|_ -> x
-    _|_ \/ x -> x
-
-where:
-
-    T = true
-    _|_ = false
-    x = arbitrary proposition
-
-An option to generalize this code might be to implement the 'free
-logic algebra' as a category, then intuitional, ternary, many-valued,
-boolean could be domains which overload /\ , \/ and - with their own
-sets of rules.
-
-Note : Please be aware that changes may be made in the future to improve
-      and correct intuitionistic logic domain, such as:
-\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.
-\end{itemize}
-\section{Intuitionistic Logic Tutorial}
-Intuitionistic logic has many possible values : true $T$, false $_|_$ and
-infinitely many other values generated by constructs such as inverse.
-These can be constructed as follows:
-
-\begin{verbatim}
-(1) -> logicF()
-
-   (1)  "_|_"
-                                                             Type : ILogic
-(2) -> logicT()
-
-   (2)  "T"
-                                                             Type : ILogic
-(3) -> ~logicT()
-
-   (3)  "_|_"
-                                                             Type : ILogic
-\end{verbatim}
-
-This logic has different rules from boolean algebra and all constructions
-do not reduce to true or false. To test out our constructs we will use
-the following list:
-
-\begin{verbatim}
-(4) -> l:List ILogic := [logicF(),logicT(),proposition("a"),~proposition("a"),proposition("b"),~proposition("b")]
-
- LISP output:
-((0 F) (0 T) (1 a) (3 NOT 1 a) (1 b) (3 NOT 1 b))
-                                                       Type : List(ILogic)
-\end{verbatim}
-
-First we will try 'not':
-\begin{verbatim}
-(5) -> [(~j)::OutputForm for j in l]
-
-   (5)  ["~(_|_)","_|_","~(a)","~(~(a))","~(b)","~(~(b))"]
-                                                   Type : List(OutputForm)
-\end{verbatim}
-
-We can print a truth table for 'and' and 'or'. This is the same as
-boolean logic for true/false values and extended for the unproven case.
-\begin{verbatim}
-(6) -> matrix[ [(k /\ j)::OutputForm for j in l] for k in l]
-
-     (6)
-    SUB
-       matrix
-       ["_|_","_|_","_|_","_|_","_|_","_|_"]
-      ["_|_","T","a","~(a)","b","~(b)"]
-      ["_|_","a","a","_|_","(a/\b)","(a/\~(b))"]
-      ["_|_","~(a)","_|_","~(a)","(~(a)/\b)","(~(a)/\~(b))"]
-      ["_|_","b","(b/\a)","(b/\~(a))","b","_|_"]
-      ["_|_","~(b)","(~(b)/\a)","(~(b)/\~(a))","_|_","~(b)"]
-                                                               Type : Symbol
-
-Note : Its hard to read this table in text, it displays better as
-html on this page:
-http://www.euclideanspace.com/prog/scratchpad/mycode/discrete/logic/intuitionistic/
-
-(7) -> matrix[ [(k \/ j)::OutputForm for j in l] for k in l]
-
-     (7)
-    SUB
-       matrix
-      ["_|_","T","a","~(a)","b","~(b)"]
-      ["T","T","T","T","T","T"]
-      ["a","T","a","(a\/~(a))","(a\/b)","(a\/~(b))"]
-      ["~(a)","T","(~(a)\/a)","~(a)","(~(a)\/b)","(~(a)\/~(b))"]
-      ["b","T","(b\/a)","(b\/~(a))","b","(b\/~(b))"]
-      ["~(b)","T","(~(b)\/a)","(~(b)\/~(a))","(~(b)\/b)","~(b)"]
-
-                                                               Type : Symbol
-\end{verbatim}
-
-'implies' produces the following truth table.
-\begin{verbatim}
-(8) -> matrix[ [implies(k, j)::OutputForm for j in l] for k in l]
-
-
-   (8)
-    SUB
-       matrix
-       ["T","T","(_|_->a)","(_|_->~(a))","(_|_->b)","(_|_->~(b))"]
-       ["_|_","T","(T->a)","(T->~(a))","(T->b)","(T->~(b))"]
-       ["(a->_|_)","(a->T)","(a->a)","(a->~(a))","(a->b)","(a->~(b))"]
-       ["(~(a)->_|_)", "(~(a)->T)", "(~(a)->a)", "(~(a)->~(a))", "(~(a)->b)",
-        "(~(a)->~(b))"]
-       ["(b->_|_)","(b->T)","(b->a)","(b->~(a))","(b->b)","(b->~(b))"]
-       ["(~(b)->_|_)", "(~(b)->T)", "(~(b)->a)", "(~(b)->~(a))", "(~(b)->b)",
-        "(~(b)->~(b))"]
-                                                               Type : Symbol
-\end{verbatim}
-
-Now that we can do intuitionistic logic with constant values we can
-go on to represent theories. We can enter a symbolic value as follows:
-\begin{verbatim}
-(9) -> proposition("p1")
-
-   (9)  "p1"
-                                                             Type : ILogic
-\end{verbatim}
-
-When applying a symbolic value, then it may not possible to compress
-as a single node, so the result remains as a tree. So (13) can be
-reduced to a single value $_|_$, because the result does not depend
-on \verb'a', however in (12) we cannot reduce to a single value.
-\begin{verbatim}
-(10) -> proposition("a") /\ proposition("b")
-
-   (10)  "(a/\b)"
-                                                             Type : ILogic
-(11) -> implies(proposition("a"),proposition("b"))
-
-   (11)  "(a->b)"
-                                                             Type : ILogic
-(12) -> proposition("a") /\ logicT()
-
-   (12)  "a"
-                                                             Type : ILogic
-(13) -> proposition("a") /\ logicF()
-
-   (13)  "_|_"
-                                                             Type : ILogic
-\end{verbatim}
-\section{applying modus ponens}
-modus ponens tells us that given : 'a' and 'a->b' then we can imply 'b'.
-So we first assert 'a' and 'a->b' as follows:
-\begin{verbatim}
-(14) -> givens := proposition("a") /\ implies(proposition("a"),proposition("b"))
-
-   (14)  "(a/\(a->b))"
-                                                             Type : ILogic
-\end{verbatim}
-We then factor into separate terms:
-\begin{verbatim}
-(15) -> fgivens := factor(givens)
-
- LISP output:
-((1 a) (2 . UNPRINTABLE))
-                                                       Type : List(ILogic)
-\end{verbatim}
-note : List ILOGIC to OutputForm is fixed in latest FriCAS so it will
-now display : [a, a->b]
-
-We now apply the deductions function to this list.
-\begin{verbatim}
-(16) -> deduct := deductions(fgivens)
-
- LISP output:
-((1 b))
-                                                       Type : List(ILogic)
-\end{verbatim}
-so we get the required deduction 'b'
-
-
 \section{Variables}
 Before we get on to the main domains we have some code to represent
 variables in Lambda and Ski domains.
@@ -491,20 +280,20 @@ follows:
 
 \begin{verbatim}
 (1) -> var("x")$Untyped
-   (1)  "x"
-                                                            Type : Untyped
+   (1)  x
+                                                             Type: Untyped
 (2) -> var("x",proposition("a"))$Typed
-   (2)  "x:a"
-                                                              Type : Typed
+   (2)  x:a
+                                                               Type: Typed
 (3) -> parseVar("x:(a->b)")$Typed
-   (3)  "x:(a->b)"
-                                                              Type : Typed
+   (3)  x:(a->b)
+                                                               Type: Typed
 (4) -> parseVar("x:(a/\b)")$Typed
-   (4)  "x:(a/\b)"
-                                                              Type : Typed
+   (4)  x:(a/\b)
+                                                               Type: Typed
 (5) -> parseVar("x:(a\/b)")$Typed
-   (5)  "x:(a\/b)"
-                                                              Type : Typed
+   (5)  x:(a\/b)
+                                                               Type: Typed
 \end{verbatim}
 (1) shows an untyped variable.
 
@@ -536,8 +325,8 @@ of both computation and in pure mathematical terms, for example:
 \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 in a flexibly way
-we must build our own type domains rather than use the types used by
+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).
 
@@ -924,9 +713,8 @@ 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
+                                                           Type: Type
 \end{verbatim}
 
 \section{Constructors}
@@ -948,19 +736,14 @@ 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)
-
+   (2)  x
+                                                    Type: Lambda(Untyped)
 (3) -> v2 := lambda(var("y")$Untyped)$UNTYP
-
-   (3)  "y"
-                                                    Type : Lambda(Untyped)
-
+   (3)  y
+                                                    Type: Lambda(Untyped)
 (4) -> v3 := lambda(0)$UNTYP
-
-   (4)  "0"
-                                                    Type : Lambda(Untyped)
+   (4)  0
+                                                    Type: Lambda(Untyped)
 \end{verbatim}
 
 This can be built up into more complex lambda terms by using compound
@@ -971,14 +754,11 @@ 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)
-
+   (5)  (x y)
+                                                    Type: Lambda(Untyped)
 (6) -> n2 := lambda(n1,var("x")$Untyped)$UNTYP
-
-   (6)  "(\x.(x y))"
-                                                    Type : Lambda(Untyped)
+   (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,
@@ -995,25 +775,20 @@ 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
+                                                             Type: String
 (8) -> n3 := lambda(v3,var("x")$Untyped)$UNTYP
-
-   (8)  "(\x.x)"
-                                                    Type : Lambda(Untyped)
+   (8)  (\x.x)
+                                                    Type: Lambda(Untyped)
 (9) -> u2 := unbind(n2)$UNTYP
-
-   (9)  "(\x.(x y))"
-                                                    Type : Lambda(Untyped)
+   (9)  (\x.(x y))
+                                                    Type: Lambda(Untyped)
 (10) -> toString(u2)$UNTYP
-
    (10)  "(\x.(x y))"
-                                                             Type : String
+                                                             Type: String
 (11) -> toString(bind(u2))$UNTYP
-
    (11)  "(\x.(0 y))"
-                                                             Type : String
+                                                             Type: String
 \end{verbatim}
 
 So we can already construct any type of lambda term, however its a bit
@@ -1027,39 +802,33 @@ 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)
+   (12)  (\x.(\y.(x y)))
+                                                    Type: Lambda(Untyped)
 (13) -> toString(n4)$UNTYP
-
    (13)  "(\x.(\y.(0 1)))"
-                                                             Type : String
+                                                             Type: String
 (14) -> n4a := parseLambda("\x.\x. 0 1")$UNTYP
-
-   (14)  "(\x.(\x'.(x x')))"
-                                                    Type : Lambda(Untyped)
+   (14)  (\x.(\x'.(x x')))
+                                                    Type: Lambda(Untyped)
 (15) -> toString(n4a)$UNTYP
-
    (15)  "(\x.(\x.(0 1)))"
-                                                             Type : String
+                                                             Type: String
 (16) -> unbind(n4a)$UNTYP
-
-   (16)  "(\x.(\x'.(x x)))"
-                                                    Type : Lambda(Untyped)
+   (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:
+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)
+   (17)  (\x.(x y))
+                                                    Type: Lambda(Untyped)
 (18) -> subst(n2, v1, v2)$UNTYP
-
-   (18)  "(\x.(x x))"
-                                                    Type : Lambda(Untyped)
+   (18)  (\x.(x x))
+                                                    Type: Lambda(Untyped)
 \end{verbatim}
 
 \section{Issues}
@@ -1677,51 +1446,48 @@ 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:
+\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)
-
+   (2)  I
+                                      Type: SKICombinators(Untyped)
 (3) -> m2 := K()$UNTYP
 
-   (3)  "K"
-                                              Type : SKICombinators(Untyped)
-
+   (3)  K
+                                      Type: SKICombinators(Untyped)
 (4) -> m3 := S()$UNTYP
 
-   (4)  "S"
-                                              Type : SKICombinators(Untyped)
-
+   (4)  S
+                                      Type: SKICombinators(Untyped)
 (5) -> v1 := ski(var("x")$Untyped)$UNTYP
 
-   (5)  "x"
-                                              Type : SKICombinators(Untyped)
-
+   (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:
-
-    In n2 the second term is an atom so brackets are not required.
-    In n3 the second term is compound so brackets are required.
+\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)
-
+   (6)  IK
+                                      Type: SKICombinators(Untyped)
 (7) -> n2 := ski(n1, m3)$UNTYP
 
-   (7)  "IKS"
-                                              Type : SKICombinators(Untyped)
+   (7)  IKS
+                                      Type: SKICombinators(Untyped)
 (8) -> n3 := ski(m3, n1)$UNTYP
 
-   (8)  "S(IK)"
-                                              Type : SKICombinators(Untyped)
+   (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
@@ -1740,12 +1506,12 @@ character.
 \begin{verbatim}
 (9) -> n4 := parseSki("IKS")$UNTYP
 
-   (9)  "IKS"
-                                              Type : SKICombinators(Untyped)
+   (9)  IKS
+                                      Type: SKICombinators(Untyped)
 (10) -> n5 := parseSki("S(IK)")$UNTYP
 
-   (10)  "S(IK)"
-                                              Type : SKICombinators(Untyped)
+   (10)  S(IK)
+                                      Type: SKICombinators(Untyped)
 \end{verbatim}
 \section{redux}
 
@@ -1758,42 +1524,39 @@ combinator:
 \begin{verbatim}
 (11) -> s1 := parseSki("Ix")$UNTYP
 
-   (11)  "I x"
-                                              Type : SKICombinators(Untyped)
+   (11)  I x
+                                      Type: SKICombinators(Untyped)
 (12) -> redux(s1)$UNTYP
+   x
 
-x
-
-   (12)  "x"
-                                              Type : SKICombinators(Untyped)
+   (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)
+   (13)  K x y
+                                      Type: SKICombinators(Untyped)
 (14) -> redux(s2)$UNTYP
+   x
 
-x
-
-   (14)  "x"
-                                              Type : SKICombinators(Untyped)
+   (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)
+   (15)  S x y z
+                                      Type: SKICombinators(Untyped)
 (16) -> redux(s3)$UNTYP
+   x z(y z)
 
-x z(y z)
-
-   (16)  "x z(y z)"
-                                              Type : SKICombinators(Untyped)
+   (16)  x z(y z)
+                                      Type: SKICombinators(Untyped)
 \end{verbatim}
 \section{Secondary Combinators}
 
@@ -1820,27 +1583,24 @@ equivalent to I
 reverses its operands.
 \begin{verbatim}
 (17) -> redux(parseSki("SKKx y")$UNTYP)$UNTYP
+   K x(K x) y
+   x y
 
-K x(K x)y
-x y
-
-   (17)  "x y"
-                                              Type : SKICombinators(Untyped)
+   (17)  x y
+                                      Type: SKICombinators(Untyped)
 (18) -> redux(parseSki("S(KS)x y")$UNTYP)$UNTYP
+   KS y(x y)
+   S(x y)
 
-KS y(x y)
-S(x y)
-
-   (18)  "S(x y)"
-                                              Type : SKICombinators(Untyped)
+   (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
 
-K(SI)x(K x)y
-Iy(Kx y)
-y x
-
-   (19)  "y x"
-                                              Type : SKICombinators(Untyped)
+   (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
@@ -2284,11 +2044,11 @@ SU to simplify notation:
 (1) -> LU := Lambda Untyped
 
    (1)  Lambda(Untyped)
-                                                               Type : Type
+                                                         Type: Type
 (2) -> SU := SKICombinators Untyped
 
    (2)  SKICombinators(Untyped)
-                                                               Type : Type
+                                                         Type: Type
 \end{verbatim}
 \section{SKI combinators to lambda functions}
 
@@ -2309,24 +2069,20 @@ 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
 
-util coerce rule SL1 : Ski[I] = \v0.0
-
-   (3)  "(\v0.v0)"
-                                                    Type : Lambda(Untyped)
-
+   (3)  (\v0.v0)
+                                              Type: Lambda(Untyped)
 (4) -> K()$SU::LU
-\end{verbatim}
-util coerce rule \verb'SL2 : Ski[K] = \v0.\v1.1'
-\begin{verbatim}
-   (4)  "(\v0.(\v1.v1))"
-                                                    Type : Lambda(Untyped)
+   util coerce rule SL2: Ski[K] = \v0.\v1.1
+
+   (4)  (\v0.(\v1.v1))
+                                              Type: Lambda(Untyped)
 (5) -> S()$SU::LU
-\end{verbatim}
-util coerce rule \verb'SL3 : Ski[S] = \v0.\v1.\v2.(2 0 (1 0))'
-\begin{verbatim}
-   (5)  "(\v0.(\v1.(\v2.(v2 (v0 (v1 v0))))))"
-                                                    Type : Lambda(Untyped)
+   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
@@ -2341,61 +2097,62 @@ parameters. This conversion works by applying the following rules:
 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
 
-util coerce apply rule SL1 in : I a
-util coerce pass unbound variable a unchanged
-
-   (6)  "a"
-                                                    Type : Lambda(Untyped)
+   (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
 
-util coerce apply rule SL2 in : K a b
-util coerce pass unbound variable a unchanged
-
-   (7)  "a"
-                                                    Type : Lambda(Untyped)
+   (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
 
-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)
+   (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)
+   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
+   util coerce rule SL4: Ski[(S(K(SI)) S(KK)I)] = (Ski[S(K(SI))] Ski[S(KK)I])
+   util coerce rule SL4: Ski[(S K(SI))] = (Ski[S] Ski[K(SI)])
+   util coerce rule SL3: Ski[S] = \v0.\v1.\v2.(2 0 (1 0))
+   util coerce rule SL4: Ski[(K SI)] = (Ski[K] Ski[SI])
+   util coerce rule SL2: Ski[K] = \v3.\v4.1
+   util coerce rule SL4: Ski[(S I)] = (Ski[S] Ski[I])
+   util coerce rule SL3: Ski[S] = \v5.\v6.\v7.(2 0 (1 0))
+   util coerce rule SL1: Ski[I] = \v8.0
+   util coerce rule SL4: Ski[(S(KK) I)] = (Ski[S(KK)] Ski[I])
+   util coerce rule SL4: Ski[(S KK)] = (Ski[S] Ski[KK])
+   util coerce rule SL3: Ski[S] = \v9.\v10.\v11.(2 0 (1 0))
+   util coerce rule SL4: Ski[(K K)] = (Ski[K] Ski[K])
+   util coerce rule SL2: Ski[K] = \v12.\v13.1
+   util coerce rule SL2: Ski[K] = \v14.\v15.1
+   util coerce rule SL1: Ski[I] = \v16.0
 
    (10)
-  "(((\v0.(\v1.(\v2.(v2 (v0 (v1 v0)))))) ((\v3.(\v4.v4)) ((\v5.(\v6.(\v7.(v7 (v
-  5 (v6 v5)))))) (\v8.v8)))) (((\v9.(\v10.(\v11.(v11 (v9 (v10 v9)))))) ((\v12.(
-  \v13.v13)) (\v14.(\v15.v15)))) (\v16.v16)))"
-                                                    Type : Lambda(Untyped)
+   (
+     ((\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}
@@ -2420,48 +2177,43 @@ eliminated.
 Here are some examples:
 \begin{verbatim}
 (11) -> parseLambda("x")$LU::SU
+   util coerce rule LS1 applied to:x giving x
 
-util coerce rule LS1 applied to : x giving x
-
-   (11)  "x"
-                                              Type : SKICombinators(Untyped)
+   (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
 
-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)
+   (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
 
-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)
+   (13)  K 1
+                                      Type: SKICombinators(Untyped)
 (14) -> parseLambda("\x.0")$LU::SU
+   util coerce warning could not match any rule to:(\x.x)
 
-util coerce warning could not match any rule to : (\x.0)
-
-   (14)  "I"
-                                              Type : SKICombinators(Untyped)
+   (14)  I
+                                      Type: SKICombinators(Untyped)
 (15) -> parseLambda("\x.\y.0 1")$LU::SU
-
-util coerce rule LS5 applied to : (\x.(\y.(0 1))) giving \x.(\y.(0 x))
-util coerce rule LS6 applied to : (\y.(0 x)) giving S \y.y \y.x
-util coerce rule LS1 applied to : y giving y
-util coerce rule LS4' applied to : \y.y giving I
-util coerce rule LS1 applied to : x giving x
-util coerce rule LS3' applied to : \y.x giving K x
-util coerce rule LS5' applied to : \x.SI(Kx) giving S \x.SI \x.Kx
-util coerce rule LS3' applied to : \x.SI giving K \x.S \x.I
-util coerce rule LS5' applied to : \x.Kx giving S \x.K \x.x
-util coerce rule LS3' applied to : \x.K giving K K
-util coerce rule LS4' applied to : \x.x giving I
-
-   (15)  "S(K(SI))(S(KK)I)"
-                                              Type : SKICombinators(Untyped)
+   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}
 
@@ -2485,31 +2237,27 @@ 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 : Ia
-warning I does not have a parameter to act on
-creating x
-
-   (16)  "((x->x)->(x->x))"
-                                                             Type : ILogic
-(17) -> parseSki("Ka b")$SU::ILogic
-
-util coerce apply rule SI2 in : K a b
-
-   (17)  "(b->(a->b))"
-                                                             Type : ILogic
-(18) -> parseSki("K(a b)c")$SU::ILogic
-
-util coerce apply rule SI2 in : K(a b) c
-
-   (18)  "(c->((a\/b)->c))"
-                                                             Type : ILogic
-(19) -> parseSki("Sa b c")$SU::ILogic
-
-util coerce apply rule SI3 in : S a b c
-
-   (19)  "((c->(b->a))->((c->b)->(c->a)))"
-                                                             Type : ILogic
+   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}
@@ -2945,35 +2693,35 @@ terms to work with:
 \begin{verbatim}
 (1) -> vx := var("x",proposition("String"))$Typed
 
-   (1)  "x:String"
-                                                              Type : Typed
+   (1)  x:String
+                                                        Type: Typed
 (2) -> vy := var("y",proposition("String"))$Typed
 
-   (2)  "y:String"
-                                                              Type : Typed
+   (2)  y:String
+                                                        Type: Typed
 (3) -> nx := lambda(vx)
 
-   (3)  "x"
-                                                      Type : Lambda(Typed)
+   (3)  x:String
+                                                Type: Lambda(Typed)
 (4) -> ny := lambda(vy)
 
-   (4)  "y"
-                                                      Type : Lambda(Typed)
+   (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)
+   (5)  (\x.x)
+                                                Type: Lambda(Typed)
 (6) -> pacEx2 : Lambda Typed := lambda(pacEx1, vy)$Lambda Typed
 
-   (6)  "(\y.(\x.y))"
-                                                      Type : Lambda(Typed)
+   (6)  (\y.(\x.y))
+                                                Type: Lambda(Typed)
 (7) -> pacEx3 : Lambda Typed := lambda(lambda(nx, ny), vy)$Lambda Typed
 
-   (7)  "(\y.(x y))"
-                                                      Type : 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}
@@ -2983,8 +2731,8 @@ Now we generate the source code using the writePackage function where:
   \item Type is the category name
 \end{itemize}
 \begin{verbatim}
-(8) -> writePackage([pacEx1,pacEx2,pacEx3],"testComp1.spad","TESTCCP","TestCCP","Type")
-                                                               Type : Void
+(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:
@@ -3012,12 +2760,12 @@ intuitionistic logic terms as examples:
 \begin{verbatim}
 (9) -> catEx1:ILogic := implies(proposition("a"),proposition("b"))/\proposition("a")
 
-   (9)  "((a->b)/\a)"
-                                                             Type : ILogic
+   (9)  ((a->b)/\a)
+                                                       Type: ILogic
 (10) -> catEx2:ILogic := proposition("a")/\proposition("b")
 
-   (10)  "(a/\b)"
-                                                                 Type : ILogic
+   (10)  (a/\b)
+                                                       Type: ILogic
 \end{verbatim}
 Now we generate the source code using the writeCategory function where:
 \begin{itemize}
@@ -3026,9 +2774,8 @@ Now we generate the source code using the writeCategory function where:
   \item TestCC is the long name
 \end{itemize}
 \begin{verbatim}
-(11) -> writeCategory([catEx1,catEx2],"testComp2.spad","TESTCC","TestCC")
-
-                                                                   Type : Void
+(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:
@@ -3232,7 +2979,7 @@ compCode() : Exports == Implementation where
       writeLine!(f1, line)
     close! f1
 
---Copyright (c) 2011, Martin J Baker.
+--Copyright (c) 2011-2016, Martin J Baker.
 --All rights reserved.
 --
 --Redistribution and use in source and binary forms, with or without
-- 
2.1.4