Language specification and variable binding

This tutorial demonstrates the use of the Coq proof assistant for reasoning about higher-order programming languages, such as those based on the lambda calculus, and their implementations. We use a simply-typed lambda calculus as a running example. Reasoning about languages with first-class functions is difficult because of variable binding. In particular, there are two important complications that make working with lambda-terms difficult.

• First, we would like to work up to alpha-equivalence. In other words, we would like our reasoning about lambda terms to not depend on the names that we use for free variables.
  For example, we would like to show that these two terms are indistinguishable to the semantics
  \x.x and \y.y
• Second, substitution should be capture avoiding. When we substitute terms with free variables, those free variables should never become bound by the terms they are being substituted into. This means that sometimes we need to rename bound variables to avoid capture. For example,
  [ z ~> \x.y ](\y.z) should be \y1.\x.y

Approaches to variable binding

Unfortunately, variable binding is an old problem. The issue isn't that we don't know how to solve this problem, in fact there are many, many different ways to solve this problem and they all have their trade offs. I won't include an entire taxonomy of solutions here, but before we go further, I want to mention a few relevant alternatives.

• Only working with closed terms, never reasoning about equivalence

If we never have to substitute an open term, then we never have to worry about variable capture. We can represent binding variables in lambda terms using names in a straightforward manner. This approach is the simplest and side-steps the two problems shown above. For example, it can be used to show type soundness, as is done in Software Foundations. However, this approach does not scale. For example, reasoning about compiler optimizations requires reasoning about the equivalence of transformed open terms.

• Named terms, with swapping

We can still work with named terms, even in the presence of free variables, as long as we define alpha equivalence and substitution appropriately. There are, again, many approaches to these definitions. However, the most elegant approach is inspired by Nominal Logic.

• Locally nameless representation (LN)

When working in Coq, it is convenient to use a representation that makes all alpha-equivalent terms definitionally equivalent. LN does this while still providing an interface that is mostly similar to paper proofs. Other approaches to variable binding include de Bruijn indices, de Bruijn levels, weak HOAS, PHOAS, locally named, canonically named... etc. Of these, de Bruijn representations are by far the most commonly used representation in Coq.

Overview

In this tutorial, we will promote the following approach to variable binding.

• Use a locally nameless representation to specify and reason about the semantics
• Use a named representation to implement environment-based interpreters for lambda calculus terms. If binders are mostly unique, then this implementation avoids additional work.
• The definitions, lemmas and proofs that are needed to work with lambda-calculus terms are highly automatable.

In the first part of the tutorial, we will demonstrate the use of a locally nameless representation to reason about a specification of a call-by-name lambda calculus. We will state the operational semantics of this language using a small-step substitution-based inductive relation. We will use this specification for metatheoretic reasoning: we will prove preservation and progress as in Software Foundations. Next, we will represent the same language using a nominal representation but specify the semantics using an abstract machine. This abstract machine is given as a Coq function from machine configurations to machine configurations, and can be used as an efficient interpreter. This abstract machine features a heap (i.e. runtime environment for variables) so we will not need to define capture-avoiding substitution as part of our semantics. Finally, we will prove that the abstract machine implements the same semantics as the locally nameless based substitution semantics.

Tool support

The development of this tutorial draws from two coordinating tools that support working with LN representations. The Ott tool provides a direct way of generating LN language definitions from a simple specification language. The file stlc.ott contains the input specification of the language of this tutorial. Definitions.v is a commented version of the Ott output. (For comparison, the raw output is in Stlc.v). The same specifications can also be used to produce LaTeX macros for typesetting language definitions, demonstrated in stlc.pdf. The LNgen tool works with Ott to generate a number of lemmas and auxiliary definitions for working with LN terms. The file Lemmas.v is commented version of that output. (For comparison, the raw output is in Stlc_inf.v.)

The simply-typed lambda calculus in Coq.

First, we import a number of definitions from the Metatheory library (see Metatheory.v). The following command makes those definitions available in the rest of this file. This command will only succeed if you have already run make and make install in the Metatheory directory to compile the Metatheory library.

Next, we import the definitions of the simply-typed lambda calculus. If you haven't skimmed this file yet, you should do so now. You don't need to understand everything in the file at first, but you will need to refer back to it in the material below.

And some notations (defined in `Stlc.Definitions`), but not automatically brought into scope.

For the examples below, we introduce some sample variable names to play with.

Encoding STLC terms

We start with examples of encodings in STLC. For example, we can encode the expression (\x. Y x) as below. We use the index 0 because it refers to the closest abs to the bound variable occurrence.

Here is another example: the encoding of (\x. \y. (y x)).

Finally, here is an example where the same bound variable has two different indices, and the same index refers to two different bound variables. \y. ((\x. (x y)) y)

Exercise: term representation

Define the following lambda calculus terms using the locally nameless representation. "two" : \s. \z. s (s z) "COMB_K" : \x. \y. x "COMB_S" : \x. \y. \z. x z (y z)

There are two important advantages of the locally nameless representation:

• Alpha-equivalent terms have a unique representation. We're always working up to alpha-equivalence.
• Operations such as free variable substitution and free variable calculation have simple recursive definitions (and therefore are simple to reason about).

Weighed against these advantages are two drawbacks:

• The exp datatype admits terms, such as abs 3, where indices are unbound. A term is called "locally closed" when it contains no unbound indices.
• We must define *both* bound variable & free variable substitution and reason about how these operations interact with each other.

Substitution

The substitution function replaces a free variable with a term. For simplicity, we define a notation for free variable substitution that mimics standard mathematical notation.

To demonstrate how free variable substitution works, we need to reason about var equality.

The decidable var equality function returns a sum. If the two vars are equal, the left branch of the sum is returned, carrying a proof of the proposition that the vars are equal. If they are not equal, the right branch includes a proof of the disequality. The demo below uses three new tactics:

• The tactic simpl reduces a Coq expression to its normal form.
• The tactic destruct (Y==Y) considers the two possible results of the equality test.

Exercise subst_eq_var

We can use almost the same proof script as above to show how substitution works in the variable case. Try it on your own.

Exercise subst_neq_var

Exercise subst_same

Free variables

The function fv_exp calculates the set of free variables in an expression. This function returns a value of type `atoms` --- a finite set of variable names. Demo fsetdec The tactic fsetdec solves a certain class of propositions involving finite sets. See the documentation in FSetWeakDecide for a full specification.

Recommended Exercise subst_exp_fresh_eq

To show the ease of reasoning with these definitions, we will prove a standard result from lambda calculus: if a variable does not appear free in a term, then substituting for it has no effect. HINTS: Prove this lemma by induction on e.

• You will need to use simpl in many cases. You can simpl everything everywhere (including hypotheses) with the pattern simpl in ×.
• Part of this proof includes a false assumption about free variables. Destructing this hypothesis produces a goal about finite set membership that is solvable by fsetdec.
• The f_equal tactic converts a goal of the form f e1 = f e1' in to one of the form e1 = e1', and similarly for f e1 e2 = f e1' e2', etc.

Additional Exercises

Step through the proof that free variables are not introduced by substitution. This proof actually is very automatable (simpl in *; auto. takes care of all but the var_f case), but the explicit proof below demonstrates two parts of the finite set library. These two parts are the tactic destruct_notin and the lemma notin_union, both defined in the module FSetWeakNotin. Before stepping through this proof, you should go to that module to read about those definitions and see what other finite set reasoning is available.

Now prove the following properties of substitution and fv

Exercise subst_exp_fresh_same

Exercise fv_exp_subst_exp_fresh

Exercise fv_exp_subst_exp_upper

LN specific operations and relations

Because we are working with a locally nameless representation, we have a few more operations to consider when working with these terms.

Opening

Opening replaces an index with a term and is defined in the Definitions module. This next demo shows the operation of open. For example, the locally nameless representation of the term (\y. (\x. (y x)) y) is abs (app (abs (app 1 0)) 0). To look at the body without the outer abstraction, we need to replace the indices that refer to that abstraction with a name. Therefore, we show that we can open the body of the abs above with Y to produce app (abs (app Y 0)) Y).

Local closure

The local closure judgement classifies terms that have no dangling indices. Step through this derivation to see why the term ((\x. Y x) Y) is locally closed.

Properties about basic operations

The most important properties about open and lc_exp concern their relationship with the free variable and subst functions. For example, one important property is shown below: that we can commute free and bound variable substitution. We won't prove this lemma as part of the tutorial (it is proved in Lemmas.v), but it is an important building block for reasoning about LN terms. NOTE: the name of this lemma was automatically generated by LNgen. If we have multiple syntactic classes and multiple sorts of variables, we need to distinguish the different forms of substitution from eachother.

Exercise subst_var

The lemma above is most often used with e2 as some fresh variable. Therefore, it simplifies matters to define the following useful corollary. HINT: Do not use induction. Rewrite with subst_exp_open_exp_wrt_exp and subst_neq_var.

Exercise subst_exp_intro

This next lemma states that opening can be replaced with variable opening and substitution. This lemma, like many about open_exp_wrt_exp, should be proven via induction on the term e. However, during this induction, the binding depth of the term changes, so to make sure that we have a flexible enough induction hypothesis, we must generalize the argument to open_exp_wrt_exp_rec.

Exercise fv_exp_open_exp_wrt_exp_upper

Now prove the following lemmas about the free variables of an opened term. The structure of this proof follows that of the proof above. You should prove this by induction on the term e1, after appropriately generalizing the induction hypothesis. Remember to use fsetdec for reasoning about properties of atom sets. Also note that you can rewrite with atom set inequalities in the hypotheses list.

Forall quantification in lc_exp.

Let's look more closely at lc_abs and lc_exp_ind.

The induction principle for the lc_exp relation is particularly strong in the abs case.

 forall P : exp -> Prop,
       ...
       (forall e : exp,
        (forall x : atom, lc_exp (e ^ x)) ->
        (forall x : atom, P (e ^ x)) -> P (abs e)) ->
       ...
       forall e : exp, lc_exp e -> P e

This principle says that to prove that a property holds for an abstraction, we can assume that the property holds for the body of the abstraction, opened with *any* variable that we like.

However, on the other hand, when we show that an abstraction is locally closed, we need to show that its body is locally closed, when opened by any variable. That can sometimes be a problem.

Here we are stuck. We don't know that x0 is not equal to x, which is a preconduction for subst_var. The solution is to prove an alternative introduction rule for local closure for abstractions. In the current rule, we need to show that the body of the abstraction is locally closed, no matter what variable we choose for the binder.

  | lc_abs : forall e,
      (forall x:var, lc_exp (open e x)) ->
      lc_exp (abs e)

An easier to use lemma requires us to only show that the body of the abstraction is locally closed for a single variable. As before, we won't prove this lemma as part of the tutorial, (it too is proved in Lemmas.v) but we will use it as part of our reasoning.

For example, with this addition, we can complete the proof above.

Local closure and relations

All of our semantics only hold for locally closed terms, and we can prove that. Sometimes, the proofs are straightforward; sometimes a little work is needed.

Exercise typing_to_lc_exp

Use lc_abs_exists below to show that well-typed terms are locally closed.

Exercise step_lc_exp2

Use properties such as subst_exp_intro and subst_exp_lc_exp to show that the result of a step is also locally closed.