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
As a side point, which is not very relevant here but good to know, we may
want the desugaring of
let to not even count as a computational step, but
as a mere structural rearrangement of the program so that other semantic
rules (beta reduction, in our case) can match and apply.
The K tool allows us to tag rules with the attribute
precisely the intuition above. You can think of structural rules as a kind
of light rules, almost like macros, or like ones which apply under the hood,
instantaneously. There are several other uses for structural rules in K,
which we will discuss later in this tutorial.
lambda.k and write some programs using
For example, consider a
lets.lambda program which takes
and replaces each integer by a let-bound variable. It should evaluate to
true, just like the original
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
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
There are two interesting observations here.
First, note that we have already in-lined the definition of the
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
$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 x
declaration in the definition ofletrec`.
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
on another binder,
mu, specifically designed to define fixed points.