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

[David CHEMOUIL]

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
> <anstenklev at gmail.com> 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>