COMP2K
Lambda Calculus
Laboratory
Shakes Chandra
4-17-2023
Instructions
Recommended you complete this part by the end of Week 9. You
should demo this lab in your Week 10 practical session.
COMP2048 Theory of Computation S. S. Chandra
1
[You must demonstrate it to the instructor in one of your practical sessions BEFORE the due date in
order to be awarded marks. Please check the ECP for the correct due date. Note that sections are
‘complete’ and marks are awarded by attempting each task AND correctly answering related
questions to the satisfaction of the instructor.]
Lambda calculus is a model of computation that is equivalent to Turing machines (as per the Church-
Turing thesis). Lambda calculus, with which the λ (lambda) symbol in computer science is
synonymous, reduces all computation to the basic operations involving only functions and its
application.
Quoting Types and Programming Languages (Benjamin C. Pierce, 2002), it can be seen
``simultaneously as a simple programming language in which computations can be described and as a
mathematical object about which rigorous statements can be proved.''. It has wide applications in
computer science, namely in programming language theory (which is also a popular research area at
UQ and in Australia!). Lambda calculus has inspired many old and modern programming languages,
and is notably the basis of functional programming, a programming paradigm in which entire
programs are made using functions; functional programming languages that you might know are Lisp,
Haskell and OCaml. All other modern programming languages have now borrowed concepts from
functional programming, through the use of a lambda keyword in one form or another including C++
(in the 2011 standard), Javascript and even Python.
In this laboratory, you will build off of concepts in the Lambda calculus and verify them with
Mikrokosmos, an educational Lambda calculus interpreter. You must use Mikrokosmos to receive any
marks for this demo. There are a few different ways of using Mikrokosmos, choose one of the
following:
• EITHER via an online interpreter for Mikrokosmos that can be used to run the language. This
is probably the easiest way for you to use it -- the installation process is challenging,
especially if you're not using Linux and don't have command line tools handy.
• OR set up a local environment by following instructions from Mikrokosmos' documentation
steps. This should be straight forward on Linux/Unix like systems and on Windows it will be
easier on Windows Subsystem for Linux (WSL) that provides a seamless Linux integration
within Windows.
Section I – Mikrokosmos Tutorial
The official tutorial available in their website is a valuable resource if you find it difficult to follow the
intermediate steps:
Mikrokosmos Tutorial – https://mroman42.github.io/mikrokosmos/tutorial.html
Try getting a hang of Lambda calculus from the tutorials and playing with Mikrokosmos to better
understand Lambda calculus and the interpreter before you start the following section. Although
you do not receive marks for this section and you do not have to complete the entire tutorial, there
is significant overlap with the tutorials and the requirements of the next section that do award
marks.
COMP2048 Theory of Computation S. S. Chandra
2
Section II – Lambda Calculus with Mikrokosmos (12 Marks)
For the following exercises, you must first come up with a Lambda calculus statement for the
corresponding function, and then try it out using Mikrokosmos; you can use inbuilt LaTeX or
Markdown interpreter in Jupyter notebooks to annotate your work with Mikrokosmos.
You may refer to Mikrokosmos' standard library to do some of these trivially, but if you've done the
tutorials on Mikrokosmos and learnt its syntax, then you can simply use the representations on the
Wikipedia page as Mikrokosmos has a one-to-one correspondence (for this exercise).
-------------------------------
[See the relevant sections of the Mikrokosmos Tutorial for hints]
1. Define the numbers 0 through 5 with Church encoding using the identity function and the
successor function.
(1 mark)
2. Define separate functions that doubles its argument, adds two numbers, and multiplies two
numbers.
(1 mark)
3. Define the logical operators true and false in lambda calculus.
(1 mark)
4. Define the AND, OR and NOT operators in lambda calculus.
(1 mark)
5. Define the XOR operator Lambda calculus.
(1 mark)
6. Define the “less than or equal to” and “greater than or equal to” functions of two arguments.
(1 mark)
7. Define the Y-combinator in Lambda calculus, and give a brief explanation on how it works.
(2 marks)
8. Write a recursive Greatest Common Divisor (GCD) function (see Euclid’s Algorithm) using the Y-
combinator. [Hint: You might need to use functions you have defined earlier]
(2 marks)
9. Define a list in the Lambda calculus; explain how “indexing” in it works.
(2 marks)
Section III – Beta Reduction (3 Marks)
A Apply beta reduction to the following expressions. Do them by hand using the beta reduction rules
and then verify them using Mikrokosmos. If the expression cannot be reduced, give a brief explanation
as to why. Show all working.
-------------------------------
1. (. )(.)
(1/2 marks)
2. (. )(((. )))
(1/2 marks)
3. (. ())(. )
(1/2 marks)
4. (�. (.)�)(.)
COMP2048 Theory of Computation S. S. Chandra
3
(1/2 marks)
5. (�. ()��. ()�)
(1 mark)
References
Benjamin C. Pierce, 2002. Types and Programming Languages, The MIT Press. The MIT Press,
Cambridge, Mass.
Copeland, B.Jack., 2004. Essential Turing: Classic Writings on Minds and Computers. Oxford
University Press, Oxford, UK.
Moore, C., Mertens, S., 2011. The Nature Of Computation. Oxford University Press.
End of Laboratory