Free variables list of a lambda expression

Question

I was just doing some homework for my upcoming OCaml test and I got into some trouble whatnot.

Consider the language of λ-terms defined by the following abstract syntax (where x is a variable):

t ::= x | t t | λx. t  

Write a type term to represent λ-terms. Assume that variables are represented as strings.

Ok, boy.

# type t = Var of string | App of (t*t) | Abs of string*t;;
type t = Var of string | App of (t * t) | Abs of (string * t)

The free variables fv(t) of a term t are defined inductively a follows:

fv(x) = {x}  
fv(t t') = fv(t) ∪ fv(t')  
fv(λx. t) = fv(t) \ {x}

Sure thing.

# let rec fv term = match term with
Var x -> [x]
  | App (t, t') -> (List.filter (fun y -> not (List.mem y (fv t'))) (fv t)) @ (fv t')
  | Abs (s, t') -> List.filter (fun y -> y<>s) (fv t');;
      val fv : t -> string list = <fun>

For instance,

fv((λx.(x (λz.y z))) x) = {x,y}.

Let's check that.

# fv (App(Abs ("x", App (Abs ("z", Var "y"), Var "z")), Var "x"));;
- : string list = ["y"; "z"; "x"]

I've checked a million times, and I'm sure that the result should include the "z" variable. Can you please reassure me on that?

Europium

No, z is not a free variable of (λz.y z) and therefore not a free variable of (λx.(x (λz.y z))) x. – Pigmentation

I'm still puzzling over why your code computes the wrong answer, but List.filter (fun y -> not (List.mem y (fv t'))) (fv t), while it seems correct to me so far, computes fv t' way to many times. You should compute it once with let fv_t' = fv t' in … and use fv_t'. – Pigmentation

@PascalCuoq I think I got it. I was reading (λz.y z) as ((λz.y) z) when in fact it should be read as (λz.(y z)). Thing is, nothing pointed me towards that kind of association. Thank you for the optimisation tip as well! – Europium

Yes, λ in the lambda-calculus associates the same as fun in OCaml. The expression fun x -> st uff is the same as fun x -> (st uff). – Pigmentation

Should we keep the question? – Europium

Well, I remember an entire class being confused until one of us figured out that “λ was just like fun in Caml”, so it is a valid question. Instead of deleting the question, you should write up your discovery as an answer and accept it. – Pigmentation

Very well, thank you again! – Europium

Answer 1

In the comments to the OP it has been pointed out by the kind @PasqualCuoq that λ in lambda calculus associates the same as fun in OCaml. That is, the term t in λx.t is evaluated greedily (see http://en.wikipedia.org/wiki/Lambda_calculus#Notation).

What this is means is that (λz.y z) is actually (λz.(y z)), and that the function above is correct, but the translation provided for the sample expression (λx.(x (λz.y z))) x isn't, as it should've been

(App(Abs("x", App(Var "x", Abs("z", App(Var "y", Var "z")))), Var "x"))

in place of

(App(Abs ("x", App (Abs ("z", Var "y"), Var "z")), Var "x"))

Here's to this awesome place called Stack Overflow!

Europium