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.