Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: daixieit

COMP2K

Lambda Calculus

Laboratory

[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 theChurch- Turing thesis).     Lambda  calculus,  with  which  the  y  (lampqa)  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 anonline interpreter for Mikrokosmosthat 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.

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.    (入x.x)(入y.yz) (1/2 marks)

2.    (入x.x)(((入x.x))y) (1/2 marks)

3.    (入x. (xy))(入z.z) (1/2 marks)

4.    ((入x. (入y.yx))x)(入z.w) (1/2 marks)

5.    ((ax. (xx))(ax. (xx))) (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.