Normalisation of the Theory T of Cartesian Closed Categories and Conservativity of Extensions T[x] of T
RAIRO - Theoretical Informatics and Applications (2010)
- Volume: 33, Issue: 3, page 227-257
- ISSN: 0988-3754
Access Full Article
top
Abstract
topHow to cite
topPreller, Anne, and Duroux, P.. "Normalisation of the Theory T of Cartesian Closed Categories and Conservativity of Extensions T[x] of T." RAIRO - Theoretical Informatics and Applications 33.3 (2010): 227-257. <http://eudml.org/doc/221951>.
@article{Preller2010,
abstract = {
Using an inductive definition of normal terms of the theory of Cartesian Closed
Categories with a given graph of distinguished morphisms, we give a reduction free
proof of the decidability of this theory. This inductive definition enables us to
show via functional completeness that extensions of such a theory by new constants
(“indeterminates”) are conservative.
},
author = {Preller, Anne, Duroux, P.},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {Cartesian closed categories; simply typed lambda calculus; rewrite system; graph of generators; inductive definition of normal terms; decidability; functional completeness},
language = {eng},
month = {3},
number = {3},
pages = {227-257},
publisher = {EDP Sciences},
title = {Normalisation of the Theory T of Cartesian Closed Categories and Conservativity of Extensions T[x] of T},
url = {http://eudml.org/doc/221951},
volume = {33},
year = {2010},
}
TY - JOUR
AU - Preller, Anne
AU - Duroux, P.
TI - Normalisation of the Theory T of Cartesian Closed Categories and Conservativity of Extensions T[x] of T
JO - RAIRO - Theoretical Informatics and Applications
DA - 2010/3//
PB - EDP Sciences
VL - 33
IS - 3
SP - 227
EP - 257
AB -
Using an inductive definition of normal terms of the theory of Cartesian Closed
Categories with a given graph of distinguished morphisms, we give a reduction free
proof of the decidability of this theory. This inductive definition enables us to
show via functional completeness that extensions of such a theory by new constants
(“indeterminates”) are conservative.
LA - eng
KW - Cartesian closed categories; simply typed lambda calculus; rewrite system; graph of generators; inductive definition of normal terms; decidability; functional completeness
UR - http://eudml.org/doc/221951
ER -
References
top- T. Altenkirch, M. Hofmann and T. Streicher, Categorical reconstruction of a reduction free normalisation proof, preliminary version, P. Dybjer and R. Pollacks, Eds., Proceedings CTCS '95, Springer, Lecture Notes in Computer Science 953 (1995) 182-199.
- U. Berger and H. Schwichtenberg, An inverse to the evaluation functional for typed λ-calculus, in Proc. of the 6th Annual IEEE Symposium of Logic in Computer Science (1991) 203-211.
- D. Cubric', Embedding of a free Cartesian Closed Category in the Category of Sets. J. Pure and Applied Algebra (to appear).
- D. Cubric', P. Dybjer and P. Scott, Normalization and the Yoneda Embedding, MSCS8 (1998) 153-192.
- R. Di Cosmo, Isomorphisms of Types, Birkhaeuser (1995).
- K. Dosen and Z. Petric', The maximality of Cartesian Categories, Rapport Institut de Recherche de Toulouse, CNRS, 97-42-R (1997).
- J. Lambek and P.J. Scott, Introduction to Higher Order Categorical Logic, Cambridge University Press (1989).
- A. Obtuowicz, Algebra of constructions I. The word problem for partial algebras. Inform. and Comput.73 (1987) 129-173.
NotesEmbed ?
topYou must be logged in to post comments.
To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.