Reputation: 429
I have to determine the set of free and bounded variables of the function s1 and s2:
s1 := \x -> if y then \z -> (x \y -> y) else (\z -> w) x
So, for s1 I'll write:
FV(s1):= FV (y) ∪ FV (x) ∪ FV (w)
Am I correct? Or should it be:
FV(s1):= FV (y) ∪ FV (x) ∪ FV (y) ∪ FV (w) ∪ FV (x)
since y and x are two times free. Once y in If and then result of -> y and for x: x is free once in the result of \z and second at the end.
The bounded variables would be:
BV(s1):= BV (x) ∪ BV (z) ∪ BV (y) ∪ BV (z)
since z occurs twice as bounded var.
In the same way I'd determine the FVs and BVs of s2:
s2 := let f x1 x2 = y1 (\x -> x2) in let y1 = f w (f y2 y2), y2 = y1 in f
FV(s2):= FV (y1) ∪ FV (x2) ∪ FV (w) ∪ FV (y1)
BV(s2):= BV (f) ∪ BV (x1) ∪ BV (x2) ∪ BV (x) ∪ BV (y1)
Could you please tell me whether I'm correct or wrong?
Thanks in advance
Upvotes: 1
Views: 2182
Reputation: 32455
A rule of thumb for free and bound variables is that the value of a free variable affects the value of the expression.
For a simple example, if I defined identity x = x
and separately said x = 6
, it wouldn't change the fact that identity 10
is 10
; in identity x = x
, the variable x
is bound because it just stands for whatever input there is. We can write identity y = y
without changing the meaning of the function.
Conversely, if we define gimmez x = z
, z
isn't bound. If we separately say z = 6
then gimmez
does something very different to if we said z = putStrLn "zed zed zed zed can you tell I'm British?"
, or gimmez x = zz
. In either case, the function gimmez
has changed - the z
wasn't bound.
Can I do find-and-replace varname
for othervarname
without changing the meaning?
varname
is bound. varname
appears free in the expression.Let's look at your actual examples
s1 := \x -> if y then \z -> (x \y -> y) else (\z -> w)
You wrote FV(s1):= FV (y) ∪ FV (x) ∪ FV (w)
or FV(s1):= FV (y) ∪ FV (x) ∪ FV (y) ∪ FV (w) ∪ FV (x)
Let's look at all the variables in turn
\x ->
binds x
for the scope of the lambda - to the end of the line. It's not a free variable at all.y
is free after the if
, but bound in the invalid expression (x \y -> y)
. The second occurrence in that bracket has the value of the bound y, rather than the free one. This obliteration of an otherwise free variable is called shadowing. y
is free in the expression, but only because of its first appearance.z
is bound in the final lambda expression.w
isn't bound anywhere - it's free.Summary: y
and z
are free. x
and z
are bound, y
is shadowed - it also occurs as a bound variable later in the expression. FV(s1) = {y,z}
, and BV(s1)={x,z,y}
I disagree with the use of the notation FV(s1):= FV (y) ∪ FV (w)
. This suggests that to find the free variables of s1
I should look at the free variables of y
and w
. I disagree - y
and z
are the free variables of s1
. It is true that if I wanted to get the free variables of the module in which s1
is defined I would need to add FV (y) ∪ FV (w)
, but that's a different question.
(The notation ∪
indicates set union. Things are either in or out of a set, you don't need to add them multiple times.)
s2 := let f x1 x2 = y1 (\x -> x2) in let y1 = f w (f y2 y2), y2 = y1 in f
The let f x1 x2 =
binds f
, x1
and x2
, even if f
feels different; they all introduce a new variable which would shadow any external definition with the same name, and find-and-replacing them in the expression wouldn't change its meaning, so they're bound.
f
, x1
, x2
are bound by the let
.y1
is free the first time it appears - the second let
binding is not in scope here.x
is bound by a lambday1
is bound by a let
now (more shadowing)w
is freey2
looks free at first, but is actually retrospectively bound in the expression y2 = y1
FV(s2):= {y1, w}
BV(s2):= {f, x1, x2, x, y1, y2}
Upvotes: 3