/LMAR=0/XLINE=3/FONT#0=BAXL30[FNT,CLT]/FONT#1=BAXM30/FONT#2=BAXB30[FNT,CLT]/FONT#5=GACS25/FONT#3=SUB/FONT#4=SUP/FONT#7=SYMB30[FNT,CLT]

␈↓ ↓H␈↓␈↓ ∧+COMPUTER SCIENCE DEPARTMENT
␈↓ ↓H␈↓␈↓ ¬πSTANFORD UNIVERSITY
␈↓ ↓H␈↓CS206  ␈↓ βiRECURSIVE PROGRAMMING AND PROVING ␈↓ 
0FALL 1979

␈↓ ↓H␈↓α␈↓ ¬QMore about ␈↓¬LAMB␈↓αs

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

␈↓ ↓H␈↓For␈α∞your␈α∂amusement␈α∞here␈α∂are␈α∞some␈α∂of␈α∞the␈α∞things␈α∂that␈α∞can␈α∂be␈α∞represented␈α∂as␈α∞␈↓¬LAMB␈↓-expressions.
␈↓ ↓H␈↓The␈α
thing␈α
being␈α
represented␈α
is␈α
on␈α
the␈α
lefthand␈α
side␈α
of␈α
the␈α
"→"␈α
and␈α
the␈α
representation␈α
is␈α
on␈α
the
␈↓ ↓H␈↓right.

␈↓ ↓H␈↓1. Positive numbers.

␈↓ ↓H␈↓␈↓ αλ1 → ␈↓¬(LAMB 1(LAMB 0(APPL(X.1)(X.0))))␈↓
␈↓ ↓H␈↓␈↓ αλ2 → ␈↓¬(LAMB 1(LAMB 0(APPL(X.1)(APPL(X.1)(X.0)))))␈↓
␈↓ ↓H␈↓␈↓ αλ3 → ␈↓¬(LAMB 1(LAMB 0(APPL(X.1)(APPL(X.1)(APPL(X.1)(X.0))))))␈↓
␈↓ ↓H␈↓␈↓ αλetc.

␈↓ ↓H␈↓␈↓ αλ␈↓↓add1␈↓ → ␈↓¬(LAMB 2(LAMB 1(LAMB 0(APPL(X.1)(APPL(APPL(X.2)(X.1))(X.0))))))␈↓
␈↓ ↓H␈↓␈↓ αλ␈↓↓plus␈↓  → ␈↓¬(LAMB 3(LAMB 2(LAMB 1(LAMB 0␈↓
␈↓ ↓H␈↓␈↓ αλ         ␈↓¬       (APPL(APPL(X.3)(X.1))(APPL(APPL(X.2)(X.1))(X.0)))))))␈↓
␈↓ ↓H␈↓␈↓ αλ␈↓↓times␈↓ → ␈↓¬(LAMB 3(LAMB 2(LAMB 1(APPL(X.3)(APPL(X.2)(X.1))))))␈↓
␈↓ ↓H␈↓␈↓ αλ␈↓↓exp␈↓ → ␈↓¬(LAMB 3(LAMB 2(APPL(X.3)(X.2))))␈↓

␈↓ ↓H␈↓2. Pairing and selecting the first and second components of a pair.

␈↓ ↓H␈↓␈↓ αλ␈↓↓pair␈↓ → ␈↓¬(LAMB 3(LAMB 2(LAMB 1(APPL(APPL(X.1)(X.3))(X.2)))))␈↓
␈↓ ↓H␈↓␈↓ αλ␈↓↓p1␈↓ → ␈↓¬(LAMB 1(APPL(X.1)(LAMB 2(LAMB 3(APPL(APPL(X.3)(LAMB 0(X.0)))(X.2))))))␈↓
␈↓ ↓H␈↓␈↓ αλ␈↓↓p2␈↓ → ␈↓¬(LAMB 1(APPL(X.1)(LAMB 2(LAMB 3(APPL(APPL(X.2)(LAMB 0(X.0)))(X.3))))))␈↓

␈↓ ↓H␈↓3. Tripling and selecting the first, second, and third components of a triple.

