A nominal representation of STLC terms. This version looks a lot like we expect a representation of the lambda calculus to look like. Unlike the LN version, the syntax does not distinguish between bound and free variables and abstractions include the name of binding variables.

Imports

Some of our proofs are by induction on the *size* of terms. We'll use Coq's omega tactic to easily dispatch reasoning about natural numbers.

We will use the atom type from the metatheory library to represent variable names.

Although we are not using LNgen, some of the tactics from its library are useful for automating reasoning about names.

Some fresh variables

A nominal representation of terms

For example, we can encode the expression (\X.Y X) as below.

For example, we can encode the expression (\Z.Y Z) as below.

As usual, the free variable function needs to remove the bound variable in the n_abs case.

The tactics for reasoning about lists and sets of atoms are useful here too.

What makes this a *nominal* representation is that our operations are based on the following swapping function for names. Note that this operation is symmetric: x becomes y and y becomes x.

The main insight of nominal representations is that we can rename variables, without capture, using a simple structural induction. Note how in the n_abs case we swap all variables, both bound and free. For example: (swap x y) (\z. (x y)) = \z. (y x)) (swap x y) (\x. x) = \y.y (swap x y) (\y. x) = \x.y

Because swapping is a simple, structurally recursive function, it is highly automatable using the default_simp tactic from LNgen library. This tactic "simplifies" goals using a combination of common proof steps, including case analysis of all disjoint sums in the goal. Because atom equality returns a sumbool, this makes this tactic useful for reasoning by cases about atoms. For more information about the default_simp tactic, see metalib/LibDefaultSimp.v. WARNING: this tactic is not always safe. It's a power tool and can put your proof in an irrecoverable state.

We define the "alpha-equivalence" relation that declares when two nominal terms are equivalent (up to renaming of bound variables). Note the two different rules for n_abs: either the binders are the same and we can directly compare the bodies, or the binders differ, but we can swap one side to make it look like the other.

Properties about swapping

Now let's look at some simple properties of swapping.

Demo: We will need the next two properties later in the tutorial, so we show that even though there are many cases to consider, default_simp can find these proofs.

Exercises

Recommended Exercise: swap properties

Prove the following properties about swapping, either explicitly (by destructing x == y) or automatically (using default_simp).

Challenge exercise: equivariance

Equivariance is the property that all functions and relations are preserved under swapping. (Hint: default_simp will be slow on some of these properties, and sometimes won't be able to do them automatically.)

An abstract machine for cbn evaluation

The advantage of named terms is an efficient operational semantics! Compared to LN or de Bruijn representation, we don't need always need to modify terms (such as via open or shifting) as we traverse binders. Instead, as long as the binder is "sufficiently fresh" we can use the name as is, and only rename (via swapping) when absolutely necessary. Below, we define an operational semantics based on an abstract machine. As before, it will model execution as a sequence of small-step transitions. However, transition will be between machine configurations, not just expressions. Our abstract machine configurations have three components:

• the current expression being evaluated the heap (aka
• environment): a mapping between variables and expressions
• the stack: the evaluation context of the current
• expression

Because we have a heap, we don't need to use substitution to define our semantics! To implement x ~> e we add a definition that x maps to e in the heap and then look up the definition when we get to x during evaluation.

The (small-step) semantics is a function from configurations to configurations, until completion or error.

Example: evaluation of "(\y. (\x. x) y) Z"

     machine                                       corresponding term

      {}, (\y. (\x. x) y) Z , nil                  (\y. (\x. x) y) Z
  ==> {}, (\y. (\x. x) y), n_app2 Z :: nil         (\y. (\x. x) y) Z
  ==> {y -> Z}, (\x.x) y, nil                      (\x. x) Z
  ==> {y -> Z}, (\x.x), n_app2 y :: nil            (\x. x) Z
  ==> {x -> y, y -> Z}, x, nil                     Z
  ==> {x -> y, y -> Z}, y, nil                     Z
  ==> {x -> y, y -> Z}, Z, nil                     Z
  ==> Done

(Note that the machine takes extra steps compared to the substitution semantics.) We will prove that this machine implements the substitution semantics in the next section.

Recommended Exercise values_are_done

Show that values don't step using this abstract machine. (This is a simple proof.)

Size based reasoning

Some properties about nominal terms require calling the induction hypothesis not on a direct subterm, but on one that has first had a swapping applied to it. However, swapping names does not change the size of terms, so that means we can prove such properties by induction on that size.

Capture-avoiding substitution

We need to use size to define capture avoiding substitution. Because we sometimes swap the name of the bound variable, this function is not structurally recursive. So, we add an extra argument to the function that decreases with each recursive call.

Our real substitution function uses the size of the size of the term as that extra argument.

This next lemma uses course of values induction lt_wf_ind to prove that the size of the term t is enough "fuel" to completely calculate a substitution. Providing larger numbers produces the same result.

Challenge Exercise subst

Use the definitions above to prove the following results about the nominal substitution function.