Ok, so that dilutes the 'pure' of the functional part. I know that in practice functional programs have an if to force termination, but the lambda calculus deals with abstracts. Anything evaluating lambda expressions then has to deal with that or you'd have to expand the syntax of the calculus to contain a termination function which 'magically' decides that enough is enough.

According to the definition all functions are unary functions, an if would have to be a binary function wouldn't it ?

With currying, you can easily make functions of n variables out of functions of one variable. To avoid syntactic confusion, here is a comparison in JavaScript

  // Call this with foo(x, y)
  function foo (x, y) {
      return x*y;
  }

  // Call this with foo(x)(y)
  function foo (x) { return function (y) {
      return x*y;
  }}

The key thing to notice is that you can get from one form to the other with a straight text substitution. So restricting yourself to functions of one variable involves no loss of generality.

Going back to the lambda Calculus, you can do Boolean logic there as well. See http://safalra.com/science/lambda-calculus/boolean-logic/ for details. In fact I believe that the if construct in Haskell is just syntactic sugar around that. So it isn't that there is a decision made within the function, but rather that you call a function which turns out to be one of two different functions.

Ah, right, yes, that's true, I forgot about the Currying bit (I read up on it earlier, promptly forgot it).

I'm coming at this from a 'coders' perspective, not the mathematical side of it, so the code example is much appreciated, that makes it much easier to understand.

The function 'foo' returns a function that has already 'bound' 'x' to whatever value you put in, the 'scope' then allows you to fish out the right 'x' when you're in the inner function doing the multiplication.

So, does that mean that as far as the inner function is concerned 'x' is 'free' ?

So far when reading articles about the lambda calculus it seemed like the 'free' variables where somehow magically present in the scope of the function without a hint about where they came from.

I could easily be wrong, but here is my understanding. Consider this snippet of JavaScript:

  function foo (x) { return function (y) {
      return x*y;
  }}

  bar = foo(5);

Within bar, x is bound and y is free.

Does that make sense to you?

Ok, so now 'bar' contains a function where the 'x' is already bound to the '5', but the 'y' is still free because it has not yet been 'bound' to any parameter, is that what you mean ?

bar contains "function(y) { return 5*y; }"

The 'x' has been replaced by the '5' because of the function call. So 'binding' effectively pins down a function parameter and allows you to replace its instances in 'named' form with its value to reduce the expression ?

That is the way that I understand it. However you should be warned that I have never made a detailed study of the lambda calculus, and so might have basic misconceptions about it.

> Anything evaluating lambda expressions then has to deal with that or you'd have to expand the syntax of the calculus to contain a termination function which 'magically' decides that enough is enough.

This isn't so magic. I don't know all the details, but it has been proved that:

* If some expression can be reduced to normal form, this normal form is unique (modulo variable naming —alpha conversion).

* There is a systematic (mechanic) strategy which guarantee to reach normal form, if it exist at all : normal order reduction.

Normal order reduction reduces the outer-most redex in an expression (instead of the inner-most one when you do eager evaluation —call by name). This is why you don't need `if`.

A small example:

    true  = \t f. t
    false = \t f. f

    if = \b t f. b t f

    nt = something_that_doesn't_reduce_to_normal_form
    id = \x. x

Now, trying to reduce this expression (in normal order):

    if false nt id -- outer redex = if X X X
    false nt id    -- outer redex = false X X
    id             -- normal form = \x. x

Now, without using definitions (except for `nt`):

    (\b t f. b t f) (\t f. f) nt (\x. x)
    (\t f. f) nt (\x. x)
    (\x. x)

Finally, the outer-most thing may not be a redex. (but you can still reduce inner-redexes). This is the weak head normal form. For example:

    \x. ((\x. x) x) -- weak head normal form. Outer redex = (\x. x) X
    \x. x           -- plain normal form

You can decide whether weak head normal form is enough, or go to normal form.