“Life, uh, finds a way.” —Ian Malcolm
All my sci-fi fantasies came true once I learned that there was a possible connection between DNA replication and lambda calculus. Although there was no Tyrannosaurus rex running after my tiny Toyota Corolla, everything I've learned about lambda calculus and recursion applied to make my fantasies of Jurassic Park come to life (at least in my head). Before we get ahead of ourselves, let us examine what lambda calculus is.
A Short Introduction to Lambda Calculus
Lambda Calculus was first introduced by mathematician and logician Alonzo Church. To be sure, Church has made major contributions to both mathematical logic and theoretical computer science; however, he is most well known for the lambda calculus and the Church-Turing thesis (Wiki). What lead Church to invent lambda calculus? Did he have a burning question that he needed to answer like mine with Jurassic Park? Yes, he did.
According to Professor Hutton, author of Programming in Haskell and professor of Computer Science at the University of Nottingham, Church was interested in the notion of a function from a computational perspective and his answer was lambda calculus. Lambda calculus is a computational model ( or a model of computation). Generally, it expresses how an output is computed given its input. Doing so requires use of variables, abstraction, and application. We'll cover those constructs under Lets Speak Lambda.
My professor once said that lambda calculus is known as the smallest and simplest possible programming language. At the time, I wasn't sure what he meant. However, after some research, I've found out why. "Any computable function can be evaluated in the context of λ-calculus and evaluating programs in the language consists of a single transformation rule: variable substitution." (Perforce). Unlike the Turing machine, lambda calculus only cares about the use of these transformation rules rather than the implementation.
Now that we've had a taste of lambda calculus, lets dive into its syntax.
Lets speak Lambda
Just like any language, lambda calculus has rules. Note that the code below is a function that adds 5 to some number k. If we were to translate the code to lambda calculus, we would have to make a few changes.
int plusFive (int k) {return k + 5}
plusFive(0);
We need to condense the code above and exclude the following (Kurz, Syntax of Lambda Calculus) :
There are no types. Meaning, no data types such as integers, doubles, or floats
No return statements (Given the program above, we don't need {return n + 1} )
No ';' or closing statements needed
Finally, 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 k.k+5
0
But it does not end there.
Now, we can write it in Lambda Calculus Notation:
(λk. k + 5) O
What is this saying?
λk. -> We have one input k
k + 5 ->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 + 5 = 5.
You may be wondering, what λ means by itself. It simply indicates the start of a function. To formalize our definition of lambda calculus expressed as function, observe the function below.
λx.x
Before the "." operator, λx, the x is the parameter of the function λ. The name of the function doesn't matter when it comes to lambda calculus. The "."operator that proceeds it and terminates the parameter(s) x. We would also view the "." operator as a divider between the parameters and the body of the program.
Before we tackle other lambda calculus problems, we must first ground 3 programming constructs.
3 Programming Constructs
Professor Kurz, Syntax of Lambda Calculus
We can examine these three construct in a practical example that we've already come across.
Recall our example:
(λk. k + 5) O
Variable: k
Abstraction: λk. k
Application: We apply our definition of k to our function k + 5
In this case, k = 0. Therefore, 0 + 5 = 5.
Since we've built our understanding of what lambda calculus is, how we transition from code to lambda, and what its 3 constructs entail, we can now now examine a coherent set of formalized rules. Remember when I said that lambda calculus has rules? Well here it is.
Wisc.edu, Lambda Calculus
In its most pure form, lambda calculus follows all rules above. Rule 2b and 2a apply 2 of our three constructs stated earlier: abstraction and application. The formal parameter in the case of 2b. is id, just like our x. M in this case is the body of the function. As for MN, it applies the function M to the argument N. However, what does 2a's rule mean or (M)? It simply means that the lambda expressions allow ( ) around anything. For instance, if we were to write the expression λx. λk. x + y, we wouldn't be required to encapsulate the expression with parenthesis.
To apply what we've learned, attempt the examples below.
Simple Examples
Example 1:
(λx. x + 5) 3
Example 2:
(λx. x + 4) 2
Example 3: Lets kick it up a notch with 2 applications.
(λx.x+4)((λy.y+1)2)
Short Summary and Hello Dinosaurs
To keep things short, lambda calculus consists of three things
Variables
Building Functions
Applying Functions
That's pretty much all there is to it.
As for dinosaurs, here's a recursive function in lambda calculus
λf.(λx f(xx))((λx. f(xx))
Notice that the structure of the expression above holds identical applications, (λx f(xx))((λx. f(xx)). What's the relevance? Human DNA has a double helix structure which self replicates. In turn, this may contain the key to DNA replication. Having a pure lambda calculus algorithm that conducts things recursively may be one step closer to Jurassic Park.
Next week's blog:
Must Reads
Tim's code stuff: https://tgdwyer.github.io/lambdacalculus/
References
Alexander Kurz: https://hackmd.io/@alexhkurz/S1D0yP8Bw
Perforce, JRbel: https://www.jrebel.com/blog/what-is-lambda-calculus
Tim's code stuff: https://tgdwyer.github.io/lambdacalculus/
Comments