[TYPES] ?==?utf-8?q? ?==?utf-8?q? Gödel's T extended with an eta-like rule for the recursor
Sergei Soloviev
Sergei.Soloviev at irit.fr
Tue Feb 5 05:28:30 EST 2019
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
More information about the Types-list
mailing list