# 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

top## How 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). Zbl0898.18004
- D. Cubric', P. Dybjer and P. Scott, Normalization and the Yoneda Embedding, MSCS8 (1998) 153-192. Zbl0918.03012
- R. Di Cosmo, Isomorphisms of Types, Birkhaeuser (1995). Zbl0819.03006
- K. Dosen and Z. Petric', The maximality of Cartesian Categories, Rapport Institut de Recherche de Toulouse, CNRS, 97-42-R (1997). Zbl0978.18001
- J. Lambek and P.J. Scott, Introduction to Higher Order Categorical Logic, Cambridge University Press (1989). Zbl0596.03002
- A. Obtuowicz, Algebra of constructions I. The word problem for partial algebras. Inform. and Comput.73 (1987) 129-173. Zbl0653.03010

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.