Chung-chieh Shan wrote:

I wonder why the only Church numerals Djinn found were 0 and 1?

Djinn> :set +m Djinn> num ? (a -> a) -> (a -> a) num :: (a -> a) -> a -> a num x1 x2 = x1 x2 -- or num _ x2 = x2

Very cool, in any case.

Ken

My answer would be the same as Lennart's; in detail, the point of this calculus (or, rather, the G4ip calculus on which the implementation is based) is that it is terminating---proofs are of bounded depth. (No loop-checking or tricks like "iterative deepening" are required.) The idea for the calculus goes back not to myself but to Vorob'ev (1950), and was rediscovered around 1988-1990 by several people, notably (and independently) Joerg Hudelmaier (Arch. Math. Logic 1992; JLC 1993), Pat Lincoln et al (LICS 1991) and myself (JSL 1992). I called the calculus "LJT"(the "T" is for terminating) and abandoned this when Herbelin later named two important related calculi "LJT" and "LJQ". "G4ip" is the name used in the Basic Proof Theory book by Troelstra & Schwichtenberg. Roy -- ------------------------------------------------------------------------ Roy Dyckhoff e-mail: rd@dcs.st-and.ac.uk (Researcher; Senior Lecturer; Director of Teaching; ...) School of Computer Science University of St Andrews tel: +44-1334-463267 North Haugh, St Andrews, ^fax: +44-1334-463278 Fife, KY16 9SX, Scotland secr: +44-1334-463253 *mob: +44-7985-266847 Home page: http://www.dcs.st-and.ac.uk/~rd * Mobile number is for emergency use only ;-) ^ There's also a personal e-fax number: +44-8707-064-446, which then sends me an e-mail with the fax as an attachment.