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

Anne Preller; Patrice Duroux

doi:10.1051/ita:1999115

Back

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

Journal article

Peer reviewed

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

Anne Preller and Patrice Duroux

RAIRO - Theoretical Informatics and Applications (RAIRO: ITA), Vol.33(3), pp.227-257

03/1999

DOI: https://doi.org/10.1051/ita:1999115

Abstract

cc:03F05

cc:03B25

cc:18D15

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.

Files and links (1)

url

Find in HALView

Metrics

1 Record Views

Details

Title: Normalisation of the Theory T of Cartesian Closed Categories and Conservativity of Extensions T [ x ] of T
Creators - without role: Anne Preller - Université de Montpellier, Laboratoire d'Informatique de Robotique et de Microélectronique de Mtp - LIRMM
Patrice Duroux - Université de Montpellier, Laboratoire d'Informatique de Robotique et de Microélectronique de Mtp - LIRMM
Publication Details: RAIRO - Theoretical Informatics and Applications (RAIRO: ITA), Vol.33(3), pp.227-257
Identifiers: 9963957209311
Academic Unit: Laboratoire d'Informatique de Robotique et de Microélectronique de Mtp - LIRMM
Language: English
Resource Type: Journal article
Local Fields: hal-05125536