Day 2

Made progress on outline.
Mostly, made progress on understanding the proof. I had only the idea behind the proof of NP-completeness before, working now on details. A few points are questionable:
1) A couple of sections end with "it is straightforward..." I shall have to figure out this "straightforward" conclusion to be able to present it. I suspect that absorbing the correlation between constraints and boolean formulas will give this intuition.
2) The translation from constraints to inference relies on different variables of the same name always having the same type. I suspect this is valid in their presentation but a huge liability of their type system. It will be interesting to see if removing this restriction makes type inference easier or harder, but probably that conclusion is way outside our scope.

This weekend I should be able to pick up the pace on working this out, but I put in a solid hour on this tonight.

--Carl