Crash Course

First Steps

Download the pre-compiled package for Windows or Linux from the web page and extract the package with tar xfz cubint_linux.tar.gz on Linux or your favourite tool (e.g. WinZip) on Windows respectively. Start the interpreter with a double click on the executable (or alternatively ./cubint on Linux). Type help;<RETURN> for information about available commands.

Untyped $\lambda$-Calculus

To switch to the untyped $\lambda$-calculus type switch tm u;<RETURN>. The syntax for untyped terms is as follows:

calculus	interpreter input
$x$	x
$\lambda x.t$	\x.t
$t_1\;t_2$	t1 t2

Let's look at some examples:

• We apply the identity function several times to itself:
  
  $$(\lambda x.x) (\lambda x.x) (\lambda x.x)$$
  
  
  can be fed to the interpreter as
  (\x.x) (\x.x) (\x.x)

  We can also bind the identity function to the identifier $id$ and apply the identifiers several times. This is shown in figure 1.

  Figure 1: definition and use of $id$

  

  As you probably noticed there are to binding constructs, namely def and rdef. The first one only binds a term to an identifier whereas the second one performs $beta$-reduction before binding.

• Now we define church booleans.
  

  $tru = \lambda t.\lambda f. t$	def tru = \t.\f.t
  $fls = \lambda t.\lambda f.f$	def fls = \t.\f.f
  $test = \lambda l.\lambda m.\lambda n.l\;m\;n$	def test = \l.\m.\n. l m n

  
  

  On the left hand side you can see the conventional definition in the untyped $\lambda$-calculus and on the right hand side there is the corresponding interpreter input. We use these definitions in the following examples:

  - def v = \x.x;
  > def v = <fun> : *
  - def w = \x.\y.x;
  > def w = <fun> : *
  - test tru v w;
  > def it = v : *
  - rdef result = test fls v w;
  > def result = w : *
  

• As a last example we give a definition of a fixpoint combinator:
  
  $$\lambda f. (\lambda x.\lambda y. f (x x) y) (\lambda x.\lambda y. f (x x) y)$$
  
  
  def Fix = \f.(\x.\y.f (x x) y) (\x.\y.f (x x) y)

  
  

  If you are not convinced that it works, conduct the following test:

  def gauss_sum = Fix (\f.\x.if x<=0 then 0 else x+f(x-1));<RETURN>
  gauss_sum 6;<RETURN>
  

  You should get def it = 26.

Simply Typed $\lambda$-Calculus

At the end of the last section we saw that Cubint supports built-in integers. As you know from the lecture this extension is very error-prone in the untyped calculus, i.e. it is very simple to input terms whose evaluation get stuck (e.g. 3+(\x.x)). Therefore types are introduced. The syntax looks as follows:

$\lambda$calculus	interpreter input
$x$	x
$\lambda x:\mathbf{T}.t$	\x:T.t
$t_1\:t_2$	t1 t2
$T\rightarrow T$	T->T
$Int$	Int

The $\lambda$-abstraction needs a type annotation. Types can be built with ->. Int is the base type for integers. For a full overview about the syntax look at 5.1.

The interpreter is started in simply typed mode at the beginning. You can also change the mode on-the-fly by typing switch tm s;<RETURN>.

Let's look at some basic examples:

• Term definitions work as before:
  
  $$\lambda f:Int\rightarrow Int.\lambda x:Int.f\:x$$
  
  
  \f:Int->Int.\x:Int.f x

• You also have the possibility to bind types to an identifier and use it in a term:

  def T = Int -> Int;
  def f  = \g:T.\x:Int.g x
  

This concludes the short overview about the base calculi. The following sections describe the usage of Cubint in more detail. All available interpreter commands and syntactic entities are listed. If you need more examples, use the tests library.