×
Krivine, Jean-Louis

Classical logic, storage operators and second-order lambda-calculus. (English) Zbl 0814.03009

Ann. Pure Appl. Logic 68, No. 1, 53-78 (1994).
Storage operators, introduced by the author [Arch. Math. Logic 30, 241- 267 (1990; Zbl 0712.03009)], are a device to simulate call-by-value in a lambda-calculus with head-reduction. In this paper this concept is used to characterize the lambda-terms encoding integers in classical logic. Let \(\text{Nat} [x]\) be the formula expressing in second-order lambda- calculus (also with first-order variables and quantifiers) the data type of natural numbers. An important consequence of the normalization theorem is that if \(\vdash M: \text{Nat} [x]\), then \(M\) is beta-equivalent to \(\underline{n}\), the Church numeral for \(n\). When one extends the calculus with axioms (i.e., when the typing context is extended with typed constants \(c_ i: \sigma_ i\)), this in general is no longer true. The paper considers the especially relevant extension obtained with the axiom \({\mathbf c}\): \(\forall X(\neg\neg X\to X)\). This system, in view of Gödel’s double-negation translation, axiomatizes classical logic. M. Parigot [Lect. Notes Comput Sci. 592, 361-380 (1991)] has shown that closed elements of type NAT in this extended system can be characterized in terms of storage operators: If \({\mathbf c} \vdash M: \text{Nat} [n]\) and if \(T\) is a storage operator for integers, then, for any variable \(f\), \(TfM\) reduces by head reduction to \(fN\), with \(N\) beta- equivalent to \(\underline {n}\), depending only on \(n\) (and not on \(M\)). The nontrivial proof uses a realizability argument. All the preliminaries, including those on storage operators and the proof of Parigot’s result, are clearly explained in the first part (pp. 53-70) of the paper. The result, besides its direct technical interest, is of potential relevance also for the ongoing research on the extraction of programs from classical proofs.
Reviewer: S.Martini (Pisa)

Cited in 2 Reviews
Cited in 25 Documents

MSC:

03B40 Combinatory logic and lambda calculus
68N15 Theory of programming languages

Keywords:

continuations; System F; second-order lambda-calculus; data type of natural numbers; classical logic; storage operators; head reduction

Citations:

Zbl 0712.03009
PDF BibTeX XML Cite
\textit{J.-L. Krivine}, Ann. Pure Appl. Logic 68, No. 1, 53--78 (1994; Zbl 0814.03009)
Full Text: DOI

References:

[1] Barendregt, H., The Lambda Calculus (1984), North-Holland: North-Holland Amsterdam · Zbl 0549.03012
[2] Felleisen, M., The calculi of \(λ_v\)-CS conversion: a syntactic theory of control and state in imperative higher order programming, Ph.D. Thesis (1987), Indiana Univ
[3] Girard, J. Y., Une extension de l’interprétation de Gödel á l’analyse, (Proc. 2nd Scand. Logic Symp. (1971), North-Holland: North-Holland Amsterdam), 63-92
[4] Girard, J. Y., A new constructive logic: classical logic (1991), preprint · Zbl 0752.03027
[5] Girard, J. Y., On the unity of logic, Ann. Pure Appl. Logic, 59, 201-217 (1993) · Zbl 0781.03044
[6] Griffin, T., A formulae-as-type notion of control, Conf. Record of the 17th ACM Symp. on Principles of Programming Languages (1990)
[7] Krivine, J. L., Lambda-calcul, types et modéles (1990), Masson: Masson Paris · Zbl 0697.03004
[8] Krivine, J. L., Opérateurs de mise en mémoire et traduction de Gödel, Arch. Math. Logic, 30, 241-267 (1990) · Zbl 0712.03009
[9] Krivine, J. L.; Parigot, M., Programming with proofs, J. Inform. Process. Cybernet. EIK, 26, 3, 149-167 (1990) · Zbl 0699.68020
[10] Leivant, D., Reasoning about functional programs and complexity classes associated with type disciplines, 24th Ann. Symp. on Found. of Comp. Sci., 460-469 (1983)
[11] Murthy, C., Extracting constructive content from classical proofs, Ph.D. Thesis (1990), Cornell Univ
[12] Parigot, M., Free deduction: an analysis of computations in classical logic, (Proc. of Logic Progr. and Automatic Reasoning, 592 (1991), Springer: Springer Berlin), 361-380, St. Petersbourg, Lecture Notes in Computer Science · Zbl 0925.03203
[13] Parigot, M., λμ-calculus: an algorithmic interpretation of classical natural deduction, (Proc. of Logic Progr. and Automatic Reasoning, 624 (1992), Springer: Springer Berlin), 190-201, St Petersbourg, Lecture Notes in Computer Science · Zbl 0925.03092
[14] Parigot, M., Séminaire de Logique, Université Paris, VII (1992)
[15] Plotkin, G., Call-by-name, call-by-value, and the λ-calculus, Theoret. Comp. Sci., 1, 125-159 (1975) · Zbl 0325.68006
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.