Strong storage operators and data types (Q1805408)

The storage operators were introduced by \textit{J. L. Krivine} [RAIRO Inf. Théor. Appl. 25, No. 1, 67-84 (1991; Zbl 0717.03003)]; they are closed \(\lambda\)-terms which, for some fixed data type (the integers for example), allow to simulate ``call by value'' while using ``call by name''. \textit{J. L. Krivine} showed that such operators can be typed, in the \({\mathcal A}{\mathcal F}2\) type system, using Gödel's translation from classical to intuitionistic logic [Arch. Math. Logic 30, No. 4, 241-267 (1990; Zbl 0712.03009)]. This paper studies the existence of storage operators which give a normal form as result (strong storage operators) for recursive and iterative representation of data in \(\lambda\)-calculus. We obtain the following result: We can find typed strong storage operators for the recursive representations of a data type, but that is not the case for the iterative representations of an infinite data type. We give the proof of this result in the case of integers.