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
mu, which can be used to elegantly define all kinds of
interesting fixed-point constructs.
mu binder has the same syntax as lambda, except that it replaces
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
mu its desired latex attribute.
The intuition for
mu x . e
is that it reduces to
e, but each free occurrence of
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
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
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
The semantics of
mu is actually disarmingly simple. We just have to
mu X . E for each free occurrence of
mu X . E => E[(mu X . E) / X]
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.