Symbolic AI – Basic Lambda Calculus 2

This is the second part to the Basic Lambda Calculus 1. In this we’ll go through a proper example.

Every Girl

Now, if you read Basic Lambda Calculus 1, then you should remember at the end i gave the example of “every girl”. But, how exactly was the lambda meaning computed?

In order to do this, we need 2 things.

1. The meaning of ‘every’
2. The meaning of ‘girl’

The meaning of girl should be fairly obvious. it is just:

• lambda(x) [girl(x)]

That is, the property of being a girl. Just a quite diversion. Since we know what the function is, then we don’t need to call it a ‘property’ anymore.

Next is the meaning of every. This one is a little trickier, however, if you look back at Basic Lambda Calculus 1, then you should be able to see the meaning of every? No? Well it’s:

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

Now you’re looking scared :D Now we have two lambda’s in one expression! But don’t worry, all will make sense in due time ;)

 

Now, normally at about this time you would draw a tree. However, this example is so small i sadly don’t see the point. But don’t threat! We will see tree’s soon :)

Now. look at the sentence, we have “every girl”. What does this tell you? Well what it should tell you is that we need to apply the meaning of ‘every’ to the meaning of ‘girl’:

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

This is looking very big and horrifying isn’t it? But it’ll be alright. Now, take a look at that calculus, and tell me; do you spot anything obvious that we need to do? That’s right, both meanings contain the bounded variable ‘x’, so we need to use Alpha-Conversion on the meaning of girl. let’s convert ‘x’ into ‘y’ :)

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

Aah, now that is much better! Now we can proceed with Beta-Reduction.

In order to make this work, what we need to do is strip off the first lambda term in the meaning of ‘every’. This first lambda term is ‘lambda(p)’, and not forgetting, we then need 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))]

What we have done here is, as stated, stripped off the ‘lambda(p)’. And then we have literally replaced every ‘p’ with ‘(lambda(y) [girl(y)])’. Take a look at the expression we just derived; notice anything? We have another redex expression that we can use Beta-Reduction on! If you have noticed it, it is: “(lambda(y) [girl(y)])(x)”

This time, instead of stripping off the “lambda(q)”, we need to strip off the “lambda(y)”. This is because lambda(q) is not being applied to the variable (x). Once we strip off the lambda(y), we then replace all ‘y’ with ‘x’:

• lambda(q) [forall(x) ( [girl(x)] –> q(x))]

And there we have it! Since there are no more redex expressions, we have derived the meaning for “every girl”, and if we pull in the meaning from Basic Lambda Calculus 1:

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

You can see we have the correct meaning :)

Note: it doesn’t matter that one has lambda(q) and the other lambda(p), they are, after all, only variables; and can be called anything. heck, i could use lambda(supercalafragli…. you get the point? :)