Computer science is definitely a huge and very important branch of mathematics. There is an immense amount of concepts, problems and ideas that have revolutionized the world in different aspects, even making an impact in our daily lives throughout all the years this science has been developed.
Sometimes, it is very easy to forget that computers and programming languages have their origin in mathematical concepts, ideas that were developed by mathematicians almost a hundred years ago. With the time those ideas were developed to a point where they took form into something tangible such as computers, reaching a point where nowadays it is almost impossible to imagine our lives without a laptop, a cell phone, a video game console or a tablet.
This article is a brief introduction to the origins of functional programming and the ideas behind this paradigm, starting by the person who came up with the cornerstone concept, then introducing the reader to the circumstances which gave birth to these ideas, after that there is a brief introduction to λ-calculus (Lambda calculus) and how to use it to do basic arithmetic operations, finally the author will share a thought with the reader.
Alonzo Church
Alonzo Church was a mathematician from the United States of America. He was born in Washington D.C. in 1903. He was a computer pioneer who contributed to the foundations of computer science. A contemporary with Alan Turing, who is considered as the father of modern computing, Turing has had an important influence in the modern society, being brought in films such as The Imitation Game in 2014 or Codebreaker in 2013 there are also novels where he appears as an important character such as Cryptonomicon by Neal Stephenson.
Church earned a Ph.D. from Princeton University in 1927, when he was only 24 years old. He dedicated his life to teaching and it was a very influential teacher, some of his students made huge contributions to the foundations of computer science such as the already mentioned Alan Turing, Stephen C. Kleene, Dana Scott, John Barkley Rosser, among others.
Church started his academic career in Princeton as an Assistant Professor (1929-39) after that he became an Associate Professor (1939-47) and finally a Professor (1947-67). Church left Princeton in 1967 and moved to University of California, Los Angeles (UCLA). He retired from teaching in the year of 1990, at 87 years old. He spent 63 years of his life teaching and continued his research until he died at the age of 92, in 1995.
A little bit about the personality of Alonzo Church:
“Alonzo Church had the polite manners of a gentleman who had grown up in Virginia. He was never known to be rude, even with people with whom he had strong disagreements. A deeply religious person, he was a lifelong member of the Presbyterian church.
In his habits he was careful and deliberate. The students in his classes would discover this on the first day, when they saw how he would erase a blackboard. The material he wrote out on paper (he did not type) was often done in several colors of ink and always done in his distinctive unslanted hand-writing. He was a master at using white-out fluid to eliminate imperfections. Finally, an important piece of writing could be made permanent by coating it with a thin layer of Duco cement. (Duco was the one brand of household cement that did not shrink the paper.).
Church enjoyed reading science fiction magazines. He preferred a nocturnal schedule, working late at night, when it was quiet and he would not be disturbed.
He never drove a car. But he would walk substantial distances, in varying weather and at all hours. A student crossing the campus at night would see a well-dressed portly gentleman with white hair, carrying a briefcase and humming softly to himself. ”
During the 1930’s Church ideated a concept named as λ-calculus which nowadays still resonates in modern computer languages. It was in “An unsolvable problem of elementary number theory”, a paper published in the year of 1936 by Church, where he focuses more in the computing aspect about this mathematical model.
What is this λ-calculus and what did Alonzo Church conceive a concept like that for? Well, let’s talk about the decision problem.
The decision problem (Entscheidungsproblem)
Originally thought by Gottfried Leibniz with the purpose of basically mechanizing reason. This problem was later raised by David Hilbert and Wilhelm Ackermann in 1928 from their text Principles of Mathematical Logic (Grundzüge der theoretischen Logik).
This problem basically asks for an effective procedure which, given a set of axioms and a mathematical proposition, can decide whether it is or is not provable from the axioms. But before elaborating more on the topic, it is necessary to talk about David Hilbert.
David Hilbert (1862-1943) was a German mathematician, during the 19th and early 20th centuries, he was a very influential figure in the science field and made a lot of contributions to different areas of mathematics. It was in August of 1900 in Paris, France when the Second International Congress of Mathematicians was celebrated. During this congress Hilbert presented 23 problems which he considered to be a look into the future of mathematics for the coming centuries:
“Who of us not be glad to lift the veil behind which the future lies hidden; to cast a glance at the next advances of our science and at the secrets of its development during future centuries?”
Among the 23 presented problems, there were 3 of them, the problem numbered 1, 2 and 10 which concern mathematical logic, those problems were the ones which gave birth to the Entscheidungsproblem. What Hilbert wanted was a process with a finite number of operations. Basically, he asked for an algorithm. At the time the word algorithm was not used as we use it nowadays, it became common in the 60’s in literature about computers.
Having an algorithm such as the one described by the problem implies that there is no such thing as an unsolvable problem and Hilbert firmly believed in that:
“However unapproachable these problems may seem to us and however helpless we stand before them, we have, nevertheless, the firm conviction that their solution must follow by a finite number of purely logical processes… This conviction of the solvability of every mathematical problem is a powerful incentive to the worker. We hear within us the perpetual call: There is the problem. Seek its solution. You can find it by pure reason, for in mathematics there is no we shall not know.”
The idea of having an algorithm able to solve all the problems sounds great. However, it was Alonzo Church in his paper previously mentioned from 1936 who demonstrated that the Entscheidungsproblem was unsolvable, by using his λ-calculus and giving an argument by contradiction. A few months later, Alan Turing would independently reach the same result by ideating the concept of the Turing machine and he would prove that λ-calculus is actually equivalent to the Turing machine. This way the Church-Turing thesis was born.
This means that unfortunately not all the problems have solutions and λ-calculus and Turing machines were concepts ideated to be used as tools to demonstrate this formally.
λ-calculus
λ-calculus is a mathematical formalism, considered to be the smallest universal programming language of the world. It was conceived as a system for capturing the idea of effective calculability. According to Turing’s definition:
“A function is said to be “effectively calculable” if its values can be found by some purely mechanical process. We may take this statement literally, understanding by a purely mechanical process one which could be carried out by a machine”
λ-calculus is universal in the sense that any computable function can be expressed and evaluated using it. As it was mentioned before, is equivalent to Turing machines.
“The λ calculus emphasizes the use of transformation rules and does not care about the actual machine implementing them. It is an approach more related to software than to hardware.”
λ-calculus and Turing machines are not the only systems to express effective calculability, between the 1920’s and 1930’s there were more related systems proposed which were computationally equivalent. This period of time was very exciting for theoretical computer science and there were great mathematicians such as Kurt Gödel and Emil Post among others, all of them were trying to understand the notion of computation:
- λ-calculus – Alonzo Church, Stephen C. Kleene
- Turing machines – Alan Turing
- Post systems – Emil Post
- μ-recursive functions – Kurt Gödel, Jacques Herbrand
- Combinatory logic – Moses Schönfinkel, Haskell B. Curry
All of the previous systems embody the idea of effective calculability or computation in one way or another. They work on several types of data, for example: Turing machines manipulate strings over a finite alphabet, μ-recursive functions manipulate the natural numbers, the λ-calculus manipulates λ-terms, and combinatory logic manipulates terms built from combinator symbols.
But let us focus on λ-calculus…
The central concept in λ-calculus is the “expression”:
<expression> := <name> | <function> | <application> <function> := λ <name>.<expression> <application> := <expression><expression>
- A name is also called a variable.
- The only keywords are the . and the λ.
- The name after the λ symbol is used as the identifier of the argument for the function.
- The . separates the function argument and body, so the expression after the . is the body.
- An expression can be surrounded with parenthesis for clarity.
Expressions associates from the left, for example:
E1E2E3…En
It is evaluated as below:
(…((E1E2)E3)…En)
A function can be defined as:
λx.x
It is possible to apply functions to expressions, that is called application:
(λx.x)y
The expression λx.x represents the Identity function (Identity function is a function which always returns the same value used as argument) which is being applied to y. Function applications are evaluated by substituting the value of the argument x (in this case y) in the body of the function definition. In the next example the identity function is applied to y so the result will be y, given the definition of the identity function:
(λx.x)y = [y/x]x = y
The notation [y/x] indicates that all the occurrences of x will be substituted by y in the expression to the right. Notice how the λx term is removed from the expression after the substitution of x has been performed.
Names are just placeholders, do not have any meaning and can be replaced by a different name in order to rearrange the arguments of the function when this is evaluated:
(λx.x) ≡ (λy.y) ≡ (λz.z)
The symbol ≡ indicates in the case of the next expression E1 ≡ E2 that E1 is a synonym of E2.
In λ-calculus a variable is “bound” since its occurrence in the body of the definition is preceded by a λ. In the opposite case is called “free”:
(λx.xy)
For the previous example x is bound and y is free. In the next example:
(λx.x)(λy.yx)
The x in the body of the first expression from the left is bound to the first λ, The y in the second expression is bound to the second λ and the x is free. The x from the second expression is completely independent of the x in the first expression.
Numbers in λ-calculus also known as Church numerals are represented by using the next notation:
0 ≡ λs.(λz.z) ≡ λsz.z 1 ≡ λsz.s(z) ≡ λs.λz.s(z) 2 ≡ λsz.s(s(z)) ≡ λs.λz.s(s(z)) 3 ≡ λsz.s(s(s(z))) ≡ λs.λz.s(s(s(z))) 4 ≡ λsz.s(s(s(s(z)))) ≡ λs.λz.s(s(s(s(z)))) … S ≡ λw.λy.λx.y(wyx) ≡ λwyx.y(wyx)
The S represents the successor function and what it does is to increment a number by one in such a way that S0 = 1, S1 = 2, S2 = 3 and so on. For example:
S0 ≡ (λw.λy.λx.y(wyx))(λs.λz.z) = [(λs.λz.z)/w](λy.λx.y(wyx)) = λy.λx.y((λs.λz.z)yx) = λy.λx.y([y/s]((λz.z)x)) = λy.λx.y((λz.z)x) = λy.λx.y(x) ≡ 1
Basically, the successor function (λw.λy.λx.y(wyx)) is being applied to number zero (λs.λz.z), and the result as shown above is the number 1 (λy.λx.y(x)). Also in the example there are two substitutions, first the zero numeral will take the place of the w term in the successor function, after that, substituting the s by the y will do the job. Notice that when doing a substitution the λ-term which is bound to the variable being substituted is removed.
Addition can be expressed in terms of S, for example: 2 + 3 = 2S3, this means to apply two times the successor function on the number 3. Thus:
2S3 ≡ (λsz.s(sz)))(λwyx.y(wyx))(λsz.s(s(sz)))
Let’s rename the last expression just for clarity:
(λsz.s(s(sz))) ≡ (λab.a(a(ab)))
Going back to the former expression, it is possible to express:
2S3 ≡ S(S3) = (λwyx.y(wyx))(λwyx.y(wyx))(λab.a(a(ab))) = (λwyx.y(wyx))([(λab.a(a(ab)))/w](λyx.y(wyx))) = (λwyx.y(wyx))(λyx.y((λab.a(a(ab)))yx)) = (λwyx.y(wyx))(λyx.y(([y/a](λb.a(a(ab))))x)) = (λwyx.y(wyx))(λyx.y((λb.y(y(yb)))x)) = (λwyx.y(wyx))(λyx.y([x/b](y(y(yb))))) = ((λwyx.y(wyx))(λyx.y(y(y(yx)))) ≡ S4
Applying the successor function again on the number 4, the result will be:
= [(λab.a(a(a(ab))))/w](λy.y(wyx)) = λyx.y(λab.a(a(a(ab))))yx = λyx.y(([y/a](λb.a(a(a(ab)))))x) = λyx.y([x/b](y(y(y(yb))))) = λyx.y(y(y(y(yx)))) ≡ 5
Multiplication can be implemented by using the expression (λxyz.x(yz)), so for example multiplying two times two (2 · 2) would produce the below computation:
2 · 2 ≡ (λxyz.x(yz))(2)(2) = (λxyz.x(yz))(λsz.s(sz))(λsz.s(sz)) = ([(λsz.s(sz))/x](λyz.x(yz)))(λsz.s(sz)) = (λyz.((λsz.s(sz))yz))(λsz.s(sz)) = (λyz.([y/s](λz.s(sz))z))(λsz.s(sz)) = (λyz.((λz.y(yz))z))(λsz.s(sz))
It is necessary to rename the variables inside the expression ((λz.y(yz))z), by inspecting the expression it is possible to notice that the last z is a free variable since it is outside of the inner expression (λz.y(yz)) so by renaming the bound variables, the expression will be rewritten as:
((λz.y(yz))z) ≡ ((λa.y(ya))z)
This way we can continue developing the former expression:
= (λyz.((λa.y(ya))z))(λsz.s(sz)) = (λyz.([z/a](y(ya))))(λsz.s(sz)) = (λyz.y(yz))(λsz.s(sz))
Again, since it is needed to substitute the second expression (λsz.s(sz)) into the first one (λyz.y(yz)), it is necessary to rename the z variable in the second expression to avoid confusion when substituting, thus:
(λsz.s(sz)) ≡ (λsb.s(sb))
Continuing the computation:
= (λyz.y(yz))(λsb.s(sb)) = [(λsb.s(sb))/y](λz.y(yz)) = λz.(λsb.s(sb))((λsb.s(sb))z) ≡ λz.(λsz.s(sz))((λsz.s(sz))z) ≡ λz.2(2z)
By analyzing the previous expression, it is possible to observe that the values of the variables x and y have been replaced by the initial values passed to the multiplication function.
2 · 2 ≡ (λxyz.x(yz))(2)(2) ≡ λz.2(2z) ≡ 4
The final result must be a 4, so continue developing the previous expression:
= λz.2((λsz.s(sz))z)
Renaming (λsz.s(sz)) to ((λsa.s(sa)) to avoid confusion:
= λz.2((λsa.s(sa))z) = λz.2([z/s](λa.s(sa))) = λz.2(λa.z(za)) = λz.((λsz.s(sz))(λa.z(za)))
Renaming ((λsz.s(sz)) to ((λsb.s(sb)):
= λz.((λsb.s(sb))(λa.z(za))) = λz.([(λa.z(za))/s](λb.s(sb))) = λz.(λb.(λa.z(za))((λa.z(za))b)) = λz.(λb.(λa.z(za))([b/a](z(za)))) = λz.(λb.(λa.z(za))(z(zb))) = λz.λb.(λa.z(za))(z(zb)) = λz.λb.([(z(zb))/a](z(za))) = λz.λb.z(z(z(zb))) ≡ λs.λz.s(s(s(s(z)))) = 4
In λ-calculus, it is also possible to express “true” and “false” values, perform logical operations, equalities, inequalities and also recursion, is a complete programming language. The scope of this text is limited to the very basics of arithmetic, in order to show in a simple way how the λ-calculus works.
Conclusion and final thoughts
Functional programming is a computer paradigm which is based on function calls as the primary programming construct, there exists representations for numbers as it was shown previously in this text and also for data structures to manipulate information, it is even possible to treat functions as values. In functional languages, the functions are arranged as chains. Thus, each function receives values from and passes new values back to the calling function. The next chunk of Javascript code is a function which calculates the successor of a Church numeral (another function) and it depicts the previous explanation on calling functions:
function successor(n) { return function(f) { return function(x) { return f(n(f)(x)); } } }
Functional languages are a little bit different than imperative or procedural languages, while in procedural languages we use assignments to change variables in whose values the execution of the program depends on (which leads to unintended side effects), functional style is more encouraged to limit the scope of variables in order to eliminate side effects.
The above functional programming explanation describes completely the essence of λ-calculus and that is because λ-calculus is the foundational concept behind the functional programming which was ideated by Alonzo Church in the 30’s to define the concept of computation in order to give an answer to the decision problem.
To finalize this text, there is this anecdote of Alonzo Church that is pretty interesting:
“In 1983 or 1984, when Alonzo Church was about 80 years old, he was invited to speak at the Center for the Study of Language and Information at Stanford University, and was taken on a little tour featuring CSLI’s Xerox Dandelion computers. These computers were running LISP, a programming language developed by John McCarthy. Church was told how LISP was based on the lambda calculus that Church had invented some 50 years earlier.
Church confessed that he didn’t know anything about computers, but that he once had a student who did. By that time, of course, everyone knew who Alan Turing was.”
λ-calculus is a huge contribution to computer science. In the end, it seems that Alonzo Church could not understand the reach of how huge this idea impacted on the world. It has been almost 90 years since the λ-calculus was conceived. Still to this date new functional languages continue to be developed and huge systems are built upon them to satisfy the needs of society and it seems it will continue being like that for the next years to come.
By – Jesús Serrato, Software Engineer, DigitalOnUs
References
An Introduction to Functional Programming Through Lambda Calculus
G.J.Michaelson
Addison-Wesley, 1988, ISBN 0-201-17812-5
An Unsolvable Problem of Elementary Number Theory
Alonzo Church
American Journal of Mathematics, Vol. 58, No. 2. (Apr., 1936), pp. 345-363.
Systems of Logic Based on Ordinals
Proceedings of the London Mathematical Society, Volume s2-45, Issue 1, 1939, Pages 161–228
Alan M. Turing
A Tutorial Introduction to the Lambda Calculus
Raúl Rojas
FU Berlin, WS-97/98
On Computable Numbers, with an Application to the Entscheidungsproblem
Proceedings of the London Mathematical Society, 42, pp.230–265.
1937
Automata and Computability
Springer-Verlag, 1997
D. Kozen
Church’s undecidability result
Alan Turing Birth Centennial Talk at IIT Bombay, Mumbai, April 21, 2011
Joachim Breitner
The Annotated Turing
Wiley Publishing Inc., 2008, ISBN 978-0-470-22905-7
Charles Petzold
Introduction Alonzo Church: Life and Work
http://www.math.ucla.edu/~hbe/church.pdf, September 2012
Introduction to Lambda Calculus
Nieuw archief voor wisenkunde, Revised edition December 1998, March 2000
Henk Barendregt, ErikBarendsen
Proof in Alonzo Church’s and Alan Turing’s Mathematical Logic: Undecidability of First Order Logic
Dissertation.com, Boca Raton, Florida USA, 2012, ISBN-10: 1-61233-951-4
Jonathan Okeke Chimakonam