␈↓ ↓H␈↓␈↓ αλ␈↓↓trip␈↓ → ␈↓¬(LAMB 4(LAMB 3(LAMB 2(LAMB 1 ␈↓
␈↓ ↓H␈↓␈↓ αλ        ␈↓¬        (APPL(APPL(APPL(X.1)(X.4))(X.3))(X.2))))))␈↓
␈↓ ↓H␈↓␈↓ αλ␈↓↓t1␈↓ → ␈↓¬(LAMB 1(APPL(X.1)(LAMB 2(LAMB 3(LAMB 4␈↓
␈↓ ↓H␈↓␈↓ αλ      ␈↓¬        (APPL(APPL(APPL(APPL(X.3)␈↓
␈↓ ↓H␈↓␈↓ αλ      ␈↓¬                (LAMB 0(X.0)))(X.4))(LAMB 0(X.0)))(X.2)))))))␈↓
␈↓ ↓H␈↓␈↓ αλ␈↓↓t2␈↓ → ␈↓¬(LAMB 1(APPL(X.1)(LAMB 2(LAMB 3(LAMB 4␈↓
␈↓ ↓H␈↓␈↓ αλ      ␈↓¬        (APPL(APPL(APPL(APPL(X.2)␈↓
␈↓ ↓H␈↓␈↓ αλ      ␈↓¬                (LAMB 0(X.0)))(X.4))(LAMB 0(X.0)))(X.3)))))))␈↓
␈↓ ↓H␈↓␈↓ αλ␈↓↓t3␈↓ → ␈↓¬(LAMB 1(APPL(X.1)(LAMB 2(LAMB 3(LAMB 4␈↓
␈↓ ↓H␈↓␈↓ αλ      ␈↓¬        (APPL(APPL(APPL(APPL(X.2)␈↓
␈↓ ↓H␈↓␈↓ αλ      ␈↓¬                (LAMB 0(X.0)))(X.3))(LAMB 0(X.0)))(X.4)))))))␈↓

␈↓ ↓H␈↓The␈α∀sense␈α∀in␈α∪which␈α∀the␈α∀␈↓¬LAMB␈↓-expressions␈α∪represent␈α∀things,␈α∀is␈α∪that␈α∀after␈α∀doing␈α∪appropriate
␈↓ ↓H␈↓reductions␈α∂(and␈α⊂renaming␈α∂of␈α∂bound␈α⊂variables)␈α∂the␈α⊂result␈α∂of␈α∂"applying"␈α⊂the␈α∂representation␈α⊂of␈α∂a
␈↓ ↓H␈↓2␈↓ H


␈↓ ↓H␈↓function␈α∞to␈α∂the␈α∞repsentation␈α∞of␈α∂its␈α∞argument(s)␈α∞is␈α∂a␈α∞representation␈α∞of␈α∂the␈α∞result␈α∞of␈α∂applying␈α∞the
␈↓ ↓H␈↓function␈α∂to␈α∞the␈α∂argument(s)␈α∞in␈α∂the␈α∞ordinary␈α∂sense.␈α∞  For␈α∂example␈α∞␈↓↓add1[1]␈↓␈α∂is␈α∞represented␈α∂by␈α∞the
␈↓ ↓H␈↓expression␈α
␈↓¬(APPL␈α
λ[add1]␈α∞λ[1])␈↓,␈α
where␈α
␈↓¬λ[thing]␈α
␈↓is␈α∞shorthand␈α
for␈α
the␈α∞␈↓¬LAMB␈↓-representation␈α
of
␈↓ ↓H␈↓␈↓¬thing␈α⊂␈↓as␈α⊂given␈α⊂above.␈α⊂ As␈α⊂a␈α⊃␈↓¬LAMB␈↓-expression␈α⊂it␈α⊂be␈α⊂reduces␈α⊂to␈α⊂the␈α⊂expression␈α⊃representing␈α⊂2.
␈↓ ↓H␈↓Given␈α∞any␈α∞two␈α∂expressions␈α∞␈↓¬e1,␈α∞␈↓␈↓¬e2,␈α∂␈↓␈α∞␈↓¬(APPL(APPL␈α∞λ[pair]␈α∂e1)␈α∞e2)␈↓␈α∞represents␈α∂the␈α∞␈↓↓pair[e1,e2]␈↓
␈↓ ↓H␈↓and␈α⊂␈↓¬(APPL␈α⊂λ[p1]␈α⊂(APPL(APPL␈α⊂λ[pair]␈α⊂e1)␈α⊂e2))␈↓␈α⊂represents␈α⊂␈↓↓p1[pair[e1,e2]]␈↓␈α⊂and␈α⊂as␈α⊃a␈α⊂␈↓¬LAMB␈↓-
␈↓ ↓H␈↓expression␈α~reduces␈α~to␈α~␈↓¬e1␈α~␈↓as␈α≠it␈α~should.␈α~ Thus␈α~arithmetic␈α~is␈α~represented␈α≠accurately␈α~(on
␈↓ ↓H␈↓representations␈αof␈αnumbers)␈αand␈αthe␈αrepresentations␈α␈↓↓pair,p1,p2␈↓␈αobey␈αrules␈αsimilar␈αto␈αthose␈αfor␈α␈↓αa␈↓,
␈↓ ↓H␈↓␈↓αd␈↓, and qcons acting on S-expressions.  The representations of ␈↓↓trip,t1,t2,t3␈↓ behave analogously.

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

␈↓ ↓H␈↓α␈↓ ¬0More to do with ␈↓¬LAMB ␈↓α

␈↓ ↓H␈↓1.␈α Using␈αthe␈αbasic␈αroutines␈αfor␈αmanipulating␈α␈↓¬LAMBs␈α␈↓you␈αcan␈αwrite␈αan␈αinteractive␈αinterpreter␈αthat
␈↓ ↓H␈↓will accept a variety of commands and take appropriate actions.  Here are some ideas.

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

␈↓ ↓H␈↓1.2.␈α→ An␈α→␈↓¬ALPHA␈α_␈↓command␈α→that␈α→takes␈α_an␈α→expression␈α→and␈α_two␈α→numbers␈α→(and␈α→possibly␈α_a
␈↓ ↓H␈↓subexpression designation) and does an ␈↓¬ALPHA ␈↓conversion.

␈↓ ↓H␈↓1.3.␈α
 A␈α∞␈↓¬BETA␈α
␈↓command␈α
that␈α∞takes␈α
an␈α∞expression␈α
(and␈α
possibly␈α∞a␈α
subexpression␈α∞designation)␈α
and
␈↓ ↓H␈↓does an ␈↓¬BETA ␈↓conversion if allowed.

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

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

␈↓ ↓H␈↓1.6.  Any other commands that seem like fun to implement.
␈↓ ↓H␈↓␈↓ 93


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

␈↓ ↓H␈↓3.␈α Modify␈αthe␈αerror␈αchecking␈αparts␈αof␈αyour␈αprogram␈αto␈αuse␈αthe␈αMACLISP␈αprimitives␈α␈↓¬CATCH␈α␈↓and
␈↓ ↓H␈↓␈↓¬THROW.␈α∂␈↓␈α⊂Cleverly␈α∂done␈α⊂this␈α∂can␈α⊂get␈α∂the␈α∂appropriate␈α⊂message␈α∂to␈α⊂the␈α∂appropriate␈α⊂place␈α∂without
␈↓ ↓H␈↓explicitly␈αcarrying␈α
around␈αan␈αextra␈α
parameter,␈αor␈αchecking␈α
every␈αtime␈αa␈α
called␈αroutine␈α
returns␈αto
␈↓ ↓H␈↓see if it succeeded.

␈↓ ↓H␈↓4.␈α
 You␈α
may␈α
have␈α
noticed␈α
that␈α
the␈α
notation␈α
for␈α
␈↓¬LAMB␈↓-expressions␈α
is␈α
not␈α
as␈α
compact␈α
or␈α
flexible␈α
as␈α
it
␈↓ ↓H␈↓might␈α⊂be.␈α∂ Devise␈α⊂some␈α⊂``shorthand''␈α∂that␈α⊂your␈α∂interpreter␈α⊂can␈α⊂understand.␈α∂ It␈α⊂should␈α⊂read␈α∂the
␈↓ ↓H␈↓short␈α∞forms,␈α
convert␈α∞to␈α
standard␈α∞form␈α∞for␈α
manipulation,␈α∞and␈α
print␈α∞the␈α
results␈α∞in␈α∞some␈α
standard
␈↓ ↓H␈↓shorthand.  Some possible abbreviations are:

␈↓ ↓H␈↓¬␈↓ αH(LAMB n (LAMB m body)) ↔ (LAMB (n m) body)
␈↓ ↓H␈↓¬␈↓ αH(APPL (APPL e1 e2) e3) ↔ (APPL e1 e2 e3)

␈↓ ↓H␈↓You may wish to think up fancier ones.

␈↓ ↓H␈↓5.␈α
 If␈α∞you␈α
are␈α
adventurous,␈α∞think␈α
about␈α
using␈α∞the␈α
destructive␈α
operations␈α∞␈↓¬RPLACA␈α
␈↓and␈α∞␈↓¬RPLACD␈α
␈↓to
␈↓ ↓H␈↓carry␈α
out␈α
some␈αof␈α
the␈α
substitutions␈αmade␈α
on␈α
␈↓¬LAMB␈↓-expressions.␈α
  First␈αconsider␈α
when␈α
such␈αaction␈α
is
␈↓ ↓H␈↓safe␈α∩and␈α⊃reasonable.␈α∩ Note␈α⊃that␈α∩if␈α⊃the␈α∩structure␈α⊃you␈α∩are␈α⊃modifying␈α∩is␈α⊃part␈α∩of␈α⊃more␈α∩the␈α⊃one
␈↓ ↓H␈↓expression,␈αyou␈αcan␈αget␈αvery␈αstrange␈αresults␈αif␈αyou␈αare␈αnot␈αcareful.␈α Sometimes␈αinitially␈αcopying␈αan
␈↓ ↓H␈↓expression␈α⊂that␈α⊂you␈α⊂wish␈α⊂to␈α⊂modify␈α∂many␈α⊂times␈α⊂and␈α⊂then␈α⊂doing␈α⊂modifications␈α⊂destructively␈α∂is
␈↓ ↓H␈↓successful and reasonable.