Informatics Report Series


Report   

EDI-INF-RR-0607


Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Home
Title:Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory
Authors: Alexander Simpson
Date: 2004
Publication Title:Annals of Pure and Applied Logic
Publisher:Elsevier
Publication Type:Journal Article Publication Status:Published
Volume No:130 Page Nos:207-275
DOI:10.1016/j.apal.2003.12.005
Abstract:
This paper provides a unifying axiomatic account of the interpretation of recursive types that incorporates both domain-theoretic and realizability models as concrete instances. Our approach is to view such models as full subcategories of categorical models of intuitionistic set theory. It is shown that the existence of solutions to recursive domain equations depends upon the strength of the set theory. We observe that the internal set theory of an elementary topos is not strong enough to guarantee their existence. In contrast, as our first main result, we establish that solutions to recursive domain equations do exist when the category of sets is a model of full intuitionistic Zermelo-Fraenkel set theory. We then apply this result to obtain a denotational interpretation of FPC, a recursively typed lambda-calculus with call-by-value operational semantics. By exploiting the intuitionistic logic of the ambient model of intuitionistic set theory, we analyse the relationship between operational and denotational semantics. We first prove an ``internal'' computational adequacy theorem: the model always believes that the operational and denotational notions of termination agree. This allows us to identify, as our second main result, a necessary and sufficient condition for genuine ``external'' computational adequacy to hold, i.e. for the operational and denotational notions of termination to coincide in the real world. The condition is formulated as a simple property of the internal logic, related to the logical notion of 1-consistency. We provide useful sufficient conditions for establishing that the logical property holds in practice. Finally, we outline how the methods of the paper may be applied to concrete models of FPC In doing so, we obtain computational adequacy results for an extensive range of realizability and domain-theoretic models.
Links To Paper
No links available
Bibtex format
@Article{EDI-INF-RR-0607,
author = { Alexander Simpson },
title = {Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory},
journal = {Annals of Pure and Applied Logic},
publisher = {Elsevier},
year = 2004,
volume = {130},
pages = {207-275},
doi = {10.1016/j.apal.2003.12.005},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh