[Prev][Next][Index][Thread]
Re: Second order logic and recursion
> Question: How does recursion appear in the logic? And if we introduce
> (first order) recursion, do we still have cut elimination (proofs in
> normal form)?
In lambda calculi, e.g. inductive types with iterators (\mu-types) and
inductive types with primitive recursors (\mu^r-types), defined for
positive or monotone type schemes, are well-behaving. (And equally
neat are coinductive types with coiterators and ditto with primitive
corecursors.) Systems that result from adding \mu- or \mu^r-types to
system F or to the simply-typed lambda calculus with product and
coproduct types are strongly normalizable. \mu-types can be encoded in
terms of \forall^2 and \imp in a fashion that preserves typing and
non-trivial \beta-reduction. For \mu^r-types, there is an encoding in
terms of \forall^2, \imp and what are sometimes called retractive
fixedpoint types (\sigma-types). Also well-behaving are something
known as inductive types a la Mendler with iterators and ditto with
primitive recursors. These may be defined for any type schemes.
Primitive recursors prove principles of structural induction,
iterators prove certain weakenings thereof.
[Note that what is meant by the term `primitive recursion' here is a
generalization of the primitive recursion from recursion theory;
Ackermann is primitive-recursive in this sense.]
Ralph Matthes wrote a PhD thesis recently on the subject, and so did I
(Tarmo Uustalu). From the notes by Pawel Urzyczyn for the Synergos
school in Edinburgh '99 I learned about the thesis of Zdzislaw
Splawski dating from 1993. A paper of theirs will appear in Proc
ICFP'99. Some of the important references to look up are, for system
F, Bo"hm and Berarducci, Leivant, Mendler, Geuvers; for Calculus of
Constructions and Martin-Lo"f Type Theory (dependent eliminations),
Pfenning, Paulin-Mohring and Coquand, Dybjer, Setzer; and on the logic
side also Parigot, Tatsuta (who don't worry about Curry-Howard, but
realizability).
The Proceedings of the 2nd Scand Logic Symposium, which you cited,
contain, besides the papers by Girard and Martin-Lo"f on hauptsatz for
the 2nd-order logic (``theory of species'') also a paper by
Martin-Lo"f on hauptsatz for ``the intuitionistic theory of iterated
inductive definitions'' (pp 179-216), with a proof of weak
normalization for inductive types given by strictly positive type
schemes. It is not mentioned in the paper, however, that induction
rules are iterators.
Below are some references. For more, you might wish to check
http://www.it.kth.se/~tarmo/bibs/tlc.bib.
Tarmo Uustalu
D Leivant. Reasoning about Functional Programs and Complexity Classes
Associated with Type Disciplines. In Proc FOCS'83, pp 460-469. IEEE
CS Press, 1983.
C Bo"hm and A Berarducci. Automatic Synthesis of Typed
{$\Lambda$}-Programs on Term Algebras. TCS, 39(2-3):135-154, 1985.
D Leivant. Contracting Proofs to Programs. In P Odifreddi, ed. Logic
and Computer Science, pp 279-327. Academic Press, 1990.
N P Mendler. Recursive Types and Type Constraints in Second-Order
Lambda-Calculus. In Proc LICS'87, pp 30-36. IEEE CS Press, 1987.
N P Mendler. Inductive Types and Type Constraints in Second-Order
Lambda-Calculus. Annals Pure Appl Logic, 51(1-2):159-172, 1991.
H Geuvers. Inductive and Coinductive Types with Iteration and
Recursion. In Informal Proc WS on Types for Proofs and Programs '92,
pp 193-217. Chalmers and Go"teborg U, 1992.
F Pfenning and Chr Paulin-Mohring. Inductively Defined Types in the
Calculus of Constructions. In Proc MFPS'89, v 442 of LNCS, pp
209-228. Springer, 1990.
Th Coquand and Chr Paulin. Inductively Defined Types (Preliminary
Version). Proc COLOG'88, v 417 of LNCS, pp 50-66. Springer, 1990.
C-E Ore. The Extended Calculus of Constructions ({ECC}) with Inductive
Types. Inform and Comput, 89(2):231-264, 1992.
P Dybjer. Inductive Families. Formal Aspects of Computing,
6(4):440-465, 1994.