090116.md

Sept 1, 2016

Goal: Introduce and reinforce proof skills about programming languages with binding by connecting paper proofs with Coq proofs. This requires understanding what is going on when we do a paper proof.

Last time: we saw a simple language with a single binding construct

op ::= + | * | ^
ty ::= num | string
e  ::= x                     variables
     | i                     constant ints
     | s                     constant strings
     | e1 op e2              binary operations
     | let x be e1 in e2     let expressions

When working with languages on paper and in textbooks like PFPL, we often use something that looks like concrete syntax (as above). This syntax is much more concise than working with abstract syntax trees in Coq; but it is important to be able to go back and forth between the two notations easily.

Last time we defined two operations on this language: (capture-avoiding) substitution and free variable calculations. We also carefully chose our Coq representation so that we didn't have to define a third predicate: alpha-equivalence. All alpha-equivalent terms have the same representation.

alpha-equivalence

But, let's go back to paper. What do the same definitions, written using the "concrete" syntax above, look like? What does it mean to work up-to-alpha equivalence?

Remember: the principle that we want to work with is that "bound variables don't matter" i.e. alpha-equivalence says that the expressions

let x be 1 in x + z

is exactly the same as

let y be 1 in y + z

Can we define alpha-equivalence formally?

Before we do so, following PFPL, we need to characterize the set of variables that can occur in an expression

Define e in exp[X] when

• e is x and x in X
• e is i or s
• e is e1 op e2 and e1 in exp[X] and e2 in exp[X]
• e is let x be e1 in e2 and e1 in exp [X] and [x <~> z]e2 in exp[X,z] for all z not in X

Above, the notation [x <~> z]e is not substitution (we haven't defined it yet anyways...). Instead, it is a renaming operation that replaces all occurrences of x with z (and all occurrences of z with x).

So X is some (undefined) superset of the free variables of e! We need this set around when we define alpha equivalence.

Define e1 =aeq=^X e2, when e1, e2 in exp[X] by the following inductive definition

x  =aeq^X=  x  

i  =aeq^X=  i

s  =aeq^X= s 

If  e1 =aeq^X= e1'  and  e2 =aeq^X= e2'  then  e1 op e2  =aeq^X= e1' op e2'

For let, we want to identify terms with different binders. This is (sort of) what PFPL defines:

If  e1 =aeq^X= e1'  and  forall fresh z, [x <~> z]e2 =aeq^{X,z}= [y <~> z]e2' then
let x be e1 in e2  =aeq^X= let y be e1' in e2'

Here fresh means that z is not in X.

Below, I'll often drop the ^X on the symbol for alpha-equivalence.

This definition of aeq is an equivalence relation. We can show that it is reflexive, symmetric and transitive.

Let's look at the proof of reflexivity:

Lemma [reflexivity]: forall e in exp[X],  e =aeq=e

We can try to prove this lemma by induction on the structure of e. It starts out ok.

• The variable & constant cases are trivial. We just need to show, for example, that x =aeq= x.

• In the case of binary operators, we need to show that e1 op e2 =aeq= e1 op e2. However, we have two induction hypotheses to use: e1 =aeq= e1 and e2 =aeq= e2. So we are done.

• We run into trouble in the let case, where e is let x be e1 in e2. We can use induction to show that e1 =aeq= e1. But we need to show that for all fresh renamings z, we have [x <~> z]e2 =aeq= [x <~> z]e2

However, all we know by structural induction is that e2 =aeq= e2. We don't know about alpha equivalence for renamings of x.

One solution is to switch to induction on the height of the term. Renaming the variable x to z doesn't change the height, no matter which variable we use for z. So our induction principle will apply to [x <~> z]e2 and we can finish the proof.

Structural induction modulo renaming

PFPL captures this idea with a stronger induction principle for expressions: structural induction modulo fresh renaming. It is the same as structural induction except in the case of let: there we can directly assume that whatever property we are trying to prove holds for any fresh renaming of the body of the let expression.

The structural induction principle modulo renaming looks like this (sort of):

 forall P, 
    (P x)
 -> (P i)
 -> (P s)
 -> (forall e1  e2, P e1 -> P e2 -> P (e1 op e2))
 -> (forall e1 x e2, P e1 ->
     (forall y, y "fresh" -> P ([x<~>y]e2) -> P (let x be e1 in e2)))
 -> forall e, P e

Compare the case for let above with the one from structural induction, which reads this instead:

 -> (forall e1 x e2, P e1 -> P e2 -> P (let x be e1 in e2)))

When we use the structural induction principle, we get to assume that the the IH applies only to e2 with one particular name x. However, with the principle above instead, our IH applies to e2 with any name for the bound variable. This is exactly the IH we needed for the reflexivity proof above. (Also see below of an example proof that needs this reasoning.)

Of course, to be fully precise, we need to add the implicit argument to this principle --- the set of variables X that control freshness. We want the property to hold true for all expressions e in exp[X]. So we need to quantify over X everywhere. (I think I quantified the Xs in the wrong place in class...)

 forall P : (forall X, exp -> Prop), 
    (forall X, x in X -> P X x)
 -> (forall X, P X i)
 -> (forall X, P X s)
 -> (forall X, e1 in exp[X], e2 in exp[X],
    P X e1 -> P X e2 -> P X (e1 op e2))
 -> (forall X X x e1, e1 in exp[X], P X e1,
    forall e2, (forall y, y `notin` X -> [x<~>y]e2 in exp[X,y]) ->
    (forall y, y `notin` X -> P (X \u {{y}}) [x<~>y] e2)
	-> P X (let x be e1 in e2))
 -> forall X, e in exp[X], P X e

Induction modulo renaming in action

Let's see this induction principle in action. We will prove this lemma.

    Lemma [transitivity]: If e1 =aeq= e2 and e2 =aeq= e3 then e1 =aeq= e3.

Proof by structural induction (modulo renaming) on e2.

• If e2 is a variable or constant, than we know what e1 and e3 must be, so we are done.

• If e2 is a binary operator (e21 op e22) then we know that e1 must be (e11 op e12) and e3 must be (e31 op e32). We are done by induction.

• If e2 is let y be e21 in e22 then e1 must be let x be e11 in e12 and e3 must be let z be e31 in e32. We must also know (by the definition of aeq) that

  • forall fresh w, [x <> w]e12 =aeq= [y <> w]e22
  • forall fresh w, [x <> w]e22 =aeq= [z <> w]e32

We want to show that

• forall fresh w, [x <> w]e12 =aeq= [z <> w]e32

And this is exactly our induction hypothesis, because we can make all of these w's fresh for the same set X (as long as e1, e2, e3 in exp[X])!

free variables

Now, here is how the statement of free variables usually goes:

fv x = {{x}}
fv n = {}
fv s = {}
fv (e1 op e2) = fv e1 \u fv e2
fv (let x = e1 in e2) = fv e1 \u (fv e2 - {{x}})

The important bit is in the last line. If we look at e2 by itself, it may have a free occurrence of the variable x. However, if we put e2 in the let x = e1 in __ scope, then x should not be free. So we need to make sure to remove x from the answer.

Now here is a property that should hold about our free variable function:

if e1 =aeq= e2  then fv e1 = fv e2

Can we prove this fact from our definitions? Exercise for the reader. :-)

substitution

Finally we get to capture-avoiding substitution. We want to define an operation, written [ x ~> e1 ] e2, for replacing the free variables x in e2 with e1.

Furthermore, we want this operation to both be total and to respect alpha-equivalence. In other words,

 if  e1 =aeq= e1' and e2 =aeq= e2' then 
 [ x ~> e1 ] e2 =aeq= [x ~> e1' ] e2'

Now we can see the problem with variable capture that we talked about last time. If substitution is not capture-avoiding, then it won't respect aeq.

Here is our definition of substitution:

  [ x ~> e1] x = e1
  [ x ~> e1] y = y  when x <> y
  [ x ~> e1] n = n
  [ x ~> e1] (e2 op e2') = [x ~> e1]e2  op [x ~> e1]e2'
  [ x ~> e1] (let x be e2 in e2') =
     let w be [x ~> e1]e2 in [x ~> e1][w <~> y]e2'
     for w fresh (to avoid capture)

Questions

Questions about representation

• Considering the term "let x be 1 in let y be x in x + y" if we implement it in Ch4.v, what should be used to indicate the second appearance of x (i.e. ... let y be x in ...)? Should it be "exp_bvar 0" or "exp_bvar 1" i.e. should the total definition be

  "exp_let (exp_num 1) (exp_let (exp_bvar 0) (exp_op plus (exp_bvar 1) (exp_bvar 0)))"

  or

  "exp_let (exp_num 1) (exp_let (exp_bvar 1) (exp_op plus (exp_bvar 1) (exp_bvar 0)))"?

• In a complete and syntactically correct program of our language, the only case when there would be any dangling indices is when we only look at the body of a let expression, and the only way to produce a free variable is by opening an expression with dangling indices. Is that correct?

Why are we interested in whether an expression is a local closure? Why would we care if all dangling indices are replaced by free variables? Certainly we can prove a lot of interesting lemmas and theorems with this concept, but where do they lead us to?

• In the context of partial evaluation, is there a best way to change opening to make it work well? This is a little hard to demonstrate with the language of CIS670, but consider the following term:

let x be e in let y be x in y + x

which is encoded internally as:

exp_let e (exp_let (exp_bvar 0) (exp_op plus (exp_bvar 0) (exp_bvar 1)))

where e is something we do not yet want to examine. If we try to dive into the let body and open the inner let, we may run into trouble, producing:

exp_let e (exp_op plus (exp_bvar 0) (exp_bvar 1))

which doesn't make sense. How can we fix this?

Subsumed questions

<< All of these are questions that point out typos that have been corrected. >>

• What version of Coq should we be using for CIS 670? I had trouble building Metalib with Coq 8.4 but it works fine with Coq 8.5.

• In proof of subst_lc, I was stuck at the lc_let case. I followed the hint and then needed to prove lc (open ([x ~> u] e2) (exp_fvar x0)) while in hypothesis there is lc ([x ~> u] open e2 (exp_fvar x0)) for any x0 not in L. Then I found that Lemma subst_open could be used to prove it. I would like to see how to prove it without using the Lemma.

• Also in the proof of subst_open, you mentioned not using induction but since e2 is an expr, the hint you give seems ok only when e2 is a free variable, which is also the case in subst_lc. It would be great if you could clarify it more in the next class.

• I was kind of confused by the subst_open lemma, since I'm not sure it holds unless x doesn't appear free in e2.

• Is there a typo in the definition of substitution? In the let rule I see [ x ~> e1] (let w be e2 in e2') = let w be [x ~> e1]e2 in [x > e1][w <> y]e2' for w fresh (to avoid capture)

but should it be [ x ~> e1] (let y be e2 in e2') = let w be [x ~> e1]e2 in [x > e1][w <> y]e2' for w fresh (to avoid capture)

with w changed for y?