Moderator: Type Systems of Programming Languages
we had the convention that when performing the beta-reduction on lambda abstractions, e.g. in:
(\y. t') [x := t]
we replace y with a free variable y0 in (\y. t') before performing the beta reduction,
if y is occurs free in t.
So that we have:
(\y0. t'[y := y0]) [x := t]
This is necessary e.g. in the following example:
\y (\x. \y. x + y) y
my question is:
the above example is only problematic, if we reduce under the lambda abstraction (what we didn't in the lecture).
It seems to me that the generation and replacing with fresh variables is not necessary,
if we dont have reduction under lambda abstractions,
and we do not allow expressions with free variables (except for sub expressions), like (\x. \y. x + y) y.
is this observation correct?
You are right that this does not happen in the simply-typed lambda calculus when disallowing reduction under lambdas. However, there are two reasons this is important nevertheless: First, there may be terms with free variables when doing metatheory, that is, proving theoremes about the simply-typed lambda calculus. Second, when investigating other languages (like object-orineted languages) there may be terms with free variables. So it makes sense to discuss this once, and be done with it.
thanks for the answer.