Constructing orders by means of inductive definitions

Guillaume Bonfante (1) , François Lamarche (1)

1 CALLIGRAMME - Linear logic, proof networks and categorial grammars

We present a class of algebraic theories that are enriched over a novel symmetrical monoidal closed structure on the category of graphs, whose free models are posets that are equipped with an induction principle, which is easily formalized in type theory. We give examples.

Mots clés: ordres; orders; induction; universal algebra; ordinals; algèbre universelle; ordinaux; martin lof

Domaines: Autre [cs.OH]

Guillaume Bonfante, François Lamarche. Constructing orders by means of inductive definitions. [Intern report] 99-R-035 || bonfante99a, 1999, 15 p. ⟨inria-00098791⟩