[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hello. Okada and Scott proved that it terminates and is ground confluent
but not confluent:
https://keio.pure.elsevier.com/en/publications/a-note-on-rewriting-theory-for-uniqueness-of-iteration
A note on rewriting theory for uniqueness of iteration
Mitsuhiro Okada, P. J. Scott
Abstract
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.
Pages
47-64
Number of pages
18
Journal
Theory and Applications of Categories
Volume
6
Publication status
Published - 2000
Le 05/02/2019 à 09:18, Ansten Mørch Klev a écrit :
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Let N be the natural numbers and A any type in the hierarchy of simple
types over N. Let s : (N)N be the successor function and let f : (N)A be
arbitrary. Then, for variables x : N, y : A we may form the term
[x, y]f(s(x)) : (N)(A)A
Let R be the recursor for type A. Then, for any term n : N, we have
R( f(0) , [x, y]f(s(x)) , n ) : A
By the reduction rules for R one can see that f and R( f(0) , [x, y]f(s(x))
) agree on the numerals.
Suppose we add the following eta-like reduction rule to Gödel's T:
R( f(0) , [x, y]f(s(x)) , x ) --> f(x)
Is it known whether the resulting system is (strongly) normalizing and
confluent?
------------
Ansten Klev
Czech Academy of Sciences, Department of Philosophy
