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