for-any
vs for-all
switch
in lambda-calculus
n
, it should reduce to the representation of n-1
. If
the number n
is represented as the n
-times repeated application,
the predecessor amounts to an un-application -- which is
not the operation lambda-calculus provides or supports. As Church was
about to give up the hope that lambda-calculus could express
arithmetic, his student Kleene was getting his wisdom teeth extracted,
and under anesthetic (or so Barendregt says) saw the solution. The
tooth-wrenching story and Kleene's predecessor have become the part
of the Functional Canon, told and retold in tutorials and
textbooks. The Kleene predecessor is so familiar that we hardly even
think there may be others. There are: I found one back in 1992 after a
day of thinking. (Incidentally, I also had a tooth extracted that
year, at a different time though.)
This article shows that by looking at the puzzle the
right way we easily see more and more solutions -- some of which
simpler (nearly half the size!) and more intuitive than
the canonical Kleene predecessor.
We can even represent the un-application.
Recall, the standard and the simplest representation of natural
numbers is Church numerals, listed below. (As a common shorthand, we write cn
for the term representing the number n
.):
c0: \f\x.x c1: \f\x.f x c2: \f\x.f (f x) ...The successor -- the term whose application to
cn
reduces to c(n+1)
-- has
two equivalent forms:succ: \n\f\x. n f (f x) succ: \n\f\x. f (n f x)The problem is to find the predecessor -- the term
pred
such that
the application pred cn
reduces to c(n-1)
. (What should be the result
of pred c0
is an open choice; often it is c0
.)The fundamental tautology of Church numerals is easy to overlook:
cn === cn succ c0where the equality is understood as beta-convertibility. Its importance appears when viewed as the template to build other representations of natural numbers; let's call these terms
pn
:pn: cn succp p0 (*)where
succp
and p0
are two arbitrary terms. This is
no longer a tautology: it is the closed-form expression for pn
in
lambda-calculus.
So far, the new numerals are the empty formality. They become useful once
we relate them to Church numerals. For example, take p0
to be cm
,
for some m
; take p1
to be c(m+1)
, etc. Clearly, succp
is just the
ordinary succ
. Then pn
has the meaning of c(n+m)
; definition (*)
immediately gives the term for adding two numerals:
add: \n\m.n succ m
To obtain the Kleene predecessor, let's think of pn
as a point between
two consecutive numbers cn
and c(n-1)
on the number line.
It can be represented as a pair (c(n-1),cn)
:
p0: (cm1, c0) p1: (c0, c1) p2: (c1, c2) ...using the standard encoding of pairs in lambda-calculus (the projections are
fst
and snd
). Here, cm1
is the term that we want as the result of applying the predecessor to c0
. For example, one may choose cm1
as c0
. The successor on
those `midpoint numbers' is easy to define:succp: \p.(snd p, succ (snd p))Definition (*) then gives the closed-form expression for
pn
, from
which we can extract c(n-1)
as the first component:pred: \n.fst (n succp p0)or, in the desugared form
\n. n (\p s. s (p (\x y. y)) (\f x. f (p (\x y. y) f x))) (\s. s (\s z. z) (\s z. z)) (\x y. x)
Albeit slick, the Kleene trick is a bit contrived. For example, succp
does not even look at the first component of the pair. The
`define new numeral' standpoint immediately brings to mind the simpler:
p0: Nothing or, desuraged: \g\y.y p1: Just c0 or, desuraged: \g\y.g (\f\x.x) p2: Just c1 or, desuraged: \g\y.g (\f\x.f x) ...using the standard encoding of the
Maybe
type. The succp
is thensuccp: \p.Just (p succ c0)which gives the predecessor as
pred: \n. (n succp p0) id c0or, in the desugared form
\n. n (\p g y. g (p (\n f x. f (n f x)) (\s z. z))) (\g y. y) (\x. x) (\s z. z)which is a bit shorter. There is room for improvement. Let us factor out the
\f\x.
`prefix' of any Church numeral, giving uspred: \n\f\x. (n (\p.Just (p f x)) p0) id xWhere we had
c0
before, we now have x
, and succ
is replaced with an
application of f
. The desugared form is:\n f x. n (\p g y. g (p f x)) (\g y. y) (\y. y) xwhich is one of the shortest predecessors, nearly half the size of Kleene's.
There is more! What can be simpler than
p0: cm1 p1: c0 p2: c1, etc.We just have to choose
cm1
in such a way so to distinguish it from all
other Church numerals. That is easy: for any Church numeral cn
,
the application cn (\z.false) false
reduces to false
.
Thus we may take as cm1
:cm1: \f\x.truethat returns
true
no matter to what it is twice applied to.
(The discrimination test takes constant time, in the normal evaluation
order). With the p-successor defined assuccp: \p.p (\z.false) false c0 (succ p)
the predecessor becomes
pred: \n.n succp (\f\x.true)Or, in the desugared form
\n. n (\p. p (\z x y. y) (\x y. y) (\s z. z) (\f x. f (p f x))) (\f x x y. x)
Finally, consider a different choice of cm1
, based on a different,
albeit slower to use, property of Church numerals: for any cn
, cn
(\x.x)
reduces to \x.x
. In other words, the identity combinator
is the fixpoint of Church numerals. As cm1
, we chose something that,
when applied to
identity, is other than the identity; for example, \x.c0
:
cm1: \f\x.c0 succp: \p.p (\x.x) (succ p)The predecessor then is
pred: \n.n (\p.p (\x.x) (succ p)) (\f\x.c0)Or, in the desugared form
\n. n (\p. p (\x. x) (\f x. f (p f x))) (\f x s z. z)This is nearly half the size of the Kleene predecessor. This was the predecessor that I found in 1992.
Even the initial puzzle of predecessor as an un-application is solvable. To be sure, lambda-calculus has no un-application primitive, letting us only apply terms but not examine them. However, lambda-calculus can represent all computations, including itself. The representations can be examined and deconstructed to our heart's content. For example, consider
mynoapp: \x. \g\y. y x myapp: \f\x. \g\y. g f x
which is an encoding of the data type:
type myterm = App myterm myterm | NoApp termrepresenting lambda-applications. If
cn
represents the natural
number n
by n
repeated applications, let pn
represent those
repeated applications:pn: \f\x. cn (myapp f) (mynoapp x)More insightfully,
pn
can be written as reify cn
wherereify: \n\f\x. n (myapp f) (mynoapp x)gives us the representation of
cn
(goes up the level of representation).
The inverse is reflect
, which recovers the numeral from its representation:reflect: \p\f\x. fix (\s r. r (\f\x. f (s x)) (\y.y)) (p f x)For example, if
p3
is reify c3
then reflect p3
reduces back to c3
.
The advantage of representing applications is that we can examine and unapply
them, as shown in OCaml notation:let unapply = fun t -> match t of | App (_,x) -> x | x -> xor, in lambda-calculus
unapp: \t.t (\d m. m) (\d.t)We obtain the predecessor of
cn
by first reifying the numeral,
removing one application and reflecting back.pred: \n. reflect (\f\x. (unapp ((reify n) f x)))
Thus, once again we have seen how important it is to contemplate representations and what they represent, and be able to move between the two. (Bonus to the reader who can find/make a Matrix quote.) Kleene numerals gave us an example that canonical, canonized approaches are not the only ones possible -- and sometimes are not the best. Hence, no matter how much something appears settled, it is worth probing. Finally, one cannot help but wonder at the delicate behavior that arises from trite rules.
Numerals and lists in lambda-calculus: P-numerals
A different representation of numerals, with the predecessor being just as simple as the successor.
P-numerals are the functional equivalent of lists: increment, decrement, and zero testing operations on P-numerals all
take constant time -- just as cons
, car
, and null?
do on lists.
Peter G. Hancock has observed that P-numerals are closely
related to Goedel's recursor R
.
Paul Brauner has pointed out that P-numerals have been introduced by Michel Parigot back in 1988, with different motivations and in a typed setting. They are since called ``Parigot integers''. Paul Brauner has pointed out yet another way to come to P-numerals, from the definition of integers in deduction modulo.
Andrew Hodges, in `Alan Turing: The Enigma', wrote: ``But underneath there lay the same powerful idea that Goedel has used, that there was no essential distinction between numbers and operations on numbers.'' And so, lambda-calculus and Turing machine are duals: In a (universal) TM, an integer encodes an operation. In lambda-calculus, an operation encodes an integer.
Michel Parigot: Programming with proofs: A second order type theory.
LNCS 300, pp. 145-159, 1988.
Peter G. Hancock: The AMEN combinators and their reduction.
Combinatorially complete arithmetic operations, and a rewriting calculus for arithmetical expressions built entirely upon addition, multiplication, exponentiation, and naught.
for-any
vs for-all
for-any
and for-all
. Lambda calculus
lets us demonstrate the truth of a proposition --
such as the predecessor being the left inverse of the successor -- for any Church numeral, and yet unable to demonstrate it
for all numerals. For P-numerals however, we can prove the proposition for all
numerals, within the lambda calculus itself. In other words, in stark
contrast to Church numerals, for P-numerals the
composition pred . succ
normalizes to the identity function.In the notation of the Haskell lambda-calculator, Church-numerals, the successor and the predecessor are defined as follows:
c1 = f ^ x ^ f # x -- Church numeral 1 succ = n ^ f ^ x ^ f # (n # f # x) pred = n ^ f ^ x ^ n # (g ^ h ^ h # (g # f)) # (y ^ x) # (y ^ y)Taking
c1
as an example, we demonstrate taking the
successor, then taking the predecessor, and checking the final result being
beta-eta-equivalent to the original numeral c1:*LC_Pnum> eval (succ # c1) (\f. (\x. f (f x))) *LC_Pnum> eval (pred # (succ # c1)) (\f. f) *LC_Pnum> eval (pred # (succ # c1)) == eval c1 True
We can do these operations for any concrete numeral. However, when we try to prove that taking the successor followed by the predecessor being the identity for all numerals, we get stuck. It is easy to define the composition of the predecessor and the successor, and to normalize it:
*LC_Pnum> let predsucc_c = n ^ pred # (succ # n) *LC_Pnum> eval predsucc_c (\n. (\f. (\x. n (\g. (\h. h (g f))) (\y. x) f)))Alas, the normalization result does not look like the the identity function at all. We must use the external, to lambda calculus, induction principle. Here is the induction step:
*LC_Pnum> eval (predsucc_c # (succ # n)) (\f. (\x. f (n (\g. (\h. h (g f))) (\y. x) f))) *LC_Pnum> eval (succ # (predsucc_c # n)) (\f. (\x. f (n (\g. (\h. h (g f))) (\y. x) f))) *LC_Pnum> eval (succ # (predsucc_c # n)) == eval (predsucc_c # (succ # n)) TrueOne is reminded of Robinson Arithmetic, or Q, which is essentially Peano Arithmetic without the induction schema. One can prove in Q that the addition of any two concrete natural numbers is commutative, but one cannot prove the commutativity of addition for all natural numbers.
We now turn to P-numerals, with the following successor and predecessor:
p0 = c0 -- the same as Church 0 succp = n ^ f ^ x ^ f # n # (n # f # x) predp = n ^ n # combK # combI p1 = succp # p0(one can use anything in place of the
I
combinator, combI
, in predp
.
More properly, one should use -1). As before, we check that
the predecessor is the left inverse of the successor, for a concrete
numeral, p1
in our example:*LC_Pnum> eval p1 -- The P-numeral 1 (\f. f (\f. (\x. x))) *LC_Pnum> eval (succp # p1) (\f. (\x. f (\f. f (\f. (\x. x))) (f (\f. (\x. x)) x))) *LC_Pnum> eval (predp # (succp # p1)) (\f. f (\f. (\x. x))) *LC_Pnum> eval (predp # (succp # p1)) == eval p1 TrueWe can likewise show that for any numeral
pn
, (predp # (succp # p1))
is beta-eta-equivalent to pn
.
We now prove a stronger claim -- that the predecessor is the
left inverse of the successor for all numerals -- within the lambda-calculus
itself. We define the composition of predp
and succp
:predsucc = n ^ predp # (succp # n)and normalize it
*LC_Pnum> eval predsucc (\n. n)obtaining the identity function, syntactically. Thus the predicate
predsucc n == n
holds uniformly, that is, for all n
.Although for-any vs for-all distinction is emblematic of intuitionism, Whitehead and Russell were already aware of it when writing Principia Mathematica. They insisted on separate notations for `any' vs. `all' (although admitting the equivalence of these notions in their theory) [Chap 1, p18, paragraph ``Ambiguous assertion and the real variable''].
The article was prompted by a question from Benedikt Ahrens.
Let c_i
denote a Church numeral for the number
i. We should design two terms beq
and bluff
so that
the following reductions hold:
beq c_i c_j ==> \x\y.x (that is, boolean 'true') iff i == j ==> \x\y.y (that is, boolean 'false') otherwise beq bluff c_i ==> \x\y.x (that is, boolean 'true') for all i beq c_i bluff ==> \x\y.x (that is, boolean 'true') for all i beq bluff bluff ==> \x\y.y (that is, boolean 'false')
In other words, beq
should act as equality on
Church numerals. The bluff combinator should be beq
-equal to
any numeral. However, the combinator should not be bequal
to itself. The gist of the problem is discriminating any
Church numeral from some other term.
Mayer Goldberg and Mads Torgersen: Circumventing Church Numerals. Nordic Journal of Computing, v9, January 2002, pp. 1-12.
((\x\y.x y) y)
the sub-expression \y.x y
shadows the (free) variable y
. Alpha-conversion renames the locally-bound variable and
eliminates the shadowing: (\x\z.x z) y
. One often hears that
variable shadowing makes programs harder to understand and
error-prone, and should be avoided whenever possible, by using distinct
variable names. OCaml and GHC Haskell compilers, among others, take
this advice to the heart: GHC has a special initial compiler phase
that uniquely renames all variables within the program.This prompts the question: Suppose we take trouble to consciously avoid variable shadowing when writing lambda-terms, choosing fresh (unique) names for bound identifiers. Do we still need alpha-conversion when evaluating such terms? In other words, can we apply alpha-conversion to a term at the very beginning, making all binders distinctly named -- and then forget about alpha-conversion for the rest of the evaluation? How necessary is the alpha-conversion really?
The unique naming of binders indeed makes alpha-conversion unnecessary -- in very many cases. Yet in general it is unavoidable. We show several subtle examples of terms with uniquely named binders that still demand alpha-conversion in the middle of evaluation. In fact, in some cases such `dynamic' alpha-conversion is needed indefinitely many times.
The answer satisfies the old curiosity: why all formal introductions to lambda-calculus start with the phrase like `Let V be an infinite countable set of variable names'. We shall see why lambda-calculus needs infinitely many names. Surprisingly, there are practical implications, for the implementation of staged languages. In fact, one of the examples below is patterned after a bug accidentally discovered in the first implementation of MetaScheme.
To start with, recall that variables in (closed) lambda-terms
play the role of pointers, between the binder (lambda) and the places
where a future application should insert its argument.
Therefore, names per se do not matter, only their equality: \x.x
and \y.y
denote the same identity function. Formally, identity and other
relations between lambda-terms are understood modulo alpha-conversion,
the renaming of bound identifiers.
Alpha-conversion is not just an formalization artifact: it is something we may have to really do during the evaluation. Consider the following beta-reductions:
(\x\y.x y) y --> \y. y y -- Wrong! (\x\z.x z) y --> \z. y z (\x\u.x u) y --> \u. y uThe terms to reduce are all equivalent, differing only in the name of one bound variable. The last two reduction results are also equivalent: the eta-expanded version of
y
. But the first reduction
breaks the equivalence. It is therefore prohibited.
The term (\x\y.x y) y
has to be first alpha-converted, say,
to (\x\z.x z) y
, before the beta-reduction may be carried out.
On the other hand, alpha-conversion
feels rather similar to beta-reduction: in either case, we traverse
the body of a lambda-abstraction, looking for a particular variable and
replacing it. It seems bothersome and inelegant to having to precede a
beta-reduction with alpha-conversion, the operation of roughly the
same complexity.In the above -- and many other cases -- alpha-conversion can be averted had we given bound variables unique names to start with. But not in all cases. No matter how variables are named at the beginning, there may come a time during the evaluation when shadowing appears. This happens when substituting a term into itself:
(\y. y y) (\z.\x. z x) --> (\z.\x. z x) (\z.\x. z x) --> (\x. (\z.\x. z x) x)To proceed further, alpha-conversion is unavoidable.
In fact, we may have to do alpha-conversion infinitely many times, e.g., when reducing the following term:
(\y.y s y) (\t\z\x. z (t x) z) --> (\t\z\x. z (t x) z) s (\t\z\x. z (t x) z) --> (\z\x. z (s x) z) (\t\z\x. z (t x) z) --> \x. (\t\z\x. z (t x) z) (s x) (\t\z\x. z (t x) z) --> {alpha-conversion is necessary} --> \x. (\t\z\x1. z (t x1) z) (s x) (\t\z\x. z (t x) z) --> \x. (\z\x1. z (s x x1) z) (\t\z\x. z (t x) z) --> \x. \x1. (\t\z\x. z (t x) z) (s x x1) (\t\z\x. z (t x) z) --> {another alpha-conversion is necessary, renaming x to something that is different from x and x1} --> \x. \x1. (\t\z\x2. z (t x2) z) (s x x1) (\t\z\x. z (t x) z) --> ...
Our examples so far relied on self-applications and were written in the untyped lambda-calculus. One may wonder if the simply-typed lambda-calculus, where self-application is ruled out, might let us escape from alpha-conversion. It does not. The indefinite number of alpha-conversions may be needed even here, as the following example with the second Church numeral demonstrates:
fun t -> (fun y -> y (y t)) (fun u z x -> u x z);; -> fun t -> (fun u z x -> u x z) (fun z x -> t x z) -> fun t -> (fun z x -> (fun z x -> t x z) x z)The example is written in the OCaml notation, to double-check it is simply typed.
Thus typed or untyped, the alpha-renaming step may have to be done during the evaluation, arbitrarily many times. We may need an inexhaustible supply of fresh names. This is something to keep in mind when implementing staged languages, for example.
c_i
means a Church numeral for integer i
, true
stands
for the term \x\y.x
and false
stands for \x\y.y
. The symbol ==>
indicates reduction in one or several steps.c_i (\x.false) false ==> false
This property of Church numerals helped to solve the bluff combinator problem.
c_i combI ==> combI
where combI
is the identity combinator \x.x
. Thus the identity
combinator is a fixpoint of any Church numeral.
c_i c_j c_k ==> c_n
where n=k^(j^i)
and the operator ^ means exponentiation. The property says that an application of a Church numeral to two other Church numerals is itself a Church numeral, which corresponds to the exponentiated integers.
c_1 === combI
, true === K
, c_0 === false
Trivial statements that c_1
is the identity
combinator and true
is the K
(a.k.a. const)
combinator. In Lambda calculus -- as in C, Perl and other programming
languages -- numeral 0
and boolean false
are the same.
c_i (\y.x) u ==> x, c_0 (\y.x) u ==> u, i>0
This property gives a simple test for discriminating c_0
from
any other Church numeral.
cons a x (cons b y) ==> a b y x
where cons
is \x\y\p.p x y
.
switch
in lambda-calculusswitch
combinator, a lambda-term
with the following reduction rules:switch 0 -> id switch n test1 stmt1 test2 stmt2 ... test_n stmt_n default -> stmt_i for the first i such that test_i -> true -> default otherwiseHere
n
is a Church numeral, test_i
are
Church Booleans, stmt_i
and default
are
arbitrary terms. We impose an additional constraint of avoiding general
recursion.
For example, assuming c2
stands for Church numeral 2, etc., and true
, false
, and zerop
are combinators with the obvious meaning,
((switch c2) true x true y z) ; reduces to: x ((switch c2) false x true y z) ; reduces to: y ((switch c3) false x false y (zerop c1) z h) ; reduces to: h
Addition, multiplication, squaring, and exponentiation are easily expressed in lambda-calculus. We discuss two approaches to their ``opposites'' -- subtraction, division, finding of a square root and of a discrete logarithm. The opposite operations present quite a challenge. One approach, based on fixpoints, is more elegant but rather impractical. The dual approach, which relies on counting, leads to constructive and useful, albeit messy, terms.
lambda-arithm-neg.scm [14K]
Negative numbers and four arithmetic operations on integers
The source code that defines and tests all four arithmetic operations on positive and negative integers, in lambda-calculus. The code is meant to be evaluated by the practical lambda-calculator in Scheme.
LC_neg.lhs [17K]
Negative numbers and the four arithmetic operations on integers [Haskell version]
lambda-calc-opposites.txt [4K]
The article ``Subtraction, division, logarithms and other opposites in Lambda calculus'' posted on comp.lang.functional on Tue, 29 May 2001 20:58:02 -0700
lambda-arithm-div-term.scm [8K]
Lambda abstraction term for division An unadorned lambda term that implements division of two signed integers (also represented as lambda terms). The article explains in detail how this division term has been derived.
LC_basic.lhs [4K]
A version for the Haskell calculator. This is a literate Haskell code that defines the terms and shows examples of their use.
car
and cdr
operations are both impossible in the simply typed lambda-calculus. Henk
Barendregt's ``The impact of the lambda-calculus in logic and computer
science'' (The Bulletin of Symbolic Logic, v3, N2, June 1997) has the
following phrase, on p. 186:Since list is a generalization of numeral -- withEven for a function as simple as the predecessor lambda definability remained an open problem for a while. From our present knowledge it is tempting to explain this as follows. Although the lambda calculus was conceived as an untyped theory, typeable terms are more intuitive. Now the functions addition and multiplication are defineable by typeable terms, while [101] and [108] have characterized the lambda-defineable functions in the (simply) typed lambda calculus and the predecessor is not among them [the story of the removal of Kleene's four wisdom teeth is skipped...]
Ref 108 is R.Statman: The typed lambda calculus is not elementary recursive. Theoretical Comp. Sci., vol 9 (1979), pp. 73-81.
cons
being a successor, append
being the addition, tail
(aka cdr
) being the predecessor -- it
follows then the list cannot be encoded in the simply typed
lambda-calculus.To encode both operations, we need either inductive (generally, recursive) types, or System F with its polymorphism. The first approach is the most common. Indeed, the familiar definition of a list
data List a = Nil | Cons a (List a)gives an (iso-) recursive data type (in Haskell. In ML, it is an inductive data type).
Lists can also be represented in System F. As a matter of
fact, we do not need the full System F (where the type reconstruction
is not decidable). We merely need the extension of the Hindley-Milner system
with higher-ranked types, which requires a modicum of type annotations
and yet is able to infer the types of all other terms. This extension
is supported in Haskell and OCaml. With such an extension, we can represent
a list by its fold, as shown in the code below. It is less known that
this representation is faithful: we can implement all list operations,
including tail
, drop
, and even zip
.
list-representations.txt [9K]
Detailed discussion of various representations of lists in Haskell, and their typing issues
The message was originally posted as ``Re: Lists vs. Monads'' on the Haskell-Cafe mailing list on Thu, 21 Jul 2005 19:30:38 -0700 (PDT)
The traditional recipe for normal-order reductions includes an
unpleasant phrase ``cook until done''. The phrase makes it necessary
to keep track of reduction attempts, and implies an ugly iterative
algorithm. We're proposing what seems to be an efficient and elegant
technique that can be implemented through intuitive re-writing rules.
Our calculator, like yacc, possesses a stack and works by doing a
sequence of shift
and reduce
steps. The only
significant difference from yacc is that the lambda-calculator
``reparses'' the result after the successful reduce step. The source
and the target languages of our ``parser'' (lambda-calculator) are the
same; therefore, the parser can indeed apply itself.
The parsing stack can be made implicit. In that case, the algorithm can be used for normalization of typed lambda-terms in Twelf.
The following examples show that lambda-calculus becomes a domain-specific language embedded into Haskell:
> c0 = f ^ x ^ x -- Church numeral 0 > succ = c ^ f ^ x ^ f # (c # f # x) -- Successor > c1 = eval $ succ # c0 -- pre-evaluate other numerals > c2 = eval $ succ # c1 > c3 = eval $ succ # c2 > c4 = eval $ succ # c3
It is indeed convenient to store terms in Haskell variables and
pre-evaluate (i.e., normalize) them. They are indeed terms. We can
always ask the interpreter to show the term. For example, show c4
yields (\f. (\x. f (f (f (f x)))))
.
let mul = a ^ b ^ f ^ a # (b # f) -- multiplication eval $ mul # c1 ---> (\b. b), the identity function eval $ mul # c0 ---> (\b. (\f. (\x. x))), which is "const 0"
These are algebraic results: multiplying any number by zero always gives zero. We can see now how lambda-calculus can be useful for theorem proving, even over universally-quantified formulas.
The calculator implements Dr. Fairbairn's suggestion to limit the depth of printed terms. This makes it possible to evaluate and print some divergent terms (so-called tail-divergent terms):
Lambda_calc> let y_comb = f^((p^p#p) # (c ^ f#(c#c))) in eval $ y_comb#c c (c (c (c (c (c (c (c (c (c (...))))))))))It is amazing how well lambda-calculus and Haskell play together.
A monadic version of the calculator gives us the trace of the reduction steps.
all_tests
.
Reynald Affeldt. Abstract machines for functional languages. A Survey.
< http://web.yl.is.s.u-tokyo.ac.jp/~affeldt/study/abstract_machines.ps >
The survey describes SECD, Krivine, CAM and ZAM machines and several of their variations.
Incidentally, Lambda_calc.lhs
appears to have little in common
with Krivine, SECD or other machines. The Lambda_calc.lhs machine has
stack, but it has no concept of environment. This is indicative of a
larger difference: in Lambda_calc.lhs variables have 'no meaning'. To
this machine, normalization of lambda terms is a pure syntactic
transformation, akin to a transformation of (((a+b)))
into a+b
by a regular parser.
The code also includes a few convenience tools: tracing of all reduction, comparing two terms modulo alpha-renaming, etc.
(?lc-calc ((lambda (x) (x x)) (lambda (y) (y z))) ; term to reduce (??!lambda (result) (display '(??! result))) )expands to
(display '(z z))
. The funny ??!lambda
is a
macro-lambda -- the abstraction of the (meta-)calculator.The calculator normalizes regular Scheme terms. The result can be compiled and evaluated in a call-by-value lambda-calculus with constants (i.e., Scheme). The lambda-calculator acts therefore as a partial evaluator.
(((NORM ((lambda (c) ; succ (lambda (f) (lambda (x) (f ((c f) x))))) (lambda (f) f) ; c1 )) (lambda (u) (+ 1 u))) 0)normalizes the application of the
succ
lambda-term
to c1
, Church numeral 1. The result, which is
a Scheme procedure, is then applied to the Scheme values (lambda (u) (+ 1 u))
and 0
to yield 2 -- which shows
that the result of the normalization was Church numeral 2.The calculator normalizes regular Scheme terms. The result can be compiled and evaluated in a call-by-value lambda-calculus with constants (i.e., Scheme). The lambda-calculator acts therefore as a partial evaluator.
The core of the interpreter indeed takes only three lines:
instance E (F x) (F x) instance (E y y', A (F x) y' r) => E ((F x) :< y) r instance (E (x :< y) r', E (r' :< z) r) => E ((x :< y) :< z) rThe first line says that abstractions evaluate to themselves, the second line executes the redex, and the third recurs to find it. The representation of abstractions is apparent from the expression for the
S
combinator, which again takes three lines:instance A (F CombS) f (F (CombS,f)) instance A (F (CombS,f)) g (F (CombS,f,g)) instance E (f :< x :< (g :< x)) r => A (F (CombS,f,g)) x rThe instances of the type class
A f x r
define the result r
of applying f
to x
. The last line shows
the familiar lambda-expression for S
, written with the
familiar variable names f
, g
, and x
. The
other two lines build the closure `record'. The closure-conversion is
indeed the trick. The second trick is taking advantage of the instance
selection mechanism. When the type checker selects a type-class
instance, the type checker instantiates it, substituting for the type
variables in the instance head. The type checker thus does the
fundamental operation of substitution, which underlies beta-reduction.
No wonder why our lambda-calculator is so simple.The encoding of the applicative fixpoint combinator is even simpler:
data Rec l instance E (l :< (F (Rec l)) :< x) r => A (F (Rec l)) x rexpressing the reduction of the application
(fix l) x
to l (fix l) x
.
The article shows several examples of using the fixpoint combinator,
e.g., to compute Fibonacci numbers.
Incidentally, the present code constitutes what seems to be the
shortest proof that the type system of Haskell with the undecidable
instances extension is indeed Turing-complete.The type-level lambda-calculator albeit trivial has the expected properties, e.g., handling of closures and higher-order functions. It uses named function arguments, rather than De Bruijn indices and is based on explicit substitutions. We again rely on the Haskell type checker for appropriate alpha-conversions.
oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML