[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear Ansten,
[Okada and Scott 1999] is certainly the paper to read here. The abstract
goes:
" 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. "
[Okada and Scott 1999] A Note on Rewriting Theory for Uniqueness of
Iteration
http://www.tac.mta.ca/tac/volumes/6/n4/6-04abs.html
Best regards,
david
Le 2019-02-05 11:28, Sergei Soloviev a écrit :
Dear Ansten,
We did work with David Chemouil on related questions, main results and
ideas
are in the papers
David Chemouil:
Isomorphisms of simple inductive types through extensional rewriting.
Mathematical Structures in Computer Science 15(5): 875-915 (2005)
David Chemouil:
An insertion operator preserving infinite reduction sequences.
Mathematical Structures in Computer Science 18(4): 693-728 (2008)
David Chemouil, Sergei Soloviev:
Remarks on isomorphisms of simple inductive types. Electr. Notes
Theor. Comput. Sci. 85(7): 106-124 (2003)
I have to check whether they cover directly your question, but in any
case there were
developped techniques that certainly could be useful.
All the best
Sergei Soloviev
Le Mardi 5 Février 2019 09:18 CET, Ansten Mørch Klev
<[email protected]> 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
--
David Chemouil
ONERA DTIS & Université de Toulouse
tel:+33-5-6225-2936
<http://www.onera.fr/staff/david-chemouil>
