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(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*' 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.

`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]`

`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]`

' from above.**(3)** - Reduct: the functions (after beta-reduction), such as '
`[2(3)]`

'

`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".

- 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)(`

(x) -> q(x))]~~lambda(y)~~[girl(y)]`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.