[TYPES] Gödel's T extended with an eta-like rule for the recursor

[Frédéric Blanqui]

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