back to root

back to Matryoshka

Soundness theorems

• Jasmin Blanchette

  2020-04-21 12:33:9 (GMT)

  This email concerns pretty much all of @Alexander Bentkamp's paper, past and future.

  We now have more soundness or sat-preservation theorems than ever in our JAR submission and in our forthcoming LMCS submission, all (IIRC) thanks to Alex. This is great because soundness/sat-preservation is the most important property; just because it's relatively easy to prove doesn't mean we shouldn't prove it. And some of the proofs were actually quite tricky and led to fixes in the rules; at least, that was the case for $\lambda$-Sup.

  It occurred to me that our theorems aren't quite as strongly stated as they could or---I would argue---should. Namely, some of the side conditions of rules cannot be computed and must be approximated in an implementation. I'm thinking of e.g. the variable condition of the $\lambda$-free calculus.

  Thus, if one were to try to perform a refinement proof to connect the soundness of the calculus to the implementation, one would fail.

  Solution: State explicitly in the soundness theorems which side conditions are needed for soundness -- in effect, prove soundness of more general rules involving fewer side conditions. I'm not sure exactly what this would look like textually; maybe something like "Sup with side condition 1 only" or "Sup (with side condition~1)" or "Sup (without side conditions 2--9)".

  This would be cleaner and would also document which side conditions are necessary for soundness and which are there only to prune the search space.

  Opinions?

• Alexander Bentkamp

  2020-04-21 12:43:49 (GMT)

  Yes, let's do that. maybe we can write
  "Sup (even without side conditions 2--9)" or
  "The rule Sup is sound. This holds even if a subset of the side conditions 2 -- 9 is violated."

• Jasmin Blanchette

  2020-04-21 12:51:5 (GMT)

  I like Alex's first version ("even without"). We'd need to number all the side conditons (esp. in the $\lambda$-free article), but that's not a big deal.

• Jasmin Blanchette

  2020-04-21 12:51:28 (GMT)

  We can always write "(1) foo; (2) bar; (3) baz".

• Alexander Bentkamp

  2020-04-22 10:29:36 (GMT)

  Instead of naming all side conditions, we can easily describe them. In the $\lambda$-free paper none of the side conditions matter, except for the ones that say that $\sigma$ must be a unifier of the indicated terms.

• Jasmin Blanchette

  2020-04-22 10:46:44 (GMT)

  True, but you end up with an exception to an exception, e.g. "Sup (even without all side conditions except the one that says that signma must be a unifier of the indicated terms)". I still prefer "Sup (even without side conditions 2--7") I guess. Or maybe there's another way, e.g. "(even without the ordering side conditions)".

• Alexander Bentkamp

  2020-04-22 11:22:46 (GMT)

  "(even without the side conditions on ordering and eligibility)"?

• Alexander Bentkamp

  2020-04-22 11:26:45 (GMT)

  and the variable condition is not necessary either...

• Alexander Bentkamp

  2020-04-22 13:20:50 (GMT)

  So I would propose: "(even without the variable condition and the side conditions on ordering and eligibility)". This way we avoid to get too technical about something that is very intuitive.

• Alexander Bentkamp

  2020-04-23 7:49:57 (GMT)

  In the JAR submission, it's a bit more complicated. I wrote:

  (even without the variable condition and the side conditions on fluidity, deep variables, ordering, and eligibility)