A semantical storage operator theorem for all types
作者： Christophe Raffalli
DOI: 10.1016/S0168-0072(97)00041-9
关键词: Type (model theory) 、 Mathematics 、 Pure mathematics 、 Gödel 、 Set (abstract data type) 、 Operator (computer programming) 、 Term (logic) 、 Translation (geometry) 、 Order (group theory) 、 Algebra
摘要: Storage operators are λ-terms which simulate call-by-value in call-by-name for a given set of terms. Krivine's storage operator theorem shows that any term type ¬D → ¬D∗, where D∗ is the Godel translation D, terms D when data-type or formula with only positive second order quantifiers. We prove new semantical version valid every types. This also gives simpler proof using properties data-types.
elsevier.com
sci-hub.se 参考文章(12)
Karim Nour, Operateurs de mise en memoire en lambda-calcul pur et type Université Savoie Mont Blanc. ,(1993)
M. Parigot, J.-L. Krivine, Programming with proofs Journal of Automata, Languages and Combinatorics. ,vol. 26, pp. 149- 167 ,(1990)
Samir Farkh, Karim Nour, Résultats de complétude pour des classes de types du système $\mathcal {AF}2$ Theoretical Informatics and Applications. ,vol. 31, pp. 513- 537 ,(1997) , 10.1051/ITA/1997310605131
Karim Nour, Storage Operators and ∀-positive Types in TTR Type System Mathematical Logic Quarterly. ,vol. 42, pp. 349- 368 ,(1996) , 10.1002/MALQ.19960420130
Jean-Louis Krivine, Opérateurs de mise en mémoire et traduction de Gödel Archive for Mathematical Logic. ,vol. 30, pp. 241- 267 ,(1990) , 10.1007/BF01792986
Daniel Leivant, Reasoning about functional programs and complexity classes associated with type disciplines 24th Annual Symposium on Foundations of Computer Science (sfcs 1983). pp. 460- 469 ,(1983) , 10.1109/SFCS.1983.50
Michel Parigot, Recursive programming with proofs Theoretical Computer Science. ,vol. 94, pp. 335- 356 ,(1992) , 10.1016/0304-3975(92)90042-E
Jean-Louis Krivine, Classical logic, storage operators and second-order lambda-calculus Annals of Pure and Applied Logic. ,vol. 68, pp. 53- 78 ,(1994) , 10.1016/0168-0072(94)90047-7
M. Parigot, Strong normalization for second order classical natural deduction logic in computer science. pp. 39- 46 ,(1993) , 10.1109/LICS.1993.287602
Henk Barendregt, The Lambda Calculus. Its Syntax and Semantics ,(2012)