Multiple Binding Constructs

Here we learn how multiple language constructs that bind variables can coexist. We will also learn about or recall another famous binder besides lambda, namely mu, which can be used to elegantly define all kinds of interesting fixed-point constructs.

The mu binder has the same syntax as lambda, except that it replaces lambda with mu.

Since mu is a binder, in order for substitution to know how to deal with variable capture in the presence of mu, we have to tell it that mu is a binding construct, same like lambda. We take advantage of being there and also add mu its desired latex attribute.

The intuition for

mu x . e

is that it reduces to e, but each free occurrence of x in e behaves like a pointer that points back to mu x . e.

With that in mind, let us postpone the definition of mu and instead redefine letrec F X = E in E' as a derived construct, assuming mu available. The idea is to simply regard F as a fixed-point of the function

lambda X . E

that is, to first calculate

mu F . lambda X . E

and then to evaluate E' where F is bound to this fixed-point:

let F = mu F . lambda X . E in E'

This new definition of letrec may still look a bit tricky, particularly because F is bound twice, but it is much simpler and cleaner than our previous definition. Moreover, now it is done in a type-safe manner (this aspect goes beyond our objective in this tutorial).

Let us now define the semantic rule of mu.

The semantics of mu is actually disarmingly simple. We just have to substitute mu X . E for each free occurrence of X in E:

mu X . E => E[(mu X . E) / X]

Compile lambda.k and execute some recursive programs. They should be now several times faster. Write a few more recursive programs, for example ones for calculating the Ackermann function, for calculating the number of moves needed to solve the Hanoi tower problem, etc.

We have defined our first programming language in K, which allows us to write interesting functional programs. In the next lesson we will learn how to fully document our language definition, in order to disseminate it, to ship it to colleagues or friends, to publish it, to teach it, and so on.

Go to Lesson 9, LAMBDA: A Complete and Commented Definition.

MOVIE (out of date) [2'40"]