[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
