# [FOM] Simply Typed Lambda Calculus

Steven Obua obua at in.tum.de
Thu Jan 17 20:09:24 EST 2008

Chad,

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