Skip to content

Latest commit

 

History

History
166 lines (119 loc) · 6.92 KB

091316.md

File metadata and controls

166 lines (119 loc) · 6.92 KB
Raw

September 16, 2016

  • See (proposed) lecture topic schedule on course website Make an appointment with me before your lecture to go over your plans

  • Talk to me if you haven't figured out your semester project yet Groups are ok!

  • Homework: Finish exercises in Ch4.v, Ch5.v and Ch6.v by Monday, Sept 19th. You do not neeed to do the Challenge exercises (but are strongly encouraged to do so).

  • If you are still new to Coq you may do paper proofs

  • Questions: don't forget to send before each class!

Plan

  • Today

    • Ch4.v (renaming, exists fresh, more Cofinite Quant discussion)
    • Transitions.v and Ch5.v (5.1-5.2)
    • Sneak preview for Ch7 (Evaluation dynamics)

  • Thursday

    • Look at Ch6.v before class
    • Preservation & progress for small step semantics Ch6.v (6.1-6.2) and discussion of bigstep semantics Ch7.v (7.1-7.3).

  • Next week: I am away at ICFP all week, no lectures

    • read Chapters 8 and 9 on your own
    • complete exercises in Ch9.v

  • Following week

    • We will start student lectures
    • Solomon will cover Ch10 on Tuesday

Questions

Questions about co-finite quantification & induction modulo renaming

    1. why we could define both cofinite quantification and exists-fresh version of typing rule for let?
    2. What does admissible mean for let ?

  • I am not clear about the meaning of L in the definition of lc_let. Is there any specific meaning of L? What will be the problem if L is empty?

  • I'm kind of confused by the induction principle stated in PFPL. It seems weird that P is parametrized by X because it suggests that the proposition might change depending on the variables you pass in, which seems like something you'd want to disallow.

    I think you could set P to be E -> Prop with a pre-determined countable set of variables, and had an equivalent induction principle like this, using cofinite induction:

       forall x, P x
   forall n, P n
   forall s, P s
   forall x x' e1 e2, exists X: x' notin X ->
        P e1 -> P ( [ x' / x ] e2 ) -> P (let x be e1 in e2)
   forall e1 e2, P e1 -> P e2 -> P (e1 `op` e2)

    What are the advantages of the approach taken in PFPL?

  • Is structural induction modulo fresh renaming a generalization of cofinite quantification?

  • In defining the judgements of local closure, we used co-finite quantification to acquire a stronger induction hypothesis in the lc_let case. From a mechanical point of view, I understand the purpose of L, but I was wondering if there's some intuitive interpretation we can apply to it?

    For example, later on when Ch4.v talked about the induction principles of ABTs, the set of free variables X indexing each ABT acts like L, and it has an interpretation being the set of free variables that can appear in this ABT, but I'm having some trouble wrapping my head around whether I can think about L in the same way. I believe that in practice, L can be chosen to be any set larger than (fv e2) (set of free variables in the let body), but is that an appropriate way to think about it?

  • Was the motivation for cofinite quantification due to technical difficulties encountered when formalizing metatheory, like the one in the tutorial? It isn't clearly a priori that the initial definition would run into trouble later on. It is worrisome that one may go about doing quite a lot of work before finding out that something at the root should be better revised. I suppose one could patch this by gluing on statements expressing some form of equivalence, but that's hardly ideal.

For example, one possibility of defining local closure is to count the number of binders from the variable to the root. How do we choose the "right" strategy for such?

  • Apart from proving alpha-equivalence, what are other fields that structural induction modulo fresh renaming can be used?

  • In the notes it's stated that the renaming operation [x <~> y] replaces every instance of x with y and every instance of y with x. Typically we seem to use this operation when y is free, is there a situation we'd need it when x and y both appear in the expression?

  • I reviewed the concepts of renaming and substitution. I wonder if they can define each other as follows:

      forall e, forall fresh z, [ x ~> y ] e = [ z <~> y ] [ x <~> z ] e.

  forall e, forall fresh z, [ x <~> y ] e = [ z ~> y ] [ y ~> x ] [ x ~> z ] e.

    If yes, can all the properties of one operation derive from those of another?

Other questions about Chapter 4

  • PFPL Ch.4 discussed a lemma called “inversion for typing”, and it says:” In richer languages such inversion principles are more difficult to state and to prove.” What’s the example of such a “richer language”?

Other questions about Chapter 5

  • In the section of equational dynamics, the book mentioned that we can't prove n1 + n2 === n2 + n1 because of the lack of induction principle. Does the book here mean that we can't introduce an induction principle out of the equational reasoning rules? Why is this a challenge? And if so, why is it more difficult than introducing an induction principle for something like typing judgements that we developed earlier?

  • My question for the class is the advantages of using contextual dynamics over structural dynamics. The book says that all transitions in contextual dynamics are between complete programs. What does this mean? Moreover, what is the observable type?

  • Chapter 5 of PFPL spends a lot of time discussing equational dynamics. What's the advantage of stating things this way? The text states that we can determine the value of an expression using simplification and substitution, but this seems true of structural dynamics as well.

Questions about Coq

  1. In Coq, unlike Agda, there are functions and theorems. I think of both of them as the same. One possible advantage of having theorems might be that we don't need to write the arguments. But I noticed that at times Coq fails to infer them. So what's the use in having this distinction?

[SCW: The difference is just presentational. There is no real semantic difference between a Theorem/Lemma/Definition in Coq.]

  1. In Coq, I have not yet seen the bot type (contradiction). I find it harder to prove contradictions in the premises. Sometimes Coq forms terms in the premises which cannot be formed according to the definitions given and I can't figure out a way to tell Coq that these terms do not exist.

  2. The tactics in Coq are powerful. I could not yet fully understand their behaviour. Sometimes they are successful, sometimes they are not. I looked at the documentation online, but it's way too much of information. Also I found their behaviour to be non-linear, for example, induction H. auto. is not the same as induction H; auto. Can you suggest something in this regard?