Game Semantics for Untyped λβη-Calculus
作者： Pietro Di Gianantonio , Gianluca Franco , Furio Honsell
关键词: Normalisation by evaluation 、 Lambda calculus 、 Calculus 、 Current (mathematics) 、 Game semantics 、 Mathematics 、 Typed lambda calculus 、 Simply typed lambda calculus 、 Denotational semantics 、 Reduction (recursion theory)
摘要: We study extensional models of the untyped lambda calculus in setting game semantics. In particular, we show that, somewhat unexpectedly and contrary to what happens ordinary categories domains, all reflexive objects category games G, introduced by Abramsky, Jagadeesan Malacaria, induce same λ-theory. This is ℌ *, maximal theory induced already classical CPO model D ∞, Scott 1969. results indicates that current notion carries a very specific bias towards head reduction.
springer.com
sci-hub.st 参考文章(15)
Furio Honsell, Marina Lenisa, Final semantics for untyped λ-calculus Lecture Notes in Computer Science. pp. 249- 265 ,(1995) , 10.1007/BFB0014057
M. Coppo, M. Dezani-Ciancaglini, F. Honsell, G. Longo, Extended Type Structures and Filter Lambda Models Logic Colloquium '82. ,vol. 112, pp. 241- 262 ,(1984) , 10.1016/S0049-237X(08)71819-6
Guy McCusker, Samson Abramsky, Games for Recursive Types. formal methods. pp. 1- 20 ,(1994)
Samson Abramsky, Full Abstraction in the Lazy λ−calculus ,(1993)
Chantal Berline, From computation to foundations via functions and application: The l-calculus and its webbed models Theoretical Computer Science. ,vol. 249, pp. 81- 161 ,(2000) , 10.1016/S0304-3975(00)00057-8
Martin Hyland, A Syntactic Characterization of the Equality in Some Models for the Lambda Calculus Journal of the London Mathematical Society. ,vol. s2-12, pp. 361- 370 ,(1976) , 10.1112/JLMS/S2-12.3.361
Jean-Yves Girard, The system F of variable types, fifteen years later Theoretical Computer Science. ,vol. 45, pp. 159- 192 ,(1986) , 10.1016/0304-3975(86)90044-7
Furio Honsell, Simonetta Ronchi Della Rocca, An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus Journal of Computer and System Sciences. ,vol. 45, pp. 49- 75 ,(1992) , 10.1016/0022-0000(92)90040-P
Samson Abramsky, C-H Luke Ong, Full abstraction in the lazy lambda calculus Information & Computation. ,vol. 105, pp. 159- 267 ,(1993) , 10.1006/INCO.1993.1044
Samson Abramsky, Radha Jagadeesan, Games and full completeness for multiplicative linear logic Journal of Symbolic Logic. ,vol. 59, pp. 543- 574 ,(1994) , 10.2307/2275407