[FOM] Simply Typed Lambda Calculus

immanuel litzroth ilitzroth at gmail.com
Tue Jan 15 16:04:50 EST 2008

> So S might lead to intermediate terms which are not typeable, but my
> question is, as I am going from a typed to another typed term, are these
> intermediate untypeable terms somehow superfluous?

Why do you think beta/eta reduction might lead to untypeable terms when
the starting term is typed? Can you give an example?

More information about the FOM mailing list