A semantical storage operator theorem for all types. (English) Zbl 0899.03014

Raffalli, Christophe

Ann. Pure Appl. Logic 91, No. 1, 17-31 (1998).

The notion of storage operator was introduced by J.-L. Krivine to simulate, for a given set of terms, “call by value” in a “call by name”. The storage operator theorem is valid for a type \(D\) if any term of type \(\neg D\to\neg D^*\) is a storage operator for the elements of \(D\) (\(D^*\) being the Gödel translation of \(D\)). Krivine proved the storage operator theorem for the type of integer in the AF2 type system. This result has been extended to any type with only positive \(\forall\)-quantifiers by Krivine, using a semantical proof, and by Nour (using a syntactic proof). The author gives a new notion of semantical storage operator which is equivalent to Krivine and Nour’s notion for data-types. Its new storage operator theorem gives a sufficient condition to ensure the existence of semantical storage operators for an arbitrary type. The proof technique is a simplification of Krivine’s techniques using only 2 variables (while Nour uses the directed \(\lambda\)-calculus).

Reviewer: Karim Nour (Le Bourget-du-Lac)

MSC:

03B40	Combinatory logic and lambda calculus
68Q60	Specification and verification (program logics, model checking, etc.)
03F35	Second- and higher-order arithmetic and fragments

Keywords:

lambda-calculus; storage operator; Gödel translation; AF2 type system; data-types

References:

[1]	Barendregt, H. P., The Lambda Calculus: its Syntax and Semantics (1984), North-Holland: North-Holland Amsterdam · Zbl 0551.03007
[3]	Krivine, J.-L., Opérateurs de mise en mémoire et traduction de Godël, (Equipe de Logique de Paris 7. Equipe de Logique de Paris 7, Technical Report, 3 (December 1989)) · Zbl 0712.03009
[4]	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
[5]	Krivine, J.-L., Lambda-Calculus: Types and Models, Computers and their Applications (1993), Ellis Horwood: Ellis Horwood Chichester · Zbl 0779.03005
[6]	Krivine, J.-L., Mise en mémoire, preuve général (1993), manuscript
[7]	Krivine, J.-L., Classical logic, storage operators and second order λ-calculus, Ann. Pure Appl. Logic, 68, 53-78 (1994) · Zbl 0814.03009
[8]	Krivine, J.-L.; Parigot, M., Programming with proofs, Inform. Process. Cybernet., EIK-26, 3, 149-167 (1990) · Zbl 0699.68020
[9]	Leivant, D., Reasoning about functional programs and complexity classes associated with type disciplines, (24th Ann. Symp. on Foundations of Computer Science, vol. 44 (1983)), 460-469
[10]	Nour, K., Opérateurs de mise en mémoire en lambda-calcul pur et typé, (Ph.D. Thesis (1993), Université de Savoie)
[11]	Nour, K., A general type for storage operator, Math. Logic Quart., 41, 505-514 (1995) · Zbl 0837.03014
[12]	Nour, K., Storage operator and ∀-positive types in system TTR, Math. Logic Quart., 42, 2, 349-368 (1996) · Zbl 0852.03006
[13]	Nour, K., Storage operators and ∀-positive types, Inform. Théorique Appl., 30, 3, 261-293 (1996) · Zbl 0869.03009
[14]	Nour, K.; David, R., Storage operator and directed λ-calculus, J. Symbolic Logic, 60, 4, 1050-1086 (1995) · Zbl 0852.03007
[15]	Parigot, M., Recursive programming with proofs, Theoret. Comput. Sci., 94, 335-356 (1992) · Zbl 0759.68014
[16]	Parigot, M., Strong normalization for second order classical natural deduction, Logic Comput. Sci., 39-46 (1993)
[17]	Raffalli, C., L’ Arithmétiques Fonctionnelle du Second Ordre avec Points Fixes, (Ph.D. Thesis (Février 1994), Université Paris 7)