Normalisation of the Theory T of Cartesian Closed Categories and Conservativity of Extensions T[x] of T

Anne Preller; P. Duroux

RAIRO - Theoretical Informatics and Applications (2010)

  • Volume: 33, Issue: 3, page 227-257
  • ISSN: 0988-3754

Abstract

top
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.

How to cite

top

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

NotesEmbed ?

top

You 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.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.