List of variable variables lambda expressions

Question

I was just doing my homework for my upcoming OCaml test, and I was having problems with something else.

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

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

Write a type term to represent λ terms. Suppose variables are represented as strings.

Okay 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 t are defined inductively a:

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

Of course.

 # 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.yz))) x) = {x,y}. 

Check that out.

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

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

Answer 1

In the comments on OP, it was pointed out by @PasqualCuoq that λ in the lambda calculus matches the same as fun in OCaml. That is, the term t in λx.t is greedy (see http://en.wikipedia.org/wiki/Lambda_calculus#Notation ).

What this means is that (λz.yz) is actually (λz.(yz)) , and that the above function is true, but the translation provided for the approximate expression (λx.(x (λz.yz))) x , is not, as it should be

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

instead

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

Here in this amazing place called stack overflow!