Computational adequacy for recursive types in models of intuitionistic set theory
Proceedings - Symposium on Logic in Computer Science - Trang 287-298
Tóm tắt
We present a general axiomatic construction of models of FPC, a recursively typed lambda-calculus with call-by-value operational semantics. Our method of construction is to obtain such models as full subcategories of categorical models of intuitionistic set theory. This allows us to obtain a notion of model that encompasses both domain-theoretic and realizability models. We show that the existence of solutions to recursive domain equations, needed for the interpretation of recursive types, depends on the strength of the set theory. The internal set theory of an elementary topos is not strong enough to guarantee their existence. However, solutions to recursive domain equations do exist if models of intuitionistic Zermelo-Fraenkel set theory are used instead We apply this result to interpret FPC, and we provide necessary and sufficient conditions on a model for the interpretation to be computationally adequate, i.e. for the operational and denotational notions of termination to agree.
Từ khóa
#Set theory #Flexible printed circuits #Equations #Sufficient conditions #Informatics #Computational modeling #Logic #Computer scienceTài liệu tham khảo
10.1016/S0168-0072(00)00014-2
10.1017/S0960129597002387
10.1007/978-1-4471-0615-9
10.1109/LICS.1991.151640
10.1017/CBO9780511752483
taylor, 1999, Practical Foundations
longley, 1995, Realizability Toposes and Language Semantics
jacobs, 1999, Categorical Logic and Type Theory
10.1016/S0022-4049(96)00108-9
hyland, 1991, First steps in synthetic domain theory, Category Theory Proc Como 1990, 131
10.1017/S0305004100057534
10.1017/S0960129500001481
10.1109/LICS.1990.113762
10.1006/inco.1994.1017
10.1016/0304-3975(77)90044-5
plotkin, 1985, Denotational Semantics With Partial Functions
10.1017/S096012959900273X
rosolini, 1986, Continuity and Effectivity in Topoi
10.1016/S0049-237X(09)70162-4
scott, 1980, Relating theories of the ?-calculus, To H B Curry, 403
simpson, 1992, Recursive types in Kleisli categories
10.1007/3-540-63172-0_36
10.1017/CBO9780511526565
10.1016/S0049-237X(09)70129-6
10.1007/3-540-57182-5_14
10.1007/10703163_22
10.1007/BFb0084215
10.1109/LICS.1990.113772
10.1137/0211062
10.1016/S0304-3975(00)00221-8
10.1109/LICS.1999.782592
10.1109/LICS.1997.614954
10.1016/0890-5401(92)90019-C
freyd, 1992, Remarks on algebraically compact categories, Applications of Categories in Computer Science, 95, 10.1017/CBO9780511525902.006