Is Lambda Calculus a dense topic? To some it may be overwhelming. Today's blog will highlight key ideas stay afloat with Lambda Calculus.
The Beginnings of Lambda Calculus
Haskell's trademark logo is a lambda. It so happens that Haskell applies lambda calculus heavily. A simple coincidence? I think not. Indeed, Haskell features lambda expressions, pattern matching, lazy evaluation (as mentioned in Week 2's blog: We Love Lazy Languages), and more. To begin, we need to breakdown lambda calculus. Let's learn to float before we can swim.
A Little History and Importance
Professor Graham Hutton of Computer Science at the University of Nottingham and the author of Programming in Haskell gifted me with a life raft to lambda calculus. His cohesive summary of lambda calculus covers the fundamentals (For the full video, click here : https://www.youtube.com/watch?v=eis11j_iGMs ).
The Church-Turing Hypothesis
For Church, a function was a black box that you were not allowed to look inside. It takes some input x and y (we'll use the example below) and processes it in some way and then produces the sum x + y. Again, this machine is a black box - it is not important to understand how it works, and as a result, it, and its components, can take any form: real, imaginary, abstract, fixed etc.
Inputs: x and y (λx. λy.)
Output : x + y
How does this relate to Lambda Calculus? My thoughts exactly. What we compute in our Turing machine can also be computed using Lambda Calculus.
Lets translate Church's black box analogy to Lambda Calculus Notation:
λx. λy. x + y
To be sure, the transition from Church's black box and Lambda Calculus may appear straight forward but we can take another approach. Perhaps one that we're more familiar with, imperative languages.
The Transition from C to Lambda Calculus
Professor Alexander Kurz of Computer Science at Chapman University covers examples about the transition from the C language to Lambda Haskell notation and further examines the syntax of Lambda Calculus (Kurz, Lambda Calculus Syntax). His approach is quite insightful and a perfect beginning to this blog since we're still adjusting to functional programming. I'm going to breakdown his overview of the topic:
The code below is a function that adds 1 to some number n.
int plusone (int n) {return n + 1}
plusone(0);
To condense the code above, we're going to exclude the following from our code above:
There are no types
Meaning, no data types such as integers, doubles, or floats
2. There are no return statements.
Given the program above, we don't need n + 1
3. No ';' or closing statements needed
4. no ( )
Given these 4 guidelines, we can translate this to our own notation. In this case, we use the dot operator as a substitute for the { }
plusone n.n+1
0
From there, we can write it in Lambda Calculus Notation:
(λn. n + 1) O
What is this saying?
λn. -> We have one input n
n + 1 ->Then, we have the output be in terms of the input, which is n + 1
O -> Finally, we must substitute 0 for the input n
In this case, our final output would be 0 + 1 = 1.
Exercises To Get Us Started
Now lets apply what we learned and examine a few other examples:
Example 1
(λx. x + 1 ) 7
STEP 1: We substitute 7 for the input x
STEP 2: Then, apply x + 1 to be in terms of x.
STEP 3: We get 7 + 1 = 8.
Example 2
When I first attempted problems with the same construct, I've noticed that if the problem is expressed differently then I tend to retreat from that problem. To understand that what you learn in this blog is applicable to problems expressed differently, I'd like you try try this boolean Lambda Calculus problem.
(λx. x FALSE TRUE ) TRUE
STEP 1: replace x with TRUE and the λx. goes away as well. STEP 2: So, we have TRUE FALSE TRUE
STEP 3: If we applied boolean logic to TRUE FALSE TRUE then of course it would be FALSE.
We covered straight forward and simple examples above but it's not enough to say that we understand Lambda Calculus.
Concepts
Don't worry, we'll tackle interesting exercises of Lambda Calculus soon enough. When practicing lambda calculus, I found a few shortcuts that I'll share with you after I introduce these concepts:
1. Free and Bound Variables
2. Predefined constants
3. Function applications
4. Lambda expressions
In pure lambda calculus, there are no predefined constants. But I found that tying lambda calculus from a software engineering perspective made sense.
To best understand these concepts, it's best to start with examples:
(λf . (λx . (f (f x))))
-> Abstraction: λf . f (Abstraction is a function with 2 arguments)
-> "λ is the identifier of the argument of this function. The expression after the point (in this case a single x) is called the “body” of the definition" Rojas, A Tutorial to Lambda Calculus).
(λx.x)y
-> Function Application: Applying a function to an argument.
(λm.m)(λy.ym)
-> Bound variables: First, check from left to right where each λ bounds its variable.
-> In this example, λm bounds m. We can consider that m is in the body of the first expression.
-> On the right side, the y bounds to the second λ. Notice that the m in the second expression is independent. It's not bounds to any λ. Although at first it may be confusing because m is on the left side as well but it's independent of that as well.
-> m on the right hand side is free (Note: to avoid confusion in the future, we're going to use alpha conversion to rename variable like the free m variable.).
As mentioned before, I was able to better understand lambda calculus from a software engineering perspective by including a predefined constant. The example below illustrates how a predefined constant can be applied in the context of lambda calculus.
(((λf . (λx . (f (f x)))) sqr) 2)
= ((λx . (sqr (sqr x))) 2)
= (sqr (sqr 2))
= (sqr 4) = 16.
-> The predefined constant/function: sqr
-> sqr - can square an integer number. For example, (sqr 5) = 25
-> STEP 1: find the first argument and replace it with the first λ variable.
-> STEP 2: λf goes away and f is replaced by sqr.
-> STEP 3: find the next argument and replace it with the first λ variable.
-> STEP 4: replace x by 2
Are you confused with the parentheses?
1. Think of λf . as a function name and the variable after the '.' as part of the body .
For example:
λf . f x c
After the '.' all variable after the . are encapsulated with λf . However, as mentioned before, x and c are free variables.
(λf . (f x c))
Note that ABC = (AB) C is a helpful tip when coming across complex lambda bodies.
Given this shortcut, we have the following:
(λf . ((f x) c))
2. What is there is another lambda that follows λf . from our previous example?
λf.λx.f x c
We would apply what we learned from the previous example. Note, λx.'s '.' comes right before f, x, and c. Hence, we can apply the same rules.
λf.(λx.((f x) c))
We could include parentheses to wrap around the expression like so:
(λf.(λx.((f x) c)))
However, the parentheses can be dropped if the expression is unambiguous.
β-Reduction and α-conversion
Applying reduction operations is the most interesting part of lambda calculus. What the two operations entail is quite simple.
β-reduction
-> Replaces the bounds variable with an argument.
-> For example: (λf. f )2
-> f is replaced by 2 so the final answer is 2
α-conversion
-> Renames the bounds variable (as I said earlier, it prevents confusion).
-> For example: (λm.m)(λy.ym)
-> Replace the free variable 'm' on the right hand side with 'p'.
-> (λm.m)(λy.yp)
The descriptions for both are simple to understand. However, parsing correctly and performing the correct operation may be confusing at first. We're going to attempt some examples. I will provide step by step instructions to guide you. From experience, I found that tackling difficult lambda problems instead of simple ones helps in understanding the material better.
Example 1
Example 2
I hope the examples and descriptions were helpful to you. At first glance, lambda calculus can be difficult to understand. Sometimes we sink when the problem appears overwhelming. That's why completing problems like the above reenforces our understanding of the subject. It appears difficult but once the problem is broken down into steps, it doesn't appear as ferocious. You may find it easier to try other problems through your command prompt as a text file. It allows you to keep track of the parentheses, hence preventing misplacement. Don't forget to check out the "Must Reads" sections below, especially the practice problems.
Till next time fellow readers and keep floating with lambda calculus!
Next Week's Blog: Breaking the Enigma Code with Rewrite Rules
Must Reads
Raul Rojas, A Tutorial to Lambda Calculus
Practice Problems That You'll Find Helpful
Lambda Calculator To check work
References
Alexander Kurz, Lambda Calculus Syntax
Raul Rojas, A Tutorial to Lambda Calculus
Comments