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
Dyckhoff
e-mail: [EMAIL PROTECTED]
(Researcher; Senior Lecturer;
Director of Teaching; ...)
School of Computer
Science
University of St Andrews tel: +44-1334-463267
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.
_______________________________________________ Haskell mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell
