Basics of Lambda Calculus


28 Mar

Lambda Calculus is a formal system for expressing computation by way of variable binding (Alpha-Conversion) and substitution (Beta-Reduction). It is a particularly useful system in Artificial Intelligence when trying to write a program that can parse sentences - such as "Every girl laughed".

Lambda Functions Before we do anything, it's probably best to first see what a function looks like in Lambda Calculus - partly because Lambda Calculus is built on functions! Therefore here's our first example:
  • lambda(x)[2x]

The function of interest here is '2x'. Go back to your Maths classes for a moment, and remember what f(x)=2x is trying to do. That's right, it maps any given integer 'x' to another multiplied by 2. Therefore, if x=0, then the function returns 0. If x=3 then we get 6.

the lambda(x) states that 'x' is a bound variable, think of it as when you write f(x); you are decalring 'x' as a bound variable.

Applying to Functions In Lambda Calculus we can apply variables, integers or even other functions to another function. So, what exactly does this 'applying' mean? Well, let's use the example function from above, but this time we'll apply this function onto the integer, 3:
  • lambda(x)[2x](3)

The first thing to do here is take note of the lambda()'s. Here, we only have to deal with one, so it's far simpler. What we do, is we first strip off the lambda(x), and then proceed to replace any occurrences of 'x' with the integer, 3:

  • lambda(x)[2x](3)
  • lambda(x)[2x](3)
  • [2(3)]
  • 6

That's it! Simple really, eh? And we definitely know we got the right answer, seeing as 2*3=6, and we got the answer 6.

Alpha-Conversion This is the renaming of bound variables. In order to demonstrate this, we shall need a bigger example! In this example, we shall take the previous function once again however, this time we shall apply it not to a variable, but to another function; namely 3+2x:
  • lambda(x)[2x](lambda(x)[3+2x])

Oh, now then, we have a problem. Can you see what it is? Both of our functions contain a bound variable called 'x'. What we need to do therefore, is convert any bound variables in the second function that are also in the first, to something else:

  • lambda(x)[2x](lambda(y)[3+2y])

That's it. That is alpha-conversion. In case you're wondering, the calculus above will simplify down to: lambda(y)[6+4y]

Beta-Reduction We have already done some beta-reducing as we've been going along, as it is simply the action of applying lambda functions to their respective arguments.
  • lambda(x)[2x](3)
  • lambda(x)[2x](3)
  • [2(3)]

Other useful terms to note are Redex and Reduct:

  • Redex: expressions that have arguments, such as 'lambda(x)[2x](3)' from above.
  • Reduct: the functions (after beta-reduction), such as '[2(3)]'

Property of being a Property Confused? Excellent! Now it's time for some proper examples using sentence structure.
  • lambda(p)[p(Mary)]

This is the "property of being a property possessed by Mary". We also see something new here as well: 'p' is now being used as a function and not a variable. Yes, this is possible. In general, whenever we have an unknown in Lambda Calculus, we will place a 'lambda(-)' to state this fact.

Furthermore, because we don't know what 'p' is - as it could be anything like 'coughed()' or 'laughed()' - then we call 'p' a property. Seeing as 'Mary' is inside of this property, then it stands to reason that Mary must possess this property. That's why we call it 'the property of being a property possessed by Mary'.

Another example is 'every girl':

  • lambda(p)[forall(x)(girl(x) -> p(x))]

Here we are stating that every 'x' is a girl. That's the easy part, but now let's move onto the p(x). This is very similar as to what we had above with p(Mary), except this time, we have a variable that represents 'every girl'. Therefore, the logic is still the same, meaning we have: "the property of being a property possessed by every girl".

How to derive 'every girl'? Good question, how do we derive 'every girl' into Lambda Calculus? In order for this to happen, we need two things, namely:
  • The lambda meaning of 'every'.
  • The lambda meaning of 'girl'.

The meaning of girl should be fairly obvious, given what I gave above:

  • lambda(x)[girl(x)]

So this is "the property of being a girl", and not "the property of being a pr--" because we know what the function is this time around: 'girl()'.

Next up is the definition of 'every', and this a little more tricky and quite frankly daunting to look at! In general, 'every' is defined as:

  • lambda(p)[lambda(q)[forall(x)(p(x) -> q(x))]]

This isn't all too bad, it's basically just saying that all 'x' belongs to function 'p' and does function 'q'. Therefore, we could have 'every x coughed' or 'every x is a girl who coughed', both of which repectively look like:

  • forall(x)(coughed(x))
  • forall(x)(girl(x) -> coughed(x))

So, proceeding forward. We now need to apply the meaning of 'every' onto the meaning of 'girl':

  • lambda(p)[lambda(q)[forall(x)(p(x) -> q(x))]](lambda(x)[girl(x)])

Now this is starting to look daunting, yeah? But it's all right. First things first, take a look at the calculus above and tell me if you spot anything obvious that we need to do? You may have noticed that both meanings contain the variable, x. Therefore, we need to apply alpha-conversion onto the meaning of 'girl'. Let's convert 'x' into 'y' shall we:

  • lambda(p)[lambda(q)[forall(x)(p(x) -> q(x))]](lambda(y)[girl(y)])

With that crisis over, we're now free to start some beta-reducing! To make this work, we first have to strip of the lambda(p) from the meaning of 'every'. With that, we then have to literally replace every 'p' with the meaning for 'girl':

  • lambda(p)[lambda(q)[forall(x)(p(x) -> q(x))]](lambda(y)[girl(y)])
  • lambda(q)[forall(x)(lambda(y)[girl(y)](x) -> q(x))]

There we go. Now then, take a look at the expression we have just derived. Notice anything? We can apply another beta-reducing onto the redex expression: lambda(y)[girl(y)](x)

  • lambda(q)[forall(x)(lambda(y)[girl(y)](x) -> q(x))]
  • lambda(q)[forall(x)(girl(x) -> q(x))]

That's it! Since there are no more redex expressions, this can only mean we have - hopefully - derived the meaning of 'every girl' successfully! If we look above to check, then you'll see that our deriviation is the same as the example used in the "Property" section.

Share this:


  Allowed tags: <a> <b> <strong> <i> <em> <del> [code] [com]