CODEWITHSUNDEEP
haskelllambda-calculus
SoMax
SoMax

Reputation: 85

Alpha equivalence between variables in lambda calculus

Just a fairly simple question (so it seems to me). If two variables (x)(x) are alpha equivalent. Is (x1x2)(x2x1) alpha equivalent?

Upvotes: 4

Views: 5689

Answers (1)

Benjamin Hodgson
Benjamin Hodgson

Reputation: 44603

Two terms are alpha-equivalent iff one can be converted into the other purely by renaming bound variables.

A variable is considered to be a bound variable if it matches the parameter name of some enclosing lambda. Otherwise it's a free variable. Here are a few examples:

λx. x          -- x is bound
λx. y          -- y is free
λf. λx. f x y  -- f and x are bound, y is free
f (λf. f x)    -- the first f is free; the second is bound. x is free
z              -- z is free

Basically, "bound" and "free" roughly correspond to the notions of "in scope" and "out of scope" in procedural languages.

Alpha-equivalence basically captures the idea that it's safe to rename a variable in a program if you also fix all the references to that variable. That is, when you change the parameter of a lambda term, you also have to go into the lambda's body and change the usages of that variable. (If the name is re-bound by another lambda inside the first lambda, you'd better make sure not to perform the renaming inside the inner lambda.)

Here are some examples of alpha-equivalent terms:

λx. x   <->   λy. y   <->   λberp. berp
λx. λf. f x   <->   λx. λg. g x   <->   λf. λx. x f   <->  λx1. λx2. x2 x1
λf. λf. f f   <->   λg. λf. f f   <->   λf. λg. g g

So is x x alpha-equivalent to x1x2 x1x2? No! x is free in the first term, because it's not bound by an enclosing lambda. (Perhaps it's a reference to a global variable.) So it's not safe to rename it to x1x2.

I suspect your tutor really meant to say that λx. x x is alpha-equivalent to λx1x2. x1x2 x1x2. Here the x is bound by the lambda, so you can safely rename it.

Is x1 x2 alpha-equivalent to x2 x1? For the same reason, no.

And is λx1. λx2. x1 x2 equivalent to λx1. λx2. x2 x1? Again, no, because this isn't just a renaming - the x1 and x2 variables moved around.

However, λx1. λx2. x1 x2 is alpha-equivalent to λx2. λx1. x2 x1:

  1. rename x1 to some temporary name like z: λz. λx2. z x2
  2. rename x2 to x1: λz. λx1. z x1
  3. rename z back to x2: λx2. λx1. x2 x1

Getting renaming right in a language implementation is a fiddly enough problem that many compiler writers opt for a nameless representation of terms called de Bruijn indices. Rather than using text, variables are represented as a number measuring how many lambdas away the variable was bound. A nameless representation of λx2. λx1. x2 x1 would look like λ. λ. 2 1. Note that that's exactly the same as the de Bruijn representation of λx1. λx2. x1 x2. de Bruijn indices thoroughly solve the problem of alpha-equivalence (although they are quite hard to read).

Upvotes: 20

Related Questions