John
John

Reputation: 429

Haskell - determine set of free and bounded variables of a function

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

Answers (1)

AndrewC
AndrewC

Reputation: 32455

General idea: bound vs free variables

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?

  • Yes - varname is bound.
  • No - varname appears free in the expression.

Let's look at your actual examples

Example 1

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

  • The initial \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}

Notation

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.)

Example 2

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 lambda
  • y1 is bound by a let now (more shadowing)
  • w is free
  • y2 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

Related Questions