Skip to content

Latest commit

 

History

History
84 lines (64 loc) · 3.84 KB

090816.md

File metadata and controls

84 lines (64 loc) · 3.84 KB
Raw

Sept 8, 2016

  • Keep signing up for lecture topics!

  • Keep thinking off semester projects. Don't forget that you can work in groups!

  • Keep reading Ch4.v and start looking at the exercises in Ch5.v and Ch6.v. Also read PFPL chapters 4-6.

  • Don't forget to send questions before EACH class.

Questions

Other questions

  • I have been reading Chapter 3 and 4 of PFPL and found the same symbol ⊢ in both chapters, representing derivability judgement of statements and typing in language E. Is it an instance of Curry–Howard correspondence between derivations and typings?

  • I've often wanted to do something like "pick fresh x in L", "let x be ...", etc. But I haven't been sufficiently well-versed with the tactic language and CIC to go about doing it. Would you be going through this in class?

  • In the draft version of the book, in chapter 4.3, page 38, the author commented on the weakening lemma saying that from a programming point of view, the weakening property allows programmers to add new variables and it won't break the existing program. However, in the footnote, there were also comments about systems that don't obey the weakening property yet they are still useful. I am wondering what interesting capabilities that these substructural systems might have over systems that do obey the weakening property? It seems to be such a fundamental law for any programming language and I can't really think of cases where not having this property can be useful.

On top of that, it seems the weakening property, substitution property and the decomposition property together tells us that the simple language described in chapter 4 is type-safe. Are these the required properties for a language to have to be called type-safe? Can a language violate some of them yet still be called type-safe?

  • Homework exercise:

    Lemma subst_open : forall (x : atom) u e1 e2, lc u -> open ([x ~> u] e1) e2 = [x ~> u] (open e1 e2). Proof. (* EXERCISE *) Admitted.

    Say e2 = exp_fvar x, e1 = exp_bvar 0. So ([x ~> u]) e1 = e1 = exp_bvar 0. open ([x ~> u] e1) e2 = e2 = exp_fvar x. Again, (open e1 e2) = exp_fvar x. So [x ~> u] (open e1 e2) = u. Now exp_fvar x is not necessarily equal to u. How do we resolve this?

    [Answer: Good catch! The original version of the file had a bug. Do a git pull for the correct version. ]

  • In Ch4.v, you chose to use a list to represent the environment. Why did you choose list over other data structures? And in particular, why did you choose list over map? I haven’t tried using maps in this file (maybe I will), but maps look like a more natural representation: you don’t need to worry if it is uniq, and the order does not matter to it.

  • You state that "If we view typing contexts as ordered lists of typing assumptions, then the type system shown in section 4.2 of PFPL does NOT satisfy the weakening property" after the statement of weakening. I'm not quite sure what is meant by this. Does it mean that we can only use the types in the context in a certain order? What kind of type system does this describe?

  • In Ch4.v, the section about typing judgements has quite a few lemma whose proof would be difficult to go through if we state them in their natural form, and they are often generalized to a stronger version in order to guide Coq. However, this technique seems to require quite a lot of experience in navigating the design space of strengthening lemmas as there seems to be no hard and fast rule. Do you have some advice on how to identify a situation on where we might need a generalized theorem? And is there some heuristics that we may try when trying to generalize theorems?

  • I find that we use atom with free variables and nat with bounded variables. Are there situations in which using nat with free variables that are more useful than atom?