 |
CiteULike |  |
robertjohnsimmons's CiteULike | |
|
 Search
|
|
Register | |
Log in |  |
A "weakly extendable" property is a generalization of an invariant that still works well enough - it seems to capture the notion of an invariant that may be temporarily violated. The notion of observable program points doesn't quite seem as general as possible, but the assertions, that talk about pairs of observable program points, may be. However, now I see that the pairs are in two different programs that we want to show a correspondence between, so I'm unsure again.
Main interesting idea from my perspective: capture the nature of a procedure's effect on (global) state, and then ask decidable questions about the programs as decidable queries about the behavior of composed substitutions. The restriction they use for restoring satisfiability is that you can't have conditional statements within loops (!) You do get recursive calls, but they're restricted in a way (presumably a way that doesn't allow you to just simulate loops).
Main interesting idea from the presenter's (Ashish Tiwari) perspective: solving this new problem of equality or disequality of composed substitutions:
σ₅ʳ⁵⋯σ₁ʳ¹(x) ?= σ₅ˡ⁵⋯σ₁^ˡ¹(y)
By reducing the problem to Presburger arithmetic. A little more math than I actually followed, though.
I think this would be a good concertrg paper... It's a good survey of a lot of tools from topology as well as abstract interpretation. Also might be a good paper to try to get fm-rg to read.
ALTERNATIVE to predicate abstraction!
Argument is totally why Yogi works like it does: CEGAR involves lots and lots of theorem prover calls, try to do this much more simply, reuse the information from the proof that the trace is infeasible. They're using interpolants, which is different.
x := 0
y := 0
while(*) x++
assert(x != -1)
assert(y != -1)
This has the obvious control flow graph, a trace is just a word over this finite state automata. Now we've got three kinds of statements to consider:
Error traces are all FSA traces that respect the control flow of P. A feasible trace is one that makes sense for some program, but may not be the program you're dealing with! I have no idea why the feasible traces aren't required to respect the control flow.
At this point, I am relatively convinced that this is just a variant of the work I did at MSR that successfully incorporated interpolants, but the interpolant automata comes along with something actually novel. The canonical interpolant automata is the generalization of the error trace, and then some interesting automata intersection is happening.
This is maybe why I could never wrap my head around how to incorporate interporlants into a Yogi setting - rather than subtracting them against the program graph, we should really be unioning them (or suitable generalizations of them) together as a separate "abstracted forest" data structure. (Something similar to this is what they seem to mean by the rather strong claim that predicate abstraction is a special case of trace abstraction.)
This work on rewriting (separation logic) proofs to rewrite programs seems ripe to connect to some of the work on parallel evaluation of functional programs and the best-case scenarios for that parallel evaluation. The obvious generalization is that shared state can be parallelized when the race condition can be prevented with locks or optimistic concurrency.
Another interesting thing to think about - a lot of these act like rewrites that we do at a much, much lower level in the compiler. Is there virtue to doing it at the while-language level? Is there virtue to thinking about the compiler optimizations at this level?
Java+tom is a way of doing rewriting in Java; it sounds like it allows pattern matching against classes, which would be really nice. Apparently there is some delcacy as to how you want to reply rewrite rules, so I guess they are nondeterministic/not church-rosser. In the paper there is a discussion of optimizations that improve temporal locality, which is definitely intriguing.
His future work: OO-Programming, more loops, fractional permissions. The extension to loops is necessary to do appropriate "battle" with traditional optimizers. Apparently an issue is that the verifiers that exist aren't open source or aren't powerful enough, and he's not doing the verifying, just the manipulation of proof trees.
Yet another thought - the work done at POPL last year about scattershot do-all-optimizations optimizing might be good to integrate with this.
Resolution is a concept underlying much of both theorem proving and logic programming. It can be a little hard to connect the literature on resolution, which usually is highly classical, to literature that gives a proof theoretic perspective on logic programming and theorem proving (such as Pfenning's logic programming notes.) In this note, I'll attempt to connect these two perspectives a little more tightly.
In proof theory, polarity is a concept that means something different than what it means in the resolution literature. Therefore, we will avoid using the term polarity at all and instead use the terms supported and rejected from the resolution literature and left/right-asynchronous from the focusing literature.
In the resolution literature, polarity has to do with how many negations a formula is under, so in the formula `A ∧ ¬B ∧ ¬(C ∧ ¬(D ∧ ¬E))` `A`, `C`, and `E` appear under an even number of negations, whereas `B` and `D` appear under an odd number of negations.
In the focusing literature, polarity is a way of glomming together connectives to make bigger connectives; focusing captures the sense in which `A ∨ B ⇒ C` is really the same thing as `A ⇒ C ∧ B ⇒ C`, for instance.
In the end, we have some facts, and we want a proof or something. In classical logic, the goal seems to be always to form a contradiction, and therefore the facts are things we treat as true and the thing we want to prove is generally treated as false. In addition, there's a bit of a tendency to go ahead and treat conjunction ∧ as a commutative operator; we use a comma instead of a wedge for conjunction when we're emphasizing this fact.
Let's start with the following running set of facts, which we will use to try and prove `G`:
A, A ⇒ B, A ⇒ C, C ⇒ D, E ⇒ F, F ⇒ G, D ⇒ G
(In the future, I'll just call this `Γ₀` for short).
In classical logic, we are always only dealing with such a big puddle of facts, with the goal of making just one of those facts `FALSE`, which means that there is a contradiction. The fundamental assumption of inference (for us right now) is this: if I know `A ∨ B` is true, and I know `B` is false, then I know `A` must be true.
Remember that our goal is always to have a contradiction, so that our goal must be either to find a contradiction from `Γ₀ ∧ ¬G` or from `¬Γ₀ ∧ G`. The way we show a contradiction is always to show both `A` and `¬A`. Remember also that classical logic treats `A ⇒ B` as `¬A ∨ B`, and So my starting puddle would have to either look like this:
A ∧ (¬A ∨ B) ∧ (¬A ∨ C) ∧ (¬C ∨ D) ∧ (¬E ∨ F) ∧ (¬F ∨ G) ∧ (¬D ∨ G) ∧ ¬G
or like this:
[¬A ∨ (A ∧ ¬B) ∨ (A ∧ ¬C) ∨ (C ∧ ¬D) ∨ (E ∧ ¬F) ∨ (F ∧ ¬G) ∨ (D ∧ ¬G)] ∧ G
In the sequent calculus, instead of dealing with one big puddle of facts, we have some facts that are assumptions and one fact in particular that is the conclusion. The assumptions are generally called `Γ` and are to the left of a judgment stroke `⊢`: the sequent `Γ ⊢ C` means that the conclusion `C` is true under the assumptions `Γ`.
Our two primary rules are the following ones:
Γ, A ⇒ B ⊢ A
Γ, A ⇒ B, B ⊢ C
----------------- ⇒L ----------- init
Γ, A ⇒ B ⊢ C Γ, A ⊢ A
but notice that we can combine the two if B and C are the same to get the following:
Γ, A ⇒ B ⊢ A
-------------- infer
Γ, A ⇒ B ⊢ B
In our running example, then, our goal is to come up with a completed proof of the following sequent:
A, A ⇒ B, A ⇒ C, C ⇒ D, E ⇒ F, F ⇒ G, D ⇒ G ⊢ G
Note the oversimplification here; if we had a premise `A ⇒ B ⇒ C` then we could have a new version of the `infer` rule:
Γ, A ⇒ B ⇒ C ⊢ A
Γ, A ⇒ B ⇒ C ⊢ B
------------------ infer2
Γ, A ⇒ B ⇒ C ⊢ C
Both of these derived `infer` rules are what we get naturally out of focusing when we treat all atoms as being right-biased (i.e. right-asynchronous i.e. negative).
Take our starting puddle:
A ∧ (¬A ∨ B) ∧ (¬A ∨ C) ∧ (¬C ∨ D) ∧ (¬E ∨ F) ∧ (¬F ∨ G) ∧ (¬D ∨ G) ∧ ¬G
To do logic programming, we require that we match a rejected proposition with a conjunct that has an asserted occurance of that propsition. The only rejected proposition above is `¬G`, and it can only be matched with `¬F ∨ G` or `¬D ∨ G`. (A conjunct is one of the formulas that is linked together by conjunction `∧`.)
Without taking any missteps (and rearranging conjuncts for clarity) the resolution proof of our running example is
... (¬D ∨ G) ∧ ¬G
... (¬C ∨ D) ∧ ¬D ∧ ¬G
... (¬A ∨ C) ∧ ¬C ∧ ¬D ∧ ¬G
... A ∧ ¬A ∧ ¬C ∧ ¬D ∧ ¬G
In the last step we have `A` and `¬A`, a contradiction.
To do goal oriented logic programming in the sequent calculus, we always deal with partial proofs - proofs with pieces that aren't done yet.
So we start with the empty partial proof
-?-?-?-
Γ₀ ⊢ G
and then we use `infer` once to get
-?-?-?-
Γ₀ ⊢ D
------- infer
Γ₀ ⊢ G
and then we use `infer` two more times to get
-?-?-?-
Γ₀ ⊢ A
------- infer
Γ₀ ⊢ C
------- infer
Γ₀ ⊢ D
------- infer
Γ₀ ⊢ G
finally, we can conclude by using the hypothesis `A` and the `init` rule.
------- init
Γ₀ ⊢ A
------- infer
Γ₀ ⊢ C
------- infer
Γ₀ ⊢ D
------- infer
Γ₀ ⊢ G
We could make the opposite choice in resolution, only matching asserted propositions with conjuncts that have rejected versions of that proposition. Then our proof starts from the atomic proposition `A` and comes up with new asserted propositions until it asserts `G`, which contradicts `¬G`.
... (¬A ∨ C) ∧ A
... (¬C ∨ D) ∧ C ∧ A
... (¬D ∨ G) ∧ D ∧ C ∧ A
... ¬G ∧ G ∧ D ∧ C ∧ A
The equivalent operation in the sequent calculus results from using the inverse method, where you start with only proofs that can be immediately show to be true and then incrementally build the proof downwards. So the only starting point is a proof of `A`, which is already an assumption in `Γ₀`.
------- init
Γ₀ ⊢ A
Then we can use that to learn `Γ₀ ⊢ C`
Γ₀ ⊢ A
------- infer
Γ₀ ⊢ C
but we can also use it to prove `Γ₀ ⊢ B`.
Γ₀ ⊢ A
------- infer
Γ₀ ⊢ B
At this point, we have three sequents which we know to be true: `Γ₀ ⊢ A`, `Γ₀ ⊢ B`, and `Γ₀ ⊢ C`. In the same fashion we can learn `Γ₀ ⊢ D` and finally, `Γ₀ ⊢ G`, which is what we wanted to prove in the first place, so we are done.
