Game Semantics for Untyped lambda beta eta-Calculus
作者： Pietro Di Gianantonio , Furio Honsell , Gianluca Franco
DOI:
关键词:
摘要: 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 H*, maximal theory induced already classical CPO model D∞ Scott 1969. results indicates that current notion carries a very specific bias towards head reduction.
acm.org 参考文章(13)
Christopher P. Wadsworth, The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus SIAM Journal on Computing. ,vol. 5, pp. 488- 521 ,(1976) , 10.1137/0205036
Furio Honsell, Marina Lenisa, Final Semantics for untyped lambda-calculus international conference on typed lambda calculi and applications. pp. 249- 265 ,(1995)
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)
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
Jan van Leeuwen, Handbook of theoretical computer science (vol. B): formal models and semantics MIT Press. ,(1990)
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