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.

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 structural, with 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.

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 $x and $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 in the body of the function defined using letrec would be captured by the lambda $x declaration in the definition of letrec.

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.

Go to Lesson 8, LAMBDA: Multiple Binding Constructs.

MOVIE (out of date) [5'10"]