for-any vs for-all
switch in lambda-calculus
This article will demonstrate basic arithmetic operations -- comparison, addition, subtraction, multiplication, and division -- on non-negative and negative integer numbers. Both the integers and the operations on them are represented as terms in the pure untyped lambda-calculus. The only building blocks are identifiers, abstractions and applications. No constants or delta-rules are used. Reductions follow only the familiar beta-substitution and eta-rules. We also show two approaches of defining a predecessor of a Church numeral. Curiously, none of the arithmetic operations involve the Y combinator; even the division gets by without Y.
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-calc-div-neg.txt [plain text file]
The article itself. It was originally posted as Negativism and division in lambda-calculus on the newsgroup comp.lang.functional on Sun, 13 May 2001 23:12:25 GMT
lambda-arithm-neg.scm [14K]
Negative numbers and four arithmetic operations on integers
The source code that defines and tests all four operations of
arithmetics on positive and negative integers, in lambda-calculus. The
code is meant to be evaluated by a practical lambda-calculator in Scheme.
LC_neg.lhs [17K]
Negative numbers and four arithmetic operations on integers [Haskell version]
This is a literate Haskell code that defines and tests all
four operations of arithmetics on positive and negative integers, in
lambda-calculus. The code is meant to be evaluated by a practical
lambda-calculator in Haskell.
lambda-calc-opposites.txt [plain text file]
An 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.
Definitions of basic lambda terms: Church numerals, combinators, Booleans, etc. These are basic lambda-calculus terms, needed to run more advanced examples. Two versions of the terms are given, in the notation of the Scheme and Haskell calculators.
lambda-arithm-basic.scm [4K]
A version for the Scheme calculator.
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.
This article derives a term in the pure untyped lambda-calculus that efficiently computes a symmetric difference of two Church numerals. We introduce other numerals, so called P-numerals, which are more convenient for arithmetic. We show the connection between the P-numerals and the list fold.
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.
LC_Pnum.lhs [13K]
The article itself. This is also a complete, literate Haskell
code that defines the numerals and the symmetric difference, gives an
example of their use, and compares Church and P-numerals.
The article was originally posted as Symmetric difference in
LC, P-numerals, and fold on comp.lang.functional on
Fri Aug 30 01:49:31 2002
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.
<http://homepages.inf.ed.ac.uk/v1phanc1/arithmetic.lhs>
for-any vs for-allContrasting Church-numerals with P-numerals gives an opportunity
to show the difference between 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)
Picking a sample numeral c1, 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))
True
One 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
True
We 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 succppredsucc = 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.
A Bluff combinator problem in the pure untyped lambda-calculus was posed by Mayer Goldberg in the 1990s:
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 a
Church numeral from some other term.
bluff.lhs [6K]
The complete code that shows one solution to the
problem. Other solutions are described in an article below.
Mayer Goldberg and Mads Torgersen: Circumventing Church Numerals. Nordic Journal of Computing, v9, January 2002, pp. 1-12.
This section collects curious properties of particular
lambda-terms. Some of the properties have been used in proving
theorems or solving puzzles described on this site. Throughout this
section, c_i means a Church numeral for integer i, true stands for a 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 ==> falsec_i combI ==> combIcombI 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)c_1 === combI, true === K, c_0 === falsec_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>0c_0 from any other Church numeral.
cons a x (cons b y) ==> a b y x\x\y\p.p x y.
switch in lambda-calculusWe implement the switch 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 otherwise
Here 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
comp.lang.functional on Tue, 25 Mar 2003 14:13:34 -0800The predecessor of a Church-encoded numeral, or, generally, the
encoding of a list with the 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:
Even 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...]Since list is a generalization of numeral -- with
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.
How to zip folds: A library of fold transformers (streams)
Detailed discussion of various representations of lists in
Haskell, and their typing issues [plain text file]
The message was originally posted as Re: Lists vs. Monads on Haskell-Cafe mailing list on Thu, 21 Jul 2005 19:30:38 -0700 (PDT)
The code below implements a normal-order interpreter for the untyped lambda-calculus. The interpret permits "shortcuts" of terms. The shortcuts are not first class and do not alter the semantics of the lambda-calculus. Yet they make complex terms easier to define and apply.
The code also includes a few convenience tools: tracing of all reduction, comparing two terms modulo alpha-renaming, etc.
Another normal-order interpreter for untyped lambda-calculus, implemented as a syntax-rule macro. The source and the object languages of the calculator are regular Scheme terms. Lambda-abstractions for the calculator are ordinary lambda-forms of Scheme:
(?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.
Yet another normal-order interpreter for untyped lambda-calculus, implemented as a direct-style syntax-rule macro. This implementation is the shortest and the fastest one. It does no alpha-renaming directly and no substitutions directly. Everything is integrated with normalization, and everything is delayed until the latest possible moment. The source and the object languages of the calculator are regular Scheme terms. Lambda-abstractions for the calculator are ordinary lambda-forms of Scheme:
(((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 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 present calculator implements what seems to be an efficient and elegant algorithm of normal order reductions. The algorithm is "more functional" than the traditionally used approach. The algorithm seems identical to that employed by yacc sans one critical difference. The calculator also takes a more "functional" approach to the hygiene of beta-substitutions, which is achieved by coloring of identifiers where absolutely necessary. This approach is "more functional" because it avoids a global counter or the threading of the paint bucket through the whole the process. The integration of the calculator with Haskell lets us store terms in variables and easily and intuitively combine them.
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.
Lambda_calc.lhs [23K]
The complete literate Haskell code for the calculator.
The code also includes convenience functions to list free
variables of a term and to compare two terms modulo
alpha-renaming. The latter function is extensively used in built-in
regression tests. To run the tests, evaluate all_tests.
The code was first posted in a message ANN: Normal-order evaluation as bottom-up parsing on Sun, 28 Apr 2002 14:11:59 -0700 on the Haskell mailing list.
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.
We present a type-level interpreter for the call-by-value lambda-calculus with booleans, natural numbers, and case discrimination. Its terms are Haskell types. Using functional dependencies for type-level reductions is well-known. Missing before was the encoding abstractions with named arguments and closures.
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) r
The 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 r
The 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 r
expressing 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 deBruijn indices and is based on explicit substitutions. We again rely on the Haskell type checker for appropriate alpha-conversions.
TypeLC.lhs [9K]
The complete literate Haskell code with explanations and tests,
including Fibonacci, S and K combinators and the combinatorial arithmetic
The code was originally posted in a message On computable types. I. Typed lambda and type closures on Thu, 14 Sep 2006 19:07:29 -0700 (PDT) on the Haskell mailing list.
This site's top page is http://okmij.org/ftp/
Converted from SXML by SXML->HTML