Conditional All-Paths

From Matching Logic
Jump to: navigation, search

Meeting notes:

A complexity in all paths reasoning is that you should only have to prove the goal is reached after applying rules in cases where they actually apply.

In the unconditional system the STEP rule has builds a logical expression for each rule containing an implication whose antecedent is false in any substitution where the LHS of the rule doesn't actually match the current pattern.

Extending this to conditional rules, we also have to somehow exclude the cases where the LHS does match but the condition cannot be satisfied.

It does not seem to be possible to transform rules so they apply whenever the LHS is satisfied - considering even an "if" in bin-step semantics, which has a different condition (evaluating the different possible bodies) depending whether the hypothesis is true or false. If you need a harder problem, a while loop in big-step semantics can take a step iff it terminates.

Maybe we can do first order logic with reachability assertions as atoms:

P_l => P_r if P_1 => P_1'

|- P_1 /\ F => P_1'
|- P_l /\ F => P_r /\ F 

~(P_l /\ F => P_r /\ F)
  \/ (P_1 /\ F => P_1')


forall FV (
  P_l => P_r if P1 => P1'

Schema (in C, P, P'):
forall RULES
forall FV (
  (exists c (P[c] /\ P_l[c])
  /\ (P1 =>[C] P1') /\ (P_r -> P'))
P ==>[C] P'
Personal tools