A semantical storage operator theorem for all types
type: Item
instance of: scholarly article
title: A semantical storage operator theorem for all types
zbMATH Open document ID: 0899.03014
DOI: 10.1016/S0168-0072(97)00041-9
author: Christophe Raffalli
published in: Annals of Pure and Applied Logic
publication date: 1998-03-25T00:00:00Z
review text: 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).
reviewed by: Karim Nour
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03F35
zbMATH DE Number: 1133082
zbMATH Keywords: lambda-calculus
zbMATH Keywords: storage operator
zbMATH Keywords: Gödel translation
zbMATH Keywords: AF2 type system
zbMATH Keywords: data-types
MaRDI profile type: Publication
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation)
cites work: Q4274979
cites work: Classical logic, storage operators and second-order lambda-calculus
cites work: Q3477935
cites work: A General Type for Storage Operators
cites work: Storage Operators and ∀‐positive Types in TTR Type System
cites work: Opérateurs de mise en mémoire et types $\forall $-positifs
cites work: Storage operators and directed lambda-calculus
cites work: Recursive programming with proofs
description: scientific article; zbMATH DE number 1133082