Symbolic AI – Basic Lambda Calculus 1


This post will explain some of the basics of Lambda Calculus, mainly Alpha-Conversion and Beta-Reduction. We’ll also see a quick example of a simple sentence.

This post is being written with me being slightly ill… so some bits may make no sense whatsoever – sorry 😦

Functions

Let’s see an example of a function in Lambda Calculus, this one should do us nicely 🙂

  • lambda(x) [2x]

‘2x’ here is the main function, mapping any given integer to another. So if x=0 then the function returns 0; x=3 and we get 6. The lambda(x) in this states that ‘x’ is a bound variable.

 

Applying to Functions

In Lambda Calculus we can apply variables, integers or even other functions to another function. Let’s use the same example as above, but this time we apply this function onto the integer 3:

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

When we see something like this, you must remember that “lambda(x) [2x]” is being applied to “(3)”.

Once we have written this down, we then look at the lambdas. Here we only have one lambda, so this makes things a lot simpler! So what we do strip off the “lambda(x)”, and then replace any occurrences of ‘x’ with the number ‘3’, so that we have:

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

 

Alpha-Conversion and Beta-Reduction

Now you probably haven’t even realised it; but we’ve already done some Beta-Reduction :D, but firstly, i need to explain what Alpha-Reduction is!

 

Alpha-Conversion

Alpha-Conversion is the renaming of bound variables.

Now for a bigger example – well, a little bigger 🙂 now lets say that we want to apply the function ‘2x’ to a function ‘3+2x’. Firstly we would write:

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

Now we have a problem. Both functions contain a bound variable ‘x’ – dun, dun, duuun! So what we need to do is convert any bound variables in the second function, that are also bound in the first to something else, such as:

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

Aaah, that’s much better, and that’s it, THAT is Alpha-Conversion 🙂

    Normally you would replace x with x-bar. written x’, or x with a line on top of it.

In case you are wondering, yes, that above calculus will work, you just have to think a little commutatively 😉

 

Beta-Reduction

Now, this part we’ve already done! Beta-Reduction is the action of applying lambda functions to their arguments:

  • lambda(x) [ F(x) ] (A)  ==>  F(A)

Or from the example above:

  • lambda(x) [2x] (3)  ==>  [2(3)]

Redex and Reduct

Here, the expressions on the left hand side, that is “lambda(x) [ F(x) ] (A)” or “lambda(x) [2x] (3)” are all called redex expressions.

The expressions on the right hand side, after Beta-Reduction are all called reduct expressions. So F(A) and [2(3)].

 

Property of being a Property – Lambda Terms

Now, that may sound like complete gibberish to some people, but it should make some sense. Don’t worry too much about not getting it, not even i fully understand it 😉

Now, let’s take on some proper examples:

  • lambda(p) [p(mary)]

This is “the property of being a property possessed by mary”. Here, we have no clue as to what the ‘p’ represents as a function, it could be anything like coughed() or laughed(), it could be literally anything! So until we know, we call it a property. Now, mary is inside of this property, so mary must possess this property, so this is why we call it “the property of being a property possessed by mary”.

Another example could be “every girl”:

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

Now this one looks slightly daunting, but it’s really very nice looking and simple to understand 🙂

Here we state that every ‘x’ is a girl. That part is easy. but now lets move onto the p(x). does this look any familiar? Remember, all x’s are girl. And we have no clue as to what ‘p’ is. So we define this lambda-term as “the property of being a property possessed by every girl”.

 

Basic Lambda Calculus 2 coming in a minute 🙂

Advertisements

About Badgerati
Computer Scientist, Games Developer, and DevOps Engineer. Fantasy and Sci-fi book lover, also founder of Cadaeic Studios.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: