<!doctype html public "-//W3C//DTD W3 HTML//EN">
<html><head><style type="text/css"><!--
blockquote, dl, ul, ol, li { padding-top: 0 ; padding-bottom: 0 }
--></style><title>[Haskell] Re: Announcing Djinn, new version
2004-12-13</title></head><body>
<div><font face="Lucida Grande" size="-3" color="#000000">Chung-chieh
Shan wrote:</font></div>
<div><br></div>
<blockquote type="cite" cite><font face="Lucida Grande" size="-3"
color="#000000">I wonder why the only Church numerals Djinn found were
0 and 1?</font></blockquote>
<blockquote type="cite" cite><font face="Lucida Grande" size="-3"
color="#000000"><br></font></blockquote>
<blockquote type="cite" cite><font face="Lucida Grande" size="-3"
color="#000000"> Djinn> :set
+m</font></blockquote>
<blockquote type="cite" cite><font face="Lucida Grande" size="-3"
color="#000000"> Djinn> num ? (a -> a) ->
(a -> a)</font></blockquote>
<blockquote type="cite" cite><font face="Lucida Grande" size="-3"
color="#000000"> num :: (a -> a) -> a ->
a</font></blockquote>
<blockquote type="cite" cite><font face="Lucida Grande" size="-3"
color="#000000"> num x1 x2 = x1
x2</font></blockquote>
<blockquote type="cite" cite><font face="Lucida Grande" size="-3"
color="#000000"> -- or</font></blockquote>
<blockquote type="cite" cite><font face="Lucida Grande" size="-3"
color="#000000"> num _ x2 = x2</font></blockquote>
<blockquote type="cite" cite><font face="Lucida Grande" size="-3"
color="#000000"><br></font></blockquote>
<blockquote type="cite" cite><font face="Lucida Grande" size="-3"
color="#000000">Very cool, in any case.</font></blockquote>
<blockquote type="cite" cite><font face="Lucida Grande" size="-3"
color="#000000"><br></font></blockquote>
<blockquote type="cite" cite><font face="Lucida Grande" size="-3"
color="#000000"><x-tab>
</x-tab>Ken</font></blockquote>
<div><font face="Lucida Grande" size="-3"
color="#000000"><br></font></div>
<div>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<b> terminating</b>---proofs are
of bounded depth. (No loop-checking or tricks like "iterative
deepening" are required.)</div>
<div><br></div>
<div>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<i>
terminating</i>) and abandoned this when Herbelin later named two
important related calculi "LJT" and "LJQ".
"G4ip" is the name used in the<i> Basic Proof Theory</i>
book by Troelstra & Schwichtenberg.</div>
<div><br></div>
<div><x-tab>
</x-tab>Roy</div>
<div><br></div>
<x-sigsep><pre>--
</pre></x-sigsep>
<div><font size="-2"
color="#000000"
>--------------------------------------------------------------------<span
></span>----</font></div>
<div><font size="-2" color="#000000">Roy
Dyckhoff <span
></span
> <span
></span>
e-mail: rd@dcs.st-and.ac.uk</font></div>
<div><font size="-2" color="#000000">(Researcher; Senior Lecturer;
Director of Teaching; ...)</font></div>
<div><font size="-2" color="#000000"><br></font></div>
<div><font size="-2" color="#000000">School of Computer
Science <span
></span
> <br
>
University of St
Andrews <span
></span
> <span
></span> tel:
+44-1334-463267</font></div>
<div><font size="-2" color="#000000">North Haugh, St
Andrews, <span
></span
> <span
></span> ^fax:
+44-1334-463278</font></div>
<div><font size="-2" color="#000000">Fife, KY16 9SX,
Scotland <span
></span
> <span
></span> secr:
+44-1334-463253</font></div>
<div><font size="-2"
color="#000000"
> <span
></span
> <span
></span
> <span
></span
> <span
></span> *mob:
+44-7985-266847</font></div>
<div><font size="-2" color="#000000">Home page:
http://www.dcs.st-and.ac.uk/~rd</font></div>
<div><font size="-2" color="#000000"><br></font></div>
<div><font size="-2" color="#000000">* Mobile number is for emergency
use only ;-)</font></div>
<div><font size="-2" color="#000000"><br></font></div>
<div><font size="-2" color="#000000">^ There's also a personal e-fax
number: +44-8707-064-446, which then</font></div>
<div><font size="-2" color="#000000">sends me an e-mail with the fax
as an attachment.</font></div>
</body>
</html>