## Lambda Calculus Demo

You are required to do either this Lambda Calculus demo OR the Quantum Computation demo

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 of function definition and application. Quoting Types and Programming Languages, 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. There are also several other modern programming languages that have borrowed concepts from functional programming, most notably lambda functions.

In this laboratory, you’ll build off of concepts in the Lambda calculus and verify them with Mikrokosmos, an educational Lambda calculus interpreter. You must use Mikrokosmos (available only in Python) to receive any marks for this prac. There’s a few different ways of using Mikrokosmos:

• There is 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.
Setting up a local environment by following these steps:
1. Install cabal (Haskell package manager)
2. Install pip (Python package manager)
3. Following remaining instructions from Mikrokosmos’ documentation

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 $I A T_{\mathrm{E}} X / \mathrm{md}$ interpreter in Jupyter notebooks to annotate your work with Mikrokosmos. Try getting a hang of Lambda calculus from the tutorials and playing with Mikrokosmos before you start these. Try these exercises yourself to better understand Lambda calculus.

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).

1. Define the numbers 0 through 5 with Church encoding using the identity function and the successor function (refer to the Church numerals Wikipedia page to find out how they’re encoded). (2 marks)
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 marks)
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 in the prac] (4 marks)
9. Define a list in the Lambda calculus; explain how “indexing” in it works. (2 marks)
10. Beta Reduction exercises (in roughly increasing difficulty); if the expression cannot be reduced, give a brief explanation as to why. Show all working. (1 mark each)
$$(\lambda x . x)(\lambda y . y z)$$
$$(\lambda x . x)(((\lambda x . x)) y)$$
$x$
$$(\lambda x .(x y))(\lambda z . z)$$
$\bullet$
$$((\lambda x \cdot(\lambda y \cdot y x)) x)(\lambda z \cdot w)$$
$$((\lambda x .(x x))(\lambda x .(x x)))$$