[Haskell] Re: Announcing Djinn, new version 2004-12-13

[Roy Dyckhoff]

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 at 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org//pipermail/haskell/attachments/20051214/747a33d1/attachment.htm