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

[Danel Ahman]

Dear Ansten, 

I believe your questions are answered in this paper from Okada and Scott

  http://www.tac.mta.ca/tac/volumes/6/n4/6-04abs.html <http://www.tac.mta.ca/tac/volumes/6/n4/6-04abs.html>


Best,
Danel


> On 5 Feb 2019, at 09:18, Ansten Mørch Klev <anstenklev at gmail.com> wrote:
> 
> [ 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