In the 1930s, a mathematician called Alonzo Church, introduced a concept that would be trivial to the development of Computer Science. This concept is the λ-calculus. Matter of fact, λ-calculus itself is the smallest programming language, it can easily represent any Turing Machine. The λ-calculus is made up of a single transformation rule and a single function definition scheme. Functional languages nowadays are based on lambda-calculus, languages such as Haskell, Miranda, Lisp and others.
In order to understand λ-expressions, we must recall what a function is. A function is a relation between a set of possible inputs and possible outputs. To exemplify, imagine you have a washing machine, when you input dirt clothes there (it would be your x variable) it returns clean clothes as outputs (y variable). As you can observe, there is a clear relationship between the set of possible inputs (in this case the dirt clothes) and the set of possible outputs (clean clothes, y). Furthermore, let's suppose the washing machine is called f, if we represented the washing machine as a mathematical function, we would use the following denotation $$f(x) = ... $$ That means, the function $f$, will receive the variable x and manipulate it inside the body to output y. So, let's suppose we have a input x and we want to know what its double will be; we can thus express this as the function f(x) = 2x. Remember x can be any number (e.g., if x is two, f(x) = 4),
Now, let's talk about the λ-expressions, they have three main components, expressions, variables and abstractions. The expression is basically the superset of all those things. The abstraction is a function, a term that has a head and a body, separated by a dot (.). The variables are simply names for potential inputs to functions (e.g, x). Formally, they can be expressed as
expression := {name} | <abstraction> | <application>,
<abstraction> := λ<name>.<expression>,
<application> := <expression><expression>.
A simple λ-function can be written as $$\lambda x.x$$ Please observe that, following the definition of abstraction, the function has a head and a body. The head consists of the body of declaration of the variables, the body is another expression. Perhaps you noticed a strange term on the definitions, the term application. An application is the act of applying a λ function to an argument.
The λ-expression I demonstrated above is a $\alpha$-equivalence. What does that mean? Alpha equivalence is all the expressions that, shows identity (e.g., λx.x , λg.g ). One example of a expression that wouldn't be Alpha equivalent is λx.y, because x and y aren't identicals (the expression would be true in case they were identical, i.e., x = y).
We have two main types of variables, the free variables and the bound variables. Free variables are variables that are not declared in the head (in other words, variables that don't come preceded by a λ symbol). For example, in the expression $$\lambda a.ab,$$ we have two types of variables, the bound variable, which is $a$, because it's bounded to the head of the expression. Meanwhile, $b$ is free, which means it is not bound to the head of the expression, it can act freely.
We can reduce λ-expressions using functions. This is called β-reduction (note: it can be reduced not only with functions). An example of beta-reduction is $$(λx.x) ((λa.λb.a b) (λy.y) (λz.z))\newline ->β (λx.x) ((λb.(λy.y) b) (λz.z))\newline ->β (λx.x) ((λy.y) (λz.z))\newline ->β (λy.y) (λz.z)\newline ->β (λz.z)$$ So, we applied another expression in order to reduce the large λ-expression we had into a simple $\alpha$-equivalence. In order terms, β-reduction is when we apply a eliminator in order to reduce a big λ-expression to the result of a simpler expression.
Since lambda-calculus is a programming language, it should be able to do basic arithmetic correctly, such as 1 + 1. So, let's see how arithmetic works in λ-calculus. We can easily define numbers in lambda calculus, 0 can be defined as $$\lambda s.(\lambda x.x).$$
Which can be rewritten as
$$\lambda sz.z.$$
Here, s will be evaluated first, then it will be time for x. This expression is commonly regarded as succ(0)
, and it is the successor function. We can define other numbers as
$$1 \equiv λsx.s(x)\newline$$
$$2 \equiv λsx.s(s(x))\newline$$
$$3 \equiv λsx.s(s(s(x)))\newline$$
and the list goes on...
We can define addition by $$\lambda m.\lambda n.\lambda s.\lambda z.ms(nsz),$$ this is simply the successor function but instead of applied to zero, applied to (nsz).
We can simply define multiplication as $$(\lambda xyz.x(yz)).$$ Let's use as example, 2 * 2, $$(\lambda xyz.x(yz))22.$$ It can be reduced to $$(\lambda z.2(2z))$$
For the same reason stated on the topic above, we can also define true and false in λ-calculus. They can be defined as follow: $$T ≡ \lambda xy.x\newline$$ $$F ≡ \lambda xy.y$$ If you read and understood this paper, you should be able to understand the logic behind the expressions. Otherwise, please read the paper more carefully or contact me for help (contact info at the end).
λ-calculus is a really powerful programming language, since it's really powerful and can be used for literally anything. It was a revolution for the world of computer science, and for the world of science in general. As Leibniz once stated as an ideal, "Create a ‘universal language’ in which all possible problems can be stated.". We had λ-calculus as the answer. Of course, this paper was merely introductory, and it was meant for teaching the basics of λ-calculus and unveil a interest of the reader on the topic; with the objective of making him research more about it, and effectively use λ-calculus to solve problems. I strongly encourage you readers to research more about λ-calculus, functional programming and other related-topics. If you have any doubts, critics or found any errors in this paper, please don't be afraid to tell me, my contact e-mail is [email protected].