Derived Constructs, Extending Predefined Syntax
In this lesson we will learn how to define derived language constructs, that is, ones whose semantics is defined completely in terms of other language constructs. We will also learn how to add new constructs to predefined syntactic categories.
When defining a language, we often want certain language constructs to be defined in terms of other constructs. For example, a let-binding construct of the form
let x = e in e'
is nothing but syntactic sugar for
(lambda x . e') e
This can be easily achieved with a rule, as shown in lambda.k.
Compile lambda.k and write some programs using let binders.
For example, consider a lets.lambda program which takes arithmetic.lambda
and replaces each integer by a let-bound variable. It should evaluate to
true, just like the original arithmetic.lambda.
Let us now consider a more interesting program, namely one that calculates the factorial of 10:
let f = lambda x . (
(lambda t . lambda x . (t t x))
(lambda f . lambda x . (if x <= 1 then 1 else (x * (f f (x + -1)))))
x
)
in (f 10)
This program follows a common technique to define fixed points in untyped lambda calculus, based on passing a function to itself.
We may not like to define fixed-points following the approach above, because
it requires global changes in the body of the function meant to be recursive,
basically to pass it to itself (f f in our case above). The approach below
isolates the fixed-point aspect of the function in a so-called fixed-point
combinator, which we call fix below, and then apply it to the function
defining the body of the factorial, without any changes to it:
let fix = lambda f . (
(lambda x . (f (lambda y . (x x y))))
(lambda x . (f (lambda y . (x x y))))
)
in let f = fix (lambda f . lambda x .
(if x <= 1 then 1 else (x * (f (x + -1)))))
in (f 10)
Although the above techniques are interesting and powerful (indeed, untyped lambda calculus is in fact Turing complete), programmers will probably not like to write programs this way.
We can easily define a more complex derived construct, called letrec and
conventionally encountered in functional programming languages, whose semantics
captures the fixed-point idea above. In order to keep its definition simple
and intuitive, we define a simplified variant of letrec, namely one which only
allows to define one recursive one-argument function. See lambda.k.
There are two interesting observations here.
First, note that we have already in-lined the definition of the fix
combinator in the definition of the factorial, to save one application of the
beta reduction rule (and the involved substitution steps). We could have
in-lined the definition of the remaining let, too, but we believe that the
current definition is easier to read.
Second, note that we extended the predefined Id syntactic category with two
new constants, $x and $y. The predefined identifiers cannot start with
$, so programs that will be executed with this semantics cannot possibly
contain the identifiers y. In other words, by adding them to Id they
become indirectly reserved for the semantics. This is indeed desirable,
because any possible uses of xdeclaration in the definition ofletrec`.
Using letrec, we can now write the factorial program as elegantly as it can
be written in a functional language:
letrec f x = if x <= 1 then 1 else (x * (f (x + -1)))
in (f 10)
In the next lesson we will discuss an alternative definition of letrec, based
on another binder, mu, specifically designed to define fixed points.