Replacing with fresh variables during beta-reduction

Moderator: Type Systems of Programming Languages

AlexanderF
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 140
Registriert: 2. Mai 2010 17:55

Replacing with fresh variables during beta-reduction

Beitrag von AlexanderF »

hello,

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?

regards,
Alexander

erdweg
Moderator
Moderator
Beiträge: 60
Registriert: 28. Mär 2013 10:08

Re: Replacing with fresh variables during beta-reduction

Beitrag von erdweg »

The problem exists whenever free variables exist in the term we substitute into some expression.

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.

Sebastian

AlexanderF
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 140
Registriert: 2. Mai 2010 17:55

Re: Replacing with fresh variables during beta-reduction

Beitrag von AlexanderF »

ok,

thanks for the answer.

Antworten

Zurück zu „Type Systems of Programming Languages“