#
A Note on Rewriting Theory for Uniqueness of Iteration

##
M. Okada and P. J. Scott

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.

Keywords: typed lambda calculus, rewriting theory, strong normalization, Mal'cev operations.

1991 MSC:

*Theory and Applications of Categories*, Vol. 6, 1999, No. 4, pp 47-64.

http://www.tac.mta.ca/tac/volumes/6/n4/n4.dvi

http://www.tac.mta.ca/tac/volumes/6/n4/n4.ps

http://www.tac.mta.ca/tac/volumes/6/n4/n4.pdf

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n4/n4.dvi

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n4/n4.ps

TAC Home