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?

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!