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

[Danko ILIK]

On Tue, Feb 05, 2019 at 09:18:30AM +0100, Ansten Mørch Klev wrote:
> 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?

Dear Ansten,

Maybe adding this kind of eta rule is not problematic when A is to
vary over simple types only. I don't know. However, in "reality" (in
proof assistants, in programming languages, or even category theory)
we often have to consider richer type structures, such as inductive
types.

And, in this case it still seems problematic to add eta rules, even
for special cases of the recursor which is the case distinction
operator for co-product types. If you want to browse through that
literature, I can point to the Related Works section of my paper
https://arxiv.org/abs/1502.04634 which should mention most of the
works on that problem.

Best regards,
Danko