Geodesic
A Note on Rewriting Theory for Uniqueness of Iteration
Theory and applications of categories, The Lambek Festschrift, Tome 6 (1999), pp. 47-64.

Voir la notice de l'article provenant de la source Theory and Applications of Categories website

Uniqueness for higher type term constructors in lambda calculi (e.g. surjective pairing for product types, or uniqueness of iterators on the natural numbers) is easily expressed using universally quantified conditional equations. We use a technique of Lambek [18] involving Mal'cev operators to equationally express uniqueness of iteration (more generally, higher-order primitive recursion) in a simply typed lambda calculus, essentially Godel's T [29,13]. We prove the following facts about typed lambda calculus with uniqueness for primitive recursors: (i) It is undecidable, (ii) Church-Rosser fails, although ground Church-Rosser holds, (iii) strong normalization (termination) is still valid. This entails the undecidability of the coherence problem for cartesian closed categories with strong natural numbers objects, as well as providing a natural example of the following computational paradigm: a non-CR, ground CR, undecidable, terminating rewriting system.
Classification :
Keywords: typed lambda calculus, rewriting theory, strong normalization, Mal'cev operations. 
@article{TAC_1999_6_a3,
     author = {M. Okada and P. J. Scott},
     title = {A {Note} on {Rewriting} {Theory} for {Uniqueness} of {Iteration}},
     journal = {Theory and applications of categories},
     pages = {47--64},
     publisher = {mathdoc},
     volume = {6},
     year = {1999},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/TAC_1999_6_a3/}
}
TY  - JOUR
AU  - M. Okada
AU  - P. J. Scott
TI  - A Note on Rewriting Theory for Uniqueness of Iteration
JO  - Theory and applications of categories
PY  - 1999
SP  - 47
EP  - 64
VL  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/TAC_1999_6_a3/
LA  - en
ID  - TAC_1999_6_a3
ER  - 
%0 Journal Article
%A M. Okada
%A P. J. Scott
%T A Note on Rewriting Theory for Uniqueness of Iteration
%J Theory and applications of categories
%D 1999
%P 47-64
%V 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/TAC_1999_6_a3/
%G en
%F TAC_1999_6_a3
M. Okada; P. J. Scott. A Note on Rewriting Theory for Uniqueness of Iteration. Theory and applications of categories, The Lambek Festschrift, Tome 6 (1999), pp. 47-64. http://geodesic.mathdoc.fr/item/TAC_1999_6_a3/