[FOM] Simply Typed Lambda Calculus
obua at in.tum.de
Fri Jan 11 22:15:39 EST 2008
I have the following question concerning the simply typed
(non-polymorphic) lambda calculus with constants and axioms for those
The axioms are all of the form p = t, where p is a linear pattern and
all the free variables in t are bound by p. All the axioms are typed.
Assume that I have two terms A and B, both typed.
Assume further that I forget now about all types and use beta , eta
conversions and the axioms as if I would do in untyped lambda calculus.
Doing this, I manage to get from A to B.
My question is, can I therefore also get from A to B if I DO NOT forget
about the types but respect them? In particular, certain eta
abstractions might not be possible that I could use
in the untyped setting but not in the typed setting.
I guess for type theorists this is a no-brainer. It would be great if
someone could point me to an answer of this question in the literature.
More information about the FOM