perm filename CHURCH[206,LSP] blob sn#485148 filedate 1979-10-24 generic text, type C, neo UTF8
```COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.REQUIRE "206MAC.PUB[206,LSP]" source_file
C00003 00003	.hd206 FALL 1979
C00004 00004	.if false then begin "lam"
C00016 00005	.cb More about \$\$LAMB\$s
C00022 00006	.cb More to do with \$LAMB
C00029 ENDMK
C⊗;
.REQUIRE "206MAC.PUB[206,LSP]" source_file;
.
.
.LSPFONT
.basicops
.
.allops
.itemmac 1;
.
.PORTION MAINPORTION
.hd206 FALL 1979
.PAGE ← 1
.if false then begin "lam"
.bb Continuing problem.

#. This problem deals with representation and manipulation of expressions
in the pure λ-calculus.  The basic properties and
manipulations of \$\$LAMB\$-expressions are defined and you are asked
to write the corresponding programs.  The goal is a program that will
apply a list of reductions to an expression.

The simplest λ-expression is a variable, represented
by a \$\$LAMB\$-variable which is a pair \$\$(X_._n)\$, \$\$n=0,_1,_2,_...\$.
The class, \$\$LAMB\$-expressions, of S-expressions representing λ-expressions
is defined inductively as follows:
.skip 1
.begin preface 0 indent 4,8 group

(i) a \$\$LAMB\$-variable is a \$\$LAMB\$-expression (of sort variable),

(ii) if ⊗e1 and  ⊗e2 are \$\$LAMB\$-expressions then \$\$(APPL e1 e1)\$
is a \$\$LAMB\$-expression (of sort application),

(iii) if ⊗e is a \$\$LAMB\$-expression then for each ⊗n, \$\$(LAMB_n_e)\$
is a \$\$LAMB\$-expression (of sort abstraction),
representing abstraction with respect to the ⊗⊗n⊗th variable \$\$(X_._n)\$.

(iv) These are all of the \$\$LAMB\$-expressions.
.end

##. Write a program ⊗islamb[e] which returns qT if ⊗e is a
\$\$LAMB\$-expression and qNIL otherwise.

[Remark:  you will find programs computing the predicates
⊗var, ⊗appl, and ⊗abstr which are satisfied by the three types of
\$\$LAMB\$-expressions useful, here and later.]

In the following we will use variable to mean \$\$LAMB\$-variable and
expression to mean \$\$LAMB\$-expression.

An occurrence of a variable, ⊗v, in an expression ⊗e,
can be classified as free or bound as follows.
If ⊗e is the variable ⊗v, then the occurrence of ⊗v in ⊗e is free in ⊗e.
If ⊗e is an abstraction on ⊗v, e.g. ⊗e is of the form \$\$(LAMB_n_e1)\$ and
⊗v is \$\$(X_._n)\$ then a free occurrence of ⊗v in ⊗e1 is bound by
this \$\$LAMB\$.  If ⊗e is of the form \$\$(LAMB_n_e1)\$, where ⊗v is not \$\$(X_._N)\$,
then an occurrence of ⊗v (in ⊗⊗e1⊗) is bound or free in ⊗e according as it
is bound or free in ⊗⊗e1⊗.
Similarly, if ⊗e is of the form \$\$(APPL_e1_e2)\$, an occurrence of ⊗v in
in ⊗⊗e1⊗ (resp. ⊗⊗e2⊗) is bound or free in ⊗e according as it
is bound or free in ⊗⊗e1⊗ (resp. ⊗⊗e2⊗).

An occurrence of ⊗v in ⊗e is designated by the list of "moves",
called a ⊗location, necessary to get from ⊗e to the subexpression of ⊗e
which is the occurrence of ⊗v.
If ⊗e is ⊗v then the location is the empty list.
If ⊗e is \$\$(APPL e1 e2)\$ and the occurrence is in \$e1 then the
location is \$A1 followed by the list of moves locating \$v in \$e1.
(similarly if the occurrence is in \$e2, with \$A2 instead of \$\$A1\$.)
If ⊗e is \$\$(LAMB m e1)\$ then the
location is \$B followed by the list of moves locating \$v in \$e1.

##.  Write a program ⊗freeoccs[n,e] that returns a list of locations
of free occurrences of the ⊗⊗n⊗th variable, \$\$(X_._n)\$, in the expression ⊗e.
(You may assume ⊗e to be a \$\$LAMB\$-expression.)__
Thus

⊗⊗⊗freeoccs[\$\$1\$,\$\$(APPL (LAMB 2 (APPL (X.2) (X.2))) (APPL (X.1) (X.1)))\$]=
\$\$((A2 A1)(A2 A2))\$⊗

##. Write a program ⊗substfree[e1,n,e] which substitutes ⊗e1 for
free occurrences of \$\$(X_._n)\$ in ⊗e.

Note that we haven't provided a means to prevent trapping of free variables
of ⊗e1.  If \$\$(X_._m)\$ occurrs free in ⊗e1 and ⊗v occurs free in a subexpression
of ⊗e of the form \$\$(LAMB_m_e2)\$ the occurrence of \$\$(X_._m)\$ in ⊗e1 will
be "trapped" upon substitution.  That is it will be bound in the resulting
expression.  This causes undesired behaviour in the λ-calculus, so we
wish to prevent such substitutions from occuring.

##. Write a program ⊗freefor[e1,n,e] which returns qT if no free variable
of ⊗e1 will become bound upon substitution of ⊗e1 for each free occurrence
of \$\$(X_._n)\$ in ⊗e.

Since we don't want to be stuck just because some expression is not
"freefor" we provide a means of modifying the expression ⊗e
so that ⊗e1 will be free for ⊗v in ⊗e.
This is known as renaming of bound variables.
It is accomplished for a variable \$\$(X_._n)\$, by choosing a variable \$\$(X_._m)\$
that is unused so far and replacing each subexpression of ⊗e of the form
\$\$(LAMB_n_e2)\$ by \$\$(LAMB_m_e3)\$ ⊗e3 is obtained from ⊗e2 by replacing
each occurrence of \$\$(X_._n)\$ in ⊗e2 bound by this \$LAMB by \$\$(X_._m)\$.

##. Write a program ⊗rename[n,m,e] that renames \$\$(X_._n)\$ to \$\$(X_._m)\$
in ⊗e as outlined above.

Now we have all of the basic programs needed to manipulate
\$\$LAMB\$-expressions, carry out reductions, look for normal forms, etc.
For example we can apply a list of reductions to an expression.  There
are two basic reductions.  First, \$\$(ALPHA_n_m)\$ applied to ⊗e is
⊗⊗rename[n,m,e]⊗.  It applies only if \$\$(X_._m)\$ does not occur in ⊗e.
Second, \$BETA applies only to expressions ⊗e of the form \$\$(APPL_e1_e2)\$
where ⊗e1 is an abstraction \$\$(LAMB_n_e3)\$ and ⊗e2 is free for \$\$(X_._n)\$
in ⊗e1.  The result of applying \$BETA to ⊗e is ⊗⊗substfree[e2,n,e1]⊗.
We generalize these reductions to apply to subxexpressions of an
expression ⊗e.  Thus \$\$(ALPHA_n_m_loc)\$ applied to ⊗e is obtained by
replacing the subexpression located at ⊗loc by the result of applying
\$\$(ALPHA_n_m)\$ to that subexpression.  It only applies if ⊗loc is
a valid location in ⊗e and the \$ALPHA reduction applies to that subexpression.
Similarly for \$\$(BETA_loc)\$.

##.  Write a program ⊗⊗LAMB-reduce[e,rlist]⊗ that applies a list of
reductions to a \$\$LAMB\$-expression.
The program should be robust in the following sense.  It should check that
⊗e is a \$\$LAMB\$-expression and return an appropriate message if not.  It
should check each element of ⊗rlist to see that it denotes a reduction and
complain if not.  Before a reduction is applied, a check should be made
that is does indeed apply and appropriate complaints made if not.

.begin nofill group
Some examples follow.  Let

⊗⊗e=\$\$(LAMB_0_(APPL_(X_._1)_(X_._0)))\$⊗
⊗⊗e1=\$\$(LAMB_1_(APPL_(X_._0)_(X_._1)))\$⊗
⊗⊗e2=\$\$(LAMB_2_(APPL_(X_._2)_(X_._1)))\$⊗
⊗⊗e3=\$\$(LAMB_2_(APPL_(X_._2)_(LAMB_1_(APPL_(X_._0)_(X_._1)))))\$⊗
⊗⊗e4=\$\$(APPL (LAMB_1_(LAMB_0_(APPL_(X_._1)_(X_._0))))\$⊗
__________\$\$(LAMB_1_(APPL_(X_._0)_(X_._1))))\$
⊗⊗rlist=\$\$((ALPHA_0_2_NIL) (BETA NIL))\$⊗

then

⊗⊗freefor[e1,\$\$1\$,e]=qNIL⊗
⊗⊗rename[\$\$0\$,\$\$2\$,e]=e2⊗
⊗⊗freefor[e1,\$\$1\$,e2]=qT⊗
⊗⊗substfree[e1,\$\$1\$,e2]=e3⊗
⊗⊗LAMB-reduce[e4,rlist]=e3]⊗
.end

After we discuss sequential programs and I/O, we will see
how ⊗LAMB-reduce can be converted in to an interactive program that
you can have various conversations with about \$\$LAMB\$-expressions.

.END

.end "lam"

This is a continuation of problem 5 in Homework 1.
First a bit of background.
The Lambda-calculus was devised by Alonzo Church in the
1930's to study the concept of computable function.
He developed the λ-notation, set down conversion rules such as
\$ALPHA and \$BETA, and studied the properties of the resulting
system.  He also show how to represent numbers and functions on
numbers in this system.  His monograph
"The Calculi of Lambda-Conversion", Annals of Math. Studies No. 6,
(1941) is an excellent survey of this work.

For your amusement here are some of the things that can be represented
as \$\$LAMB\$-expressions.  The thing being represented is on the
lefthand side of the "→" and the representation is on the right.

#. Positive numbers.
.begin nofill indent 4,4

1 → \$\$(LAMB 1(LAMB 0(APPL(X.1)(X.0))))\$
2 → \$\$(LAMB 1(LAMB 0(APPL(X.1)(APPL(X.1)(X.0)))))\$
3 → \$\$(LAMB 1(LAMB 0(APPL(X.1)(APPL(X.1)(APPL(X.1)(X.0))))))\$
etc.

⊗add1 → \$\$(LAMB 2(LAMB 1(LAMB 0(APPL(X.1)(APPL(APPL(X.2)(X.1))(X.0))))))\$
⊗plus  → \$\$(LAMB 3(LAMB 2(LAMB 1(LAMB 0\$
\$\$_______(APPL(APPL(X.3)(X.1))(APPL(APPL(X.2)(X.1))(X.0)))))))\$
⊗times → \$\$(LAMB 3(LAMB 2(LAMB 1(APPL(X.3)(APPL(X.2)(X.1))))))\$
⊗exp → \$\$(LAMB 3(LAMB 2(APPL(X.3)(X.2))))\$
.end

#. Pairing and selecting the first and second components of a pair.
.begin nofill indent 4,4

⊗pair → \$\$(LAMB 3(LAMB 2(LAMB 1(APPL(APPL(X.1)(X.3))(X.2)))))\$
⊗p1 → \$\$(LAMB 1(APPL(X.1)(LAMB 2(LAMB 3(APPL(APPL(X.3)(LAMB 0(X.0)))(X.2))))))\$
⊗p2 → \$\$(LAMB 1(APPL(X.1)(LAMB 2(LAMB 3(APPL(APPL(X.2)(LAMB 0(X.0)))(X.3))))))\$
.end

#. Tripling and selecting the first, second, and third components of a triple.
.begin nofill indent 4,4

⊗trip → \$\$(LAMB 4(LAMB 3(LAMB 2(LAMB 1 \$
\$\$________(APPL(APPL(APPL(X.1)(X.4))(X.3))(X.2))))))\$
⊗t1 → \$\$(LAMB 1(APPL(X.1)(LAMB 2(LAMB 3(LAMB 4\$
\$\$________(APPL(APPL(APPL(APPL(X.3)\$
\$\$________________(LAMB 0(X.0)))(X.4))(LAMB 0(X.0)))(X.2)))))))\$
⊗t2 → \$\$(LAMB 1(APPL(X.1)(LAMB 2(LAMB 3(LAMB 4\$
\$\$________(APPL(APPL(APPL(APPL(X.2)\$
\$\$________________(LAMB 0(X.0)))(X.4))(LAMB 0(X.0)))(X.3)))))))\$
⊗t3 → \$\$(LAMB 1(APPL(X.1)(LAMB 2(LAMB 3(LAMB 4\$
\$\$________(APPL(APPL(APPL(APPL(X.2)\$
\$\$________________(LAMB 0(X.0)))(X.3))(LAMB 0(X.0)))(X.4)))))))\$
.end

The sense in which the \$\$LAMB\$-expressions represent things, is that
after doing appropriate reductions (and renaming of bound variables)
the result of "applying" the representation of a function to the repsentation
of its argument(s) is a representation of the result of applying the function
to the argument(s) in the ordinary sense.
For example ⊗⊗add1[1]⊗ is represented by the expression
\$\$(APPL λ[add1] λ[1])\$, where \$λ[thing] is shorthand for the \$\$LAMB\$-representation
of \$thing as given above.  As a \$\$LAMB\$-expression it be reduces to the
expression representing 2.  Given any two expressions \$e1, \$e2,
\$\$(APPL(APPL λ[pair] e1) e2)\$ represents the ⊗pair[e1,e2] and
\$\$(APPL λ[p1] (APPL(APPL λ[pair] e1) e2))\$ represents ⊗p1[pair[e1,e2]] and
as a \$\$LAMB\$-expression reduces to \$e1 as it should.
Thus arithmetic is represented accurately (on representations of numbers)
and the representations ⊗pair,p1,p2 obey rules similar to those for
qqa, qqd, and qcons acting on S-expressions.
The representations of ⊗trip,t1,t2,t3 behave analogously.

You should use these ideas to exercise your interpreter and try out
some non-trivial reductions which have some meaning.

.cb More to do with \$LAMB
.item ← 0

#.  Using the basic routines for manipulating \$LAMBs you can
write an interactive interpreter that will accept a variety of
commands and take appropriate actions.  Here are some ideas.

##.  A \$DEFINE command to give names to particular \$\$LAMB\$-expressions.
You should then extend the ability to recognize expressions to include
defined names where ever an expression could occur.  Thus if \$ONE and
\$add1 were defined as above \$\$(APPL add1 ONE)\$ would be a valid expression
and should be expanded by your interpreter using the definition before
attempting to any computation with the expression.

##.  An \$ALPHA command that takes an expression and two numbers
(and possibly a subexpression designation) and does an \$ALPHA conversion.

##.  A \$BETA command that takes an expression
(and possibly a subexpression designation) and does an \$BETA conversion
if allowed.

##.  A \$BETA! command that takes an expression
(and possibly a subexpression designation) and does an \$BETA conversion
first doing any necessary remaning of bound variables.  Thus it will
have to discover what variables are to be renamed and figure out
a safe name (for example \$(X.n) for the least \$n such that \$(X.n) doesn't
occur in the given expression).

##. Commands for building sequences of reductions.   One way is to have
a notion of current reduction (undefined initially).  Each sequence
should have a name so you can switch to that as the current reduction.
You will need a command to start a new reduction which should take a name
and an expression, to be the first member of the sequence.
The above reduction commands can apply to the some element
of the reduction sequence to extend it.  The command for switching attention
to a new current reduction sequence should save the old one in such a manner
that it can be retrieved by name later.  (Association lists and property lists
are good for such things.)  You will also need a command to print any
given reduction sequence.

##.  Any other commands that seem like fun to implement.

.if lines≤10 then next page;

#.  As a basis for your LAMB interpreter you should have programs
⊗islamb, ⊗mklamb, ⊗bvarof, ⊗body, ⊗isappl, ⊗mkappl, ⊗funof, ⊗argof and
⊗isvar to test for, construct and take apart the various types
of \$\$LAMB\$-expressions.  Such auxiliary programs make the main
programs more readable, but require extra function calls when
these programs are executed.  You should replace these auxiliary
program definitions by suitable \$MACRO definitions.  This helps
make readability and efficiency more compatible.

#.  Modify the error checking parts of your program to use the MACLISP
primitives \$CATCH and \$THROW.  Cleverly done this can get the
appropriate message to the appropriate place without explicitly
carrying around an extra parameter, or checking every time
a called routine returns to see if it succeeded.

#.  You may have noticed that the notation for \$\$LAMB\$-expressions
is not as compact or flexible as it might be.  Devise some
``shorthand'' that your interpreter can understand.  It should
read the short forms, convert to standard form for manipulation,
and print the results in some standard shorthand.
Some possible abbreviations are:
.begin nofill select 6 indent 8,8

(LAMB n (LAMB m body)) ↔ (LAMB (n m) body)
(APPL (APPL e1 e2) e3) ↔ (APPL e1 e2 e3)
.end
You may wish to think up fancier ones.