6

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?

rickmeizter
  • 131
  • 1
  • 7
  • 2
    No, `z` is not a free variable of `(λz.y z)` and therefore not a free variable of `(λx.(x (λz.y z))) x`. – Pascal Cuoq Dec 09 '12 at 00:30
  • 1
    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'`. – Pascal Cuoq Dec 09 '12 at 00:35
  • 1
    @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! – rickmeizter Dec 09 '12 at 00:41
  • 2
    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)`. – Pascal Cuoq Dec 09 '12 at 00:43
  • Should we keep the question? – rickmeizter Dec 09 '12 at 00:46
  • 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. – Pascal Cuoq Dec 09 '12 at 00:52
  • Very well, thank you again! – rickmeizter Dec 09 '12 at 00:54

1 Answers1

4

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!

rickmeizter
  • 131
  • 1
  • 7