Re: Lambda calculus numerals book recommendation?

From: HERC777 (herc777_at_hotmail.com)
Date: 12/07/04


Date: 6 Dec 2004 21:06:48 -0800

I haven't heard of 'numerals', mentioned in some sites though
http://www.bath.ac.uk/~cs1spw/notes/Lisp/notes45.html

Church Numerals
Typed Church numerals are peculiar - you get the whole range of Church
numerals for each type, giving you an eventually infinite set.
Polymorphic Church Numerals are more flexible:

n = Λt.λxt -> tyt.xny

One kind of numeral can apply to anything as long as the type
structures match. They behave exactly the same as normal Church
numerals in pure lambda calculus.

Polymorphic Combinators
K = Λst.λxsyt.x
Type: ∀st. s->t->s

S = Λrst.λxr->s->tyr->szr.xz(yz)
Type: ∀rst.(r->s->t)->(r->s)->r->t

but I'm familiar with S and K combinators, they are used in the Miranda
compiler and should have more extensive literature.

I don't know why Sander is talking about function Y here, recursion is
taken for granted in application oriented lambda calculus, unless you
are interested in recursion itself but Y is inefficient.

Yf = fYf
something like that, a trick of lambda calculus to get multiple
versions of the one function instantiated. There's other bizzare
functions aswell that handle construction of lists and peano axioms
with pure functions, but aren't used.

Lambda Calculus + recursion + list constructors + primitive data
structure = useful language
though lambda calculus can do it all itself if you want.

Herc