[FOM] Simply Typed Lambda Calculus

[Steven Obua]

Chad,

> Does this answer your question?

thank you a lot for your counterexample, yes it is an answer to my 
question. I would not have thought of this example, I thought more along 
the problems that eta abstraction/reduction could introduce:

1. assume I have a constant c::int
2. eta expansion goes to  A = (\lambda x. c x)
3. now I go back to c via eta reduction

Obviously in the above, i dont need the intermediate, untypeable step.
But the untypeability of A has a different quality than the 
untypeability of your Y, because A could be typed by just changing the 
type of c to int -> int.

What happens if one restricts the use of axioms "from left to right" 
only? So beta can be used in both directions, eta also in both 
directions, but rewriting only in one direction.
This seems to be also more in sync with the idea that there should be no 
free variables on the right hand side of the rules. Because if one can 
use the axioms in both directions, then your system

(1) C x = Q x x
(2) D x = Q (N x) x
(3) C x = T
(4) D x = F

is equal to the system

(1) C x = Q x x
(2) D x = Q (N x) x
(3') T = C x
(4) D x = F

which does NOT anymore obey the condition of no free variables on the 
right hand side. Therefore with directed rewriting

T => C Y => Q Y Y => Q (N Y) Y => D Y => F

would not be a counterexample anymore, because the first step T => C Y 
could not be executed anymore.

So I guess now it should not be possible anymore to introduce new equations?

Best,

Steven