From 4f6a15155a736ef800bc9bcc93ef49f2726f00cd Mon Sep 17 00:00:00 2001 From: Traian-Florin Serbanuta Date: Tue, 12 Apr 2022 16:44:32 +0300 Subject: [PATCH 1/9] Sketch of Full correctness algorithm --- ...Corectness-All-Path-Reachability-Proofs.md | 389 ++++++++++++++++++ 1 file changed, 389 insertions(+) create mode 100644 docs/2022-04-07-Full-Corectness-All-Path-Reachability-Proofs.md diff --git a/docs/2022-04-07-Full-Corectness-All-Path-Reachability-Proofs.md b/docs/2022-04-07-Full-Corectness-All-Path-Reachability-Proofs.md new file mode 100644 index 0000000000..3ec0341f2d --- /dev/null +++ b/docs/2022-04-07-Full-Corectness-All-Path-Reachability-Proofs.md @@ -0,0 +1,389 @@ +Proving Full Correctness All-Path Reachability Claims +===================================================== + +This document details Full Correctness All-Path Reachability without solving the +most-general-unifier (MGU) problem. +MGU will be detailed in a separate document. + +_Prepared by Traian Șerbănuță, based on [proving All-Path Reachability +claims](2019-03-28-All-Path-Reachability-Proofs.md)_ + +Background +---------- + +Similarly to the All-Path Reachability document, we assume all pattern variables +used in this document to be _extended function-like patterns_, that is patterns +which can be written as `t ∧ p` where the interpretation of `t` contains at most +one element and `p` is a predicate. + +_Extended constructor patterns_ will be those extended function-like patterns +for which `t` is a functional term, composed out of constructor-like symbols +and variables. + + +__Note:__ +Whenever `φ` is a function-like pattern, +``` +φ ∧ ∃z.ψ = φ ∧ ∃z.⌈φ ∧ ψ⌉ +``` +and +``` +φ ∧ ¬∃z.ψ = φ ∧ ¬∃z.⌈φ ∧ ψ⌉ +``` + +In this document we prefer the formulations on the right because they are of the +form pattern and predicate. + +Moreover, suppose all free variables in the above formulae are from `x`, +we will assume that the unification condition `⌈φ ∧ ψ⌉` can always be +computed to be of the form `z = t ∧ p`, where + +* `t`s are functional patterns with no free variables from `z` + * i.e., `[t / z]` is a substitution. +* `p` is a predicate over `x ∪ z` + +Under this assumption, `∃z.⌈φ ∧ ψ⌉` can be rewritten without the existential +quantification, as `p[t/z]`, i.e., `p` in which all ocurrences of the variables +from `z` are substituted with the corresponding term in `t`. + + +Definitions +----------- + +### All-path finally + +Given a formula `φ`, let `♢φ` denote the formula “all-path finally” `φ`, +defined by: + +``` +♢φ := μX.φ ∨ (○X ∧ •⊤) +``` + +one consequence of the above is that `♢φ ≡ φ ∨ (○♢φ ∧ •⊤)`. + +Given this definition of all-path finally, a full correctness all-path +reachability claim +``` +∀x.φ(x) → ♢∃z.ψ(x,z) +``` +basically states that if `φ(x)` holds for a configuration `γ`, for some `x`, +then `P(γ)` holds, where `P(G)` is recursively defined on configurations as: +* there exists `z` such that `ψ(x,z)` holds for `G` +* or + * `G` is not stuck (`G → • T`) and + * `P(G')` for all configurations `G'` in which `G` can transition + +__Note:__ +Using the least fix-point (`μ`) instead of the greatest fix-point (`ν`) +restricts paths to finite ones. Therefore, the intepretation of a reachability +claim guarantees full-correctness, as it requires that the conclusion is +reached in a finite number of steps. + +Problem Description +------------------- + +Given a set of reachability claims, of the form `∀x.φ(x) → ♢∃z.ψ(x,z)`, +we are trying to prove all of them together. + +### Additional complication + +Since proving a claim now also needs to guarantee termination, there are several +extra requirements, as applications of circularities would now need to be +guarded by a measure of decreasingness instead of a measure of progress +(switching from coinduction to induction). + +## Proposal of syntax changes to address the above mentioned complication + +- claims need to mention the other claims (including themselves) which are + needed to complete their proof; this induces a dependency relation +- claims which are part of a dependency cycle (including self-dependencies) + would need to be specified together as a "claim group" +- a claim group would need to provide a metric on their input variables, which + would be used as part of the decreasingness guard whenever one tries to apply + a claim from the group during the proof of one the claims in the group + +A claim group would be something like +``` +claim group + decreasing measure(x) + + . . . + + claim φᵢ(x) → ♢∃zᵢ.ψᵢ(x,zᵢ) [using(claimᵢ₁, ..., claimᵢₖ)] + + . . . + +end claim group +``` + +where the claims in the `using` mention the dependencies which are not part of +the cycle. + +## Algorithms +------------- +(detailed in the next section) + + +### Algorithm `proveAllPath` + +__Input:__ claim group `∀x. (φ₁(x) → ♢∃z.ψ₁(x,z)) ∧ ... ∧ (φₙ(x) → ♢∃z.ψₙ(x,z)) [decreasing measure(x)]` + +__Output:__ Proved or Unproved + +* Fix an instance `x₀` for the variables `x` +* Let `claims ::= { ∀ x . φᵢ(x) ∧ measure(x) =Int 0` + * Let `claimsᵢ ::= claims ∪ { claimᵢ₁, ..., claimᵢₖ }` + * Let `Goals := { φᵢ(x₀) }` + * While `Goals` is not empty: + * Extract and remove `goal` of the form `φ` from `Goals` + * Let `goalᵣₑₘ := φ ∧ ¬∃z.⌈φ ∧ ψᵢ⌉` + * If `goalᵣₑₘ` is bottom (`goalᵣₑₘ ≡ ⊥`) + * continue to the next goal + * `(Goals', goal'ᵣₑₘ) := derivePar(goalᵣₑₘ, claimsᵢ)` + * Let `(Goals'', goal''ᵣₑₘ) := derivePar(goal'ᵣₑₘ, axioms)` + * If `goal''ᵣₑₘ` is not trivially valid (its lhs is not equivalent to `⊥`) + * Return `Unprovable` + * Let `Goals := Goals ∪ Goals' ∪ Goals''` +* Return `Provable` + +__Note:__ Since the derivation process can continue indefinitely, one could add +a bound on the total number of (levels of) expansions attempted before +returning `Unprovable`. + +__Note__: If the unfication condition `⌈φ ∧ ψ⌉ = (z=t)∧ p` +with `t` functional, `p` predicate, and `t` free of `z`. +Then `goalᵣₑₘ := φ ∧ ¬∃z.⌈φ ∧ ψ⌉` +is equivalent to `φ ∧ ¬pᵢ[tᵢ/xᵢ]`. + +### Algorithm `derivePar` + +__Input:__: goal `φ` and set of tuples `{ (xᵢ,φᵢ,zᵢ,ψᵢ) : 1 ≤ i ≤ n }` representing either + +* claims `{ ∀xᵢ.φᵢ → ♢∃zᵢ.ψᵢ : 1 ≤ i ≤ n }`, or +* axioms `{ ∀xᵢ.φᵢ → •∃zᵢ.ψᵢ : 1 ≤ i ≤ n }` + +__Output:__ `(Goals, goalᵣₑₘ)` + +* Let `goalᵣₑₘ := φ ∧ ¬∃x₁.⌈φ∧φ₁⌉ ∧ … ∧ ¬∃xₙ.⌈φ∧φₙ⌉` +* Let `Goals := { ∀z₁.(∃x₁.ψ₁ ∧ ⌈φ∧φ₁⌉), … , ∀zₙ.(∃xₙ.ψₙ ∧ ⌈φ∧φₙ⌉) }` + +__Note__: `∀zᵢ.(∃xᵢ.ψᵢ ∧ ⌈φ∧φᵢ⌉)` is obtained from +`(∃xᵢ.(∃zᵢ.ψᵢ) ∧ ⌈φ∧φᵢ⌉) → ♢∃z.ψ` + +__Note__: If the unfication condition `⌈φ ∧ φᵢ⌉ = (xᵢ=tᵢ)∧ pᵢ` +with `tᵢ` functional, `pᵢ` predicate, and `tᵢ` free of `xi`. +Then the goal `∀x∪zᵢ.(∃xᵢ.ψᵢ ∧ ⌈φ∧φᵢ⌉) → ♢∃z.ψ` +is equivalent to `∀x∪zᵢ.ψᵢ[tᵢ/xᵢ] ∧ pᵢ[tᵢ/xᵢ] → ♢∃z.ψ`. + +Similarly `goalᵣₑₘ := (φ ∧ ¬∃x₁.⌈φ∧φ₁⌉ ∧ … ∧ ¬∃xₙ.⌈φ∧φₙ⌉)` +is equivalent to `(φ ∧ ⋀ⱼ ¬pⱼ[tⱼ/xⱼ])` +where `j` ranges over the set `{ i : 1 ≤ i ≤ n, φ unifies with φᵢ }`. + +__Note__: If `φ` does not unify with `φᵢ`, then `⌈φ∧φᵢ⌉ = ⊥`, hence +the goal `∀x∪zᵢ.(∃xᵢ.ψᵢ ∧ ⌈φᵢʳᵉᵐ∧φᵢ⌉) → ♢∃z.ψ` is equivalent to +`∀x.⊥ → ♢∃z.ψ` which can be discharged immediately. Also, in the +remainder `¬∃x₁.⌈φ∧φ₁⌉ = ⊤` so the conjunct can be removed. + + +Explanation +----------- + +Say we want to prove `∀x. (φ₁(x) → ♢∃z.ψ₁(x,z)) ∧ ... ∧ (φₙ(x) → ♢∃z.ψₙ(x,z)) [decreasing measure(x)]`. + +We will do that by well-founded induction over `measure(x)`. +To do that, we would need to ensure that `measure(x)` is always positive; +this could be checked either syntactically, or using the SMT. + +Fix an arbitrary instance `x₀` of the variables. We have to prove each +reachability claim `φᵢ(x₀) → ♢∃z.ψᵢ(x₀,z)`, using the induction hypothesis +`∀x. measure(x) < measure(x₀) → (φ₁(x) → ♢∃z.ψ₁(x,z)) ∧ ... ∧ (φₙ(x) → ♢∃z.ψₙ(x,z))` +which can be split into induction hypotheses for each claim +`∀x. φᵢ(x) ∧ measure(x) < measure(x₀) → ♢∃z.ψᵢ(x,z)`. + +Since we might be using the claims to advance the proof of the claim, to avoid +confusion (and to reduce caring about indices) we will denote a goal with +`φ(x₀) → ♢∃z.ψ(x₀,z)` in all subsequent steps, although the exact goal might +change from one step to the next. + +### Eliminating the conclusion + +First, let us eliminate the case when the conclusion holds now. We have +the following sequence of equivalent claims: + +``` +φ(x₀) → ♢∃z.ψ(x₀,z) +φ(x₀) ∧ (∃z.ψ(x₀, z) ∨ ¬∃z.ψ(x₀, z)) → ♢∃z.ψ(x₀,z) +(φ(x₀) ∧ ∃z.ψ(x₀, z)) ∨ (φ(x₀) ∧ ¬∃z.ψ(x₀, z)) → ♢∃z.ψ(x₀,z) +(φ(x₀) ∧ ∃z.ψ(x₀, z) → ♢∃z.ψ(x₀,z)) ∧ (φ(x₀) ∧ ¬∃z.ψ(x₀, z) → ♢∃z.ψ(x₀,z)) +``` + +The first conjunct, `φ(x₀) ∧ ∃z.ψ(x₀, z) → ♢∃z.ψ(x₀,z)` can be discharged by +unrolling `♢∃z.ψ(x₀,z)` to `∃z.ψ(x₀,z) φ ∨ (○♢∃z.ψ(x₀,z) ∧ •⊤)`, and then +using that `∃z.ψ(x₀, z)` appears in both lhs (as a conjunct) and rhs (as a +disjunct). + +This reduces the above to proving the following remainder claim: + +```` +φ(x₀) ∧ ¬∃z.ψ(x₀, z) → ♢∃z.ψ(x₀,z) +``` + +Let `φ(x₀)` denote `φ(x₀) ∧ ¬(∃z.ψ(x₀, z))` in the sequel. +If `φ(x₀)` is equivalent to `⊥`, then the implication holds and we are done. + +### Applying circularities (induction hypotheses) + +To apply circularities we have to ensure that the measure has decreased. +However, whenever circularities may be applied, we want to apply them +immediately (to allow skipping over loops/recursive calls), and to only apply +regular rules on the parts on which circularities cannot apply. + +On the other hand, care should be taken when choosing the measure, to ensure +it actually holds whenever one needs to reenter a loop/call a recursive +function. Failing to have a good such measure would result in the circularities +never being applied and the proof looping (and branching) forever. + +In the following, let `∀x.φᵢ(x) → ♢∃z.ψᵢ(x,z)` denote the ith induction +hypothesis, with `φᵢ(x)` including the `measure(x) < measure(x₀)` check. + +``` +φ(x₀) → ♢∃z.ψ(x₀,z) +φ(x₀) ∧ (∃x.φ₁(x) ∨ … ∨ ∃x.φₙ(x) ∨ (¬∃x.φ₁(x) ∧ … ∧ ¬∃x.φₙ(x)) → ♢∃z.ψ(x₀,z) +(φ(x₀) ∧ ∃x.φ₁(x)) ∨ … ∨ (φ(x₀) ∧ ∃x.φₙ(x)) ∨ (φ(x₀) ∧ (¬∃x.φ₁(x) ∧ … ∧ ¬∃x.φₙ(x))) → ♢∃z.ψ(x₀,z) +(φ(x₀) ∧ ∃x.φ₁(x) → ♢∃z.ψ(x₀,z)) ∧ … (φ(x₀) ∧ ∃x.φₙ(x) → ♢∃z.ψ(x₀,z)) ∧ (φ(x₀) ∧ (¬∃x₁.φ₁ ∧ … ∧ ¬∃xₙ.φₙ)) → ♢∃z.ψ(x₀,z)) +``` + +Note that the remainder can be rewritten using the following equivalences: + +``` +φ(x₀) ∧ (¬∃x.φ₁(x) ∧ … ∧ ¬∃x.φₙ(x)) → ♢ψ(x₀,z) +(φ(x₀) ∧ ¬∃x.φ₁(x)) ∧ … ∧ (φ(x₀) ∧ ¬∃x.φₙ(x)) → ♢ψ(x₀,z) +(φ(x₀) ∧ ¬∃x.⌈φ(x₀) ∧ φ₁(x)⌉) ∧ … ∧ (φ(x₀) ∧ ¬∃x.⌈φ(x₀)∧φₙ(x)⌉) → ♢ψ(x₀,z) +φ(x₀) ∧ (¬∃x.⌈φ(x₀) ∧ φ₁(x)⌉ ∧ … ∧ ¬∃x.⌈φ(x₀)∧φₙ(x)⌉) → ♢ψ(x₀,z) +``` + +In particular, part of the predicate of the remainder will include the negation +of the measure check, `¬measure(x) < measure(x₀)` instantiated with the +substitution associated with any term part of some `φᵢ(x)` matching `φ(x₀)`. + +#### Using a claim to advance the corresponding goal + +We want to prove that from the induction hypothesis `∀x. φᵢ(x) → ♢∃z.ψᵢ(x,z)` +and the derived goal `∀zᵢ.∃x.(ψᵢ(x,zᵢ) ∧ ⌈φ(x₀) ∧ φᵢ(x)⌉) → ♢∃z.ψ(x₀, z)` +we can deduce that `φ(x₀) ∧ ∃x.φᵢ(x) → ♢∃z.ψ(x₀,z)`. + +This would allow us to replace goal `φ(x₀) ∧ ∃x.φᵢ(x) → ♢∃z.ψ(x₀,z)` +with goal `∀zᵢ.∃x.(ψᵢ(x,zᵢ) ∧ ⌈φ(x₀) ∧ φᵢ(x)⌉) → ♢∃z.ψ(x₀,z)`. + +_Proof:_ + +The main step of our proof is to prove +`φ(x₀) ∧ ∃x.φᵢ(x) → ♢∃x.((∃zᵢ.ψᵢ(x,z)) ∧ ⌈φ(x₀) ∧ φᵢ(x)⌉)` +from `∀x. φᵢ(x) → ♢∃z.ψᵢ(x,z)`. + +Assume `⌈φ(x₀) ∧ φᵢ(x)⌉ = (x=tᵢ(x₀))∧ pᵢ(x, x₀)` with `tᵢ(x₀)` functional and +free of `x` and `pᵢ(x₀,x)` predicate. + +Then, +``` +φᵢ(tᵢ) → ♢∃z.ψᵢ(tᵢ, z) // by induction hypothesis ∀x.φᵢ(x) → ♢∃z.ψᵢ(x,z) instantiated to x := tᵢ +φᵢ(tᵢ) ∧ p(x₀,tᵢ) → (♢∃z.ψᵢ(tᵢ, z)) ∧ p(x₀,tᵢ) // framing +φᵢ(tᵢ) ∧ p(x₀,tᵢ) → ♢((∃z.ψᵢ(tᵢ, z)) ∧ p(x₀,tᵢ)) // predicate properties +∃x.φᵢ(x) ∧ x=tᵢ ∧ p(x₀,x) → ♢∃x.((∃z.ψᵢ(x,z)) ∧ x=tᵢ ∧ p(x₀,x)) // substitution properties +∃x.φᵢ(x) ∧ ⌈φ(x₀)∧φᵢ(x)⌉ → ♢∃x.((∃z.ψᵢ(x,z)) ∧ ⌈φ(x₀)∧φᵢ(x)⌉) // definition of ⌈φ(x₀)∧φᵢ(x)⌉ +φ(x₀) ∧ ∃x.φᵢ(x) ∧ ⌈φ(x₀)∧φᵢ(x)⌉ → ♢∃x.((∃z.ψᵢ(x,z)) ∧ ⌈φ(x₀)∧φᵢ(x)⌉) // Strengthening +φ(x₀) ∧ ∃x.⌈φ(x₀) ∧ φᵢ(x) ∧ ⌈φ(x₀)∧φᵢ(x)⌉⌉ → ♢∃x.((∃z.ψᵢ(x,z)) ∧ ⌈φ(x₀)∧φᵢ(x)⌉) // φ is functional +φ(x₀) ∧ ∃x.(⌈φ(x₀) ∧ φᵢ(x)⌉ ∧ ⌈φ(x₀)∧φᵢ(x)⌉) → ♢∃x.((∃z.ψᵢ(x,z)) ∧ ⌈φ(x₀)∧φᵢ(x)⌉) // predicate properties +φ(x₀) ∧ ∃x.⌈φ(x₀) ∧ φᵢ(x)⌉ → ♢∃x.((∃z.ψᵢ(x,z)) ∧ ⌈φ(x₀)∧φᵢ(x)⌉) // idempotency +φ(x₀) ∧ ∃x.φᵢ(x) → ♢∃x.((∃z.ψᵢ(x,z)) ∧ ⌈φ(x₀)∧φᵢ(x)⌉) // φ is functional +``` + +#### Summary of applying circularities + +By applying the circularities, we will replace the existing goal with a set +consisting of a goal for each circularity (some with the hypothesis equivalent +with `⟂`) and a remainder. + +For a given induction hypothesis ``∀x. φᵢ(x) → ♢∃z.ψᵢ(x,z)`, +since `φ(x₀)` and `φᵢ(x)` are both function-like patterns (constrained terms), +we can assume that `⌈φ(x₀) ∧ φᵢ(x)⌉` can be written of the form +`(x=tᵢ(x₀)) ∧ pᵢ(x, x₀)` with `tᵢ(x₀)` functional and free of `x` and +`pᵢ(x₀,x)` a predicate (which can be bottom to account for unification failure). + +Then the derived goal associated to this induction hypothesis will be +`∀zᵢ.∃x.(ψᵢ(x,zᵢ) ∧ ⌈φ(x₀) ∧ φᵢ(x)⌉) → ♢∃z.ψ(x₀,z)`, which, using the above +identity, is equivalent to + +``` +∀zᵢ.∃x.(ψᵢ(x,zᵢ) ∧ (x=tᵢ(x₀)) ∧ pᵢ(x, x₀)) → ♢∃z.ψ(x₀,z) +∀zᵢ.∃x.(ψᵢ(tᵢ(x₀),zᵢ) ∧ pᵢ(tᵢ(x₀), x₀)) → ♢∃z.ψ(x₀,z) +∀zᵢ.ψᵢ(tᵢ(x₀),zᵢ) ∧ pᵢ(tᵢ(x₀), x₀) → ♢∃z.ψ(x₀,z) +``` + +Using the fact that the variables `zᵢ` only appear in the lhs, we can +instantiate them to arbitrary (but fixed) symbolic variables `z₀`, and then +let `φ(x₀)` denote ψᵢ(tᵢ(x₀),z₀) ∧ pᵢ(tᵢ(x₀), x₀)` for the next phase of the +algorithm. + + +### Applying axioms + +We're back now to `φ(x₀) → (○♢∃z.ψ(x₀,z)) ∧ •⊤`, which is equivalent to +`(φ(x₀) → ○♢∃z.ψ(x₀, z)) ∧ (φ(x₀) → •⊤)` + +Therefore we need to check two things: + +1. That `φ(x₀)` is not stuck +1. That `φ(x₀) → ○♢∃z.ψ` + +Assume `∀xᵢ.φᵢ(xᵢ) → •∃zᵢ.ψᵢ(xᵢ,zᵢ), 1 ≤ i ≤ n` are all the one-step axioms +in the definition, and `P -> o ⋁ᵢ ∃xᵢ.⌈P ∧ φᵢ(xᵢ)⌉ ∧ ∃zᵢ.ψᵢ(xᵢ,zᵢ)` +is the STEP rule associated to them. + +Using the same reasoning as when applying all claims in parallel, +`φ(x₀) → α` is equivalent with +``` +(φ(x₀) ∧ ∃x₁.φ₁(x₁) → α) ∧ … ∧ (φ(x₀) ∧ ∃xₙ.φₙ(xₙ) → α) ∧ (φ(x₀) ∧ ¬∃x₁.φ₁(x₁) ∧ … ∧ ¬∃xₙ.φₙ(xₙ) → α) +``` + +Now, for the first thing to check, take `α := •⊤`. +Since all but the last conjunct are guaranteed to hold +(because of the rewrite axioms), `φ` is stuck if the remainder after attempting +to apply all axioms (i.e., the lhs of the last conjunct) is not equivalent to `⊥`. + +We want to prove that from the STEP rule and +``` +(∀z₁.∃x₁.ψ₁(x₁,z₁) ∧ ⌈φ(x₀) ∧ φ₁(x₁)⌉ → ♢∃z.ψ(x₀,z)) ∧ … ∧ (∀zₙ.∃xₙ.ψₙ(xₙ,zₙ) ∧ ⌈φ(x₀) ∧ φₙ(xₙ)⌉ → ♢∃z.ψ(x₀,z)) +``` + +we can derive `φ(x₀) → ○♢∃z.ψ(x₀,z)` + +This would allow us to replace the goal `φ(x₀) → ○♢∃z.ψ(x₀,z)` with the set of goals +``` +{ ∀zᵢ.∃xᵢ.ψᵢ(xᵢ,zᵢ) ∧ ⌈φ(x₀) ∧ φᵢ(xᵢ)⌉ → ♢∃z.ψ(x₀,z) : 1 ≤ i ≤ n } +``` + +_Proof:_ + +Apply `(STEP)` on `φ(x₀)`, and we obtain that +``` +φ(x₀) → o ⋁ᵢ ∃xᵢ.⌈φ(x₀) ∧ φᵢ(xᵢ)⌉ ∧ ∃zᵢ.ψᵢ(xᵢ,zᵢ) +``` + +We can replace our goal succesively with: +``` +o ⋁ᵢ ∃xᵢ.⌈φ(x₀) ∧ φᵢ(xᵢ)⌉ ∧ ∃zᵢ.ψᵢ(xᵢ,zᵢ) → ○♢∃z.ψ(x₀, z) // transitivity of → +⋁ᵢ ∃xᵢ.⌈φ(x₀) ∧ φᵢ(xᵢ)⌉ ∧ ∃zᵢ.ψᵢ(xᵢ,zᵢ) → ♢∃z.ψ(x₀, z) // framing on ○ +∃xᵢ.⌈φ(x₀) ∧ φᵢ(xᵢ)⌉ ∧ ∃zᵢ.ψᵢ(xᵢ,zᵢ) → ♢∃z.ψ(x₀, z) for all i +``` + +#### Summary of applying the claims + +- Check that the remainder `φ(x₀) ∧ ¬∃x₁.φ₁(x₁) ∧ … ∧ ¬∃xₙ.φₙ(xₙ)` is equivalent to `⟂` +- Replace the goal `φ(x₀) → ○♢∃z.ψ(x₀,z)` by the set of goals + ``` + { ∀zᵢ.∃xᵢ.ψᵢ(xᵢ,zᵢ) ∧ ⌈φ(x₀) ∧ φᵢ(xᵢ)⌉ → ♢∃z.ψ(x₀,z) : 1 ≤ i ≤ n } + ``` + From ae8c6735f70c272ced43b83505cec50b35079c9b Mon Sep 17 00:00:00 2001 From: Traian-Florin Serbanuta Date: Thu, 14 Apr 2022 15:10:40 +0300 Subject: [PATCH 2/9] Some updates --- ...Corectness-All-Path-Reachability-Proofs.md | 421 +++++++++--------- 1 file changed, 222 insertions(+), 199 deletions(-) diff --git a/docs/2022-04-07-Full-Corectness-All-Path-Reachability-Proofs.md b/docs/2022-04-07-Full-Corectness-All-Path-Reachability-Proofs.md index 3ec0341f2d..82129870fb 100644 --- a/docs/2022-04-07-Full-Corectness-All-Path-Reachability-Proofs.md +++ b/docs/2022-04-07-Full-Corectness-All-Path-Reachability-Proofs.md @@ -8,45 +8,6 @@ MGU will be detailed in a separate document. _Prepared by Traian Șerbănuță, based on [proving All-Path Reachability claims](2019-03-28-All-Path-Reachability-Proofs.md)_ -Background ----------- - -Similarly to the All-Path Reachability document, we assume all pattern variables -used in this document to be _extended function-like patterns_, that is patterns -which can be written as `t ∧ p` where the interpretation of `t` contains at most -one element and `p` is a predicate. - -_Extended constructor patterns_ will be those extended function-like patterns -for which `t` is a functional term, composed out of constructor-like symbols -and variables. - - -__Note:__ -Whenever `φ` is a function-like pattern, -``` -φ ∧ ∃z.ψ = φ ∧ ∃z.⌈φ ∧ ψ⌉ -``` -and -``` -φ ∧ ¬∃z.ψ = φ ∧ ¬∃z.⌈φ ∧ ψ⌉ -``` - -In this document we prefer the formulations on the right because they are of the -form pattern and predicate. - -Moreover, suppose all free variables in the above formulae are from `x`, -we will assume that the unification condition `⌈φ ∧ ψ⌉` can always be -computed to be of the form `z = t ∧ p`, where - -* `t`s are functional patterns with no free variables from `z` - * i.e., `[t / z]` is a substitution. -* `p` is a predicate over `x ∪ z` - -Under this assumption, `∃z.⌈φ ∧ ψ⌉` can be rewritten without the existential -quantification, as `p[t/z]`, i.e., `p` in which all ocurrences of the variables -from `z` are substituted with the corresponding term in `t`. - - Definitions ----------- @@ -83,16 +44,14 @@ Problem Description ------------------- Given a set of reachability claims, of the form `∀x.φ(x) → ♢∃z.ψ(x,z)`, -we are trying to prove all of them together. - -### Additional complication +we are trying to prove all of them together, by well-founded induction on a +given `measure` defined on the quantified variables `x`. -Since proving a claim now also needs to guarantee termination, there are several -extra requirements, as applications of circularities would now need to be -guarded by a measure of decreasingness instead of a measure of progress -(switching from coinduction to induction). +The well-founded induction argument requiring the `measure` to decrease before +applying a claim as a circularity replaces the coinductive argument requiring +that progress is made before applying a circularity. -## Proposal of syntax changes to address the above mentioned complication +## Proposal of syntax changes - claims need to mention the other claims (including themselves) which are needed to complete their proof; this induces a dependency relation @@ -115,97 +74,107 @@ claim group end claim group ``` +where the claims referred to by the `using` attribute mention dependencies which +are not part of the cycle. -where the claims in the `using` mention the dependencies which are not part of -the cycle. +TODO(virgil): wouldn't it work to use the existing module syntax? +if so, `import` statements could replace `using` attributed. +Still, syntax for `decreasing` statements, and accounting for sharing the +variables would need to be implemented. -## Algorithms -------------- -(detailed in the next section) +## Approach +For the algorithms derived by the present approach, please see next section. -### Algorithm `proveAllPath` +Assume we want to prove a group of claims defined over the same set of variables +`x`. Further assume that all claims not in group on which these claims depend +have already been proven. Assume also a given integer pattern `measure(x)`, +over the same variables as the claims in the group. -__Input:__ claim group `∀x. (φ₁(x) → ♢∃z.ψ₁(x,z)) ∧ ... ∧ (φₙ(x) → ♢∃z.ψₙ(x,z)) [decreasing measure(x)]` +Since we're proving all claims together, we can gather them in a single goal, +`P(x) ::= (φ₁(x) → ♢∃z.ψ₁(x,z)) ∧ ... ∧ (φₙ(x) → ♢∃z.ψₙ(x,z))`. -__Output:__ Proved or Unproved +A well-founded induction principle allowing to prove `P` using `measure` would +be of the form -* Fix an instance `x₀` for the variables `x` -* Let `claims ::= { ∀ x . φᵢ(x) ∧ measure(x) =Int 0` - * Let `claimsᵢ ::= claims ∪ { claimᵢ₁, ..., claimᵢₖ }` - * Let `Goals := { φᵢ(x₀) }` - * While `Goals` is not empty: - * Extract and remove `goal` of the form `φ` from `Goals` - * Let `goalᵣₑₘ := φ ∧ ¬∃z.⌈φ ∧ ψᵢ⌉` - * If `goalᵣₑₘ` is bottom (`goalᵣₑₘ ≡ ⊥`) - * continue to the next goal - * `(Goals', goal'ᵣₑₘ) := derivePar(goalᵣₑₘ, claimsᵢ)` - * Let `(Goals'', goal''ᵣₑₘ) := derivePar(goal'ᵣₑₘ, axioms)` - * If `goal''ᵣₑₘ` is not trivially valid (its lhs is not equivalent to `⊥`) - * Return `Unprovable` - * Let `Goals := Goals ∪ Goals' ∪ Goals''` -* Return `Provable` - -__Note:__ Since the derivation process can continue indefinitely, one could add -a bound on the total number of (levels of) expansions attempted before -returning `Unprovable`. - -__Note__: If the unfication condition `⌈φ ∧ ψ⌉ = (z=t)∧ p` -with `t` functional, `p` predicate, and `t` free of `z`. -Then `goalᵣₑₘ := φ ∧ ¬∃z.⌈φ ∧ ψ⌉` -is equivalent to `φ ∧ ¬pᵢ[tᵢ/xᵢ]`. +``` + forall x0, (forall x, 0 <= measure(x) < measure(x0) -> P(x)) -> P(x0) + --------------------------------------------------------------------- + forall x, P(x) +``` -### Algorithm `derivePar` +By the above induction principle, to prove `forall x, P(x)` it suffices to prove +`forall x0, (forall x, 0 <= measure(x) < measure(x0) -> P(x)) -> P(x0)` -__Input:__: goal `φ` and set of tuples `{ (xᵢ,φᵢ,zᵢ,ψᵢ) : 1 ≤ i ≤ n }` representing either +Fixing an arbitrary instance `x₀` of the variables and assuming the induction +hypothesis `forall x, 0 <= measure(x) < measure(x0) -> P(x)`, we need to prove +`P(x₀)`. -* claims `{ ∀xᵢ.φᵢ → ♢∃zᵢ.ψᵢ : 1 ≤ i ≤ n }`, or -* axioms `{ ∀xᵢ.φᵢ → •∃zᵢ.ψᵢ : 1 ≤ i ≤ n }` +By first-order manipulation we can transform the induction hypothesis for `P` +into a set of induction hypotheses, one for each claim: +``` +∀x. φᵢ(x) ∧ 0 ≤ measure(x) < measure(x₀) → ♢∃z.ψᵢ(x,z) +``` -__Output:__ `(Goals, goalᵣₑₘ)` +Similarly we can split the goal into a separate goal `φᵢ(x₀) → ♢∃z.ψᵢ(x₀,z)` +for each claim. -* Let `goalᵣₑₘ := φ ∧ ¬∃x₁.⌈φ∧φ₁⌉ ∧ … ∧ ¬∃xₙ.⌈φ∧φₙ⌉` -* Let `Goals := { ∀z₁.(∃x₁.ψ₁ ∧ ⌈φ∧φ₁⌉), … , ∀zₙ.(∃xₙ.ψₙ ∧ ⌈φ∧φₙ⌉) }` +Since we might be using the claims to advance the proof of the claim, to avoid +confusion (and to reduce caring about indices) we will denote a goal with +`φ(x₀) → ♢∃z.ψ(x₀,z)` in all subsequent steps, although the exact goal might +change from one step to the next. -__Note__: `∀zᵢ.(∃xᵢ.ψᵢ ∧ ⌈φ∧φᵢ⌉)` is obtained from -`(∃xᵢ.(∃zᵢ.ψᵢ) ∧ ⌈φ∧φᵢ⌉) → ♢∃z.ψ` +Moreover, we will consider the induction hypotheses to be derived claims to +be applied as circularities, and denote them as `∀x. φᵢ(x) → ♢∃z.ψᵢ(x,z)`, +where `φᵢ(x)` also contains the guard `0 ≤ measure(x) < measure(x₀)`. -__Note__: If the unfication condition `⌈φ ∧ φᵢ⌉ = (xᵢ=tᵢ)∧ pᵢ` -with `tᵢ` functional, `pᵢ` predicate, and `tᵢ` free of `xi`. -Then the goal `∀x∪zᵢ.(∃xᵢ.ψᵢ ∧ ⌈φ∧φᵢ⌉) → ♢∃z.ψ` -is equivalent to `∀x∪zᵢ.ψᵢ[tᵢ/xᵢ] ∧ pᵢ[tᵢ/xᵢ] → ♢∃z.ψ`. +### Background on unification and remainders of unification -Similarly `goalᵣₑₘ := (φ ∧ ¬∃x₁.⌈φ∧φ₁⌉ ∧ … ∧ ¬∃xₙ.⌈φ∧φₙ⌉)` -is equivalent to `(φ ∧ ⋀ⱼ ¬pⱼ[tⱼ/xⱼ])` -where `j` ranges over the set `{ i : 1 ≤ i ≤ n, φ unifies with φᵢ }`. +Similarly to the All-Path Reachability document, we assume all pattern variables +used in this document to be _extended function-like patterns_, that is patterns +which can be written as `t ∧ p` where the interpretation of `t` contains at most +one element and `p` is a predicate. Note that this definition is similar to that +of _constrained terms_ used in reachability logic literature except that it +allows their term part `t` to be undefined. -__Note__: If `φ` does not unify with `φᵢ`, then `⌈φ∧φᵢ⌉ = ⊥`, hence -the goal `∀x∪zᵢ.(∃xᵢ.ψᵢ ∧ ⌈φᵢʳᵉᵐ∧φᵢ⌉) → ♢∃z.ψ` is equivalent to -`∀x.⊥ → ♢∃z.ψ` which can be discharged immediately. Also, in the -remainder `¬∃x₁.⌈φ∧φ₁⌉ = ⊤` so the conjunct can be removed. +_Extended constructor patterns_ will be those extended function-like patterns +for which `t` is a functional term, composed out of constructor-like symbols +and variables. -Explanation ------------ +__Note:__ +Whenever `φ` is an extended function-like pattern with no variables from `z` and +`ψ(z)` is an extended constructor-like pattern, then +``` +φ ∧ ∃z.ψ(z) ≡ ∃z.φ ∧ ψ(z) ≡ ∃z.ψ(z) ∧ ⌈φ ∧ ψ(z)⌉ +``` +and +``` +φ ∧ ¬∃z.ψ = φ ∧ ¬∃z.⌈φ ∧ ψ(z)⌉ +``` -Say we want to prove `∀x. (φ₁(x) → ♢∃z.ψ₁(x,z)) ∧ ... ∧ (φₙ(x) → ♢∃z.ψₙ(x,z)) [decreasing measure(x)]`. +Moreover, we will assume that the unification condition `⌈φ ∧ ψ(z)⌉` can always +be computed to be of the form `(z = t) ∧ p(z)`, where -We will do that by well-founded induction over `measure(x)`. -To do that, we would need to ensure that `measure(x)` is always positive; -this could be checked either syntactically, or using the SMT. +* `t`s are functional patterns with no free variables from `z` + * i.e., `[t / z]` is a substitution. +* `p(z)` is a predicate -Fix an arbitrary instance `x₀` of the variables. We have to prove each -reachability claim `φᵢ(x₀) → ♢∃z.ψᵢ(x₀,z)`, using the induction hypothesis -`∀x. measure(x) < measure(x₀) → (φ₁(x) → ♢∃z.ψ₁(x,z)) ∧ ... ∧ (φₙ(x) → ♢∃z.ψₙ(x,z))` -which can be split into induction hypotheses for each claim -`∀x. φᵢ(x) ∧ measure(x) < measure(x₀) → ♢∃z.ψᵢ(x,z)`. +Note that `p` can be `⟂` to signify that unification failed. +Hence, whenever `φ` is an extended function-like pattern and `ψ(z)` is an +extended constructor-like pattern, we have the following equivalent patterns: +``` +φ ≡ φ ∧ ⊤ ≡ φ ∧ (∃z.ψ(z) ∨ ¬∃z.ψ(z)) ≡ (φ ∧ ∃z.ψ(z)) ∨ (φ ∧ ¬∃z.ψ(z)) ≡ +(∃z.φ ∧ ψ(z)) ∨ (φ ∧ ¬∃z.⌈φ ∧ ψ(z)⌉) ≡ +(∃z.ψ(z) ∧ ⌈φ ∧ ψ(z)⌉) ∨ (φ ∧ ¬∃z.⌈φ ∧ ψ(z)⌉) ≡ +(∃z.ψ(z) ∧ (z = t) ∧ p(z)) ∨ (φ ∧ ¬∃z.(z = t) ∧ p(z)) ≡ +(ψ(t) ∧ p(t)) ∨ (φ ∧ ¬p(t)) +``` -Since we might be using the claims to advance the proof of the claim, to avoid -confusion (and to reduce caring about indices) we will denote a goal with -`φ(x₀) → ♢∃z.ψ(x₀,z)` in all subsequent steps, although the exact goal might -change from one step to the next. +Note that in the left disjunct we can eliminate the predicate part of `ψ(t)` +from `p(t)` (by idempotence, as it's already present in `ψ(t)`). +Similarly, in the right disjunct we can eliminate the predicate part of `φ` +from `p(t)` (by deMorgan, distributivity, and cancelation). ### Eliminating the conclusion @@ -214,8 +183,7 @@ the following sequence of equivalent claims: ``` φ(x₀) → ♢∃z.ψ(x₀,z) -φ(x₀) ∧ (∃z.ψ(x₀, z) ∨ ¬∃z.ψ(x₀, z)) → ♢∃z.ψ(x₀,z) -(φ(x₀) ∧ ∃z.ψ(x₀, z)) ∨ (φ(x₀) ∧ ¬∃z.ψ(x₀, z)) → ♢∃z.ψ(x₀,z) +(φ(x₀) ∧ ∃z.ψ(x₀, z)) ∨ (φ(x₀) ∧ ¬∃z.ψ(x₀, z)) → ♢∃z.ψ(x₀,z) (φ(x₀) ∧ ∃z.ψ(x₀, z) → ♢∃z.ψ(x₀,z)) ∧ (φ(x₀) ∧ ¬∃z.ψ(x₀, z) → ♢∃z.ψ(x₀,z)) ``` @@ -226,111 +194,86 @@ disjunct). This reduces the above to proving the following remainder claim: -```` +``` φ(x₀) ∧ ¬∃z.ψ(x₀, z) → ♢∃z.ψ(x₀,z) ``` -Let `φ(x₀)` denote `φ(x₀) ∧ ¬(∃z.ψ(x₀, z))` in the sequel. +Note that `φ(x₀) ∧ ¬∃z.ψ(x₀, z)` is also an extended function-like pattern, as +it can be rewritten to be of the form `φ(x₀) ∧ ¬p(x₀, t(x₀))` +By abuse of notation, let `φ(x₀)` denote `φ(x₀) ∧ ¬∃z.ψ(x₀, z)` in the sequel. If `φ(x₀)` is equivalent to `⊥`, then the implication holds and we are done. -### Applying circularities (induction hypotheses) +### Applying (extended) claims -To apply circularities we have to ensure that the measure has decreased. -However, whenever circularities may be applied, we want to apply them -immediately (to allow skipping over loops/recursive calls), and to only apply -regular rules on the parts on which circularities cannot apply. - -On the other hand, care should be taken when choosing the measure, to ensure -it actually holds whenever one needs to reenter a loop/call a recursive -function. Failing to have a good such measure would result in the circularities -never being applied and the proof looping (and branching) forever. - -In the following, let `∀x.φᵢ(x) → ♢∃z.ψᵢ(x,z)` denote the ith induction -hypothesis, with `φᵢ(x)` including the `measure(x) < measure(x₀)` check. +Since both circularities (induction hypotheses) and already proven claims are of +the form `∀x.φᵢ(x) → ♢∃z.ψᵢ(x,z)`, we will refer to all as extended claims. +Let `∀x.φᵢ(x) → ♢∃z.ψᵢ(x,z)` denote the ith induction hypothesis or already +proven claim. ``` φ(x₀) → ♢∃z.ψ(x₀,z) -φ(x₀) ∧ (∃x.φ₁(x) ∨ … ∨ ∃x.φₙ(x) ∨ (¬∃x.φ₁(x) ∧ … ∧ ¬∃x.φₙ(x)) → ♢∃z.ψ(x₀,z) +φ(x₀) ∧ (∃x.φ₁(x) ∨ … ∨ ∃x.φₙ(x) ∨ (¬∃x.φ₁(x) ∧ … ∧ ¬∃x.φₙ(x))) → ♢∃z.ψ(x₀,z) (φ(x₀) ∧ ∃x.φ₁(x)) ∨ … ∨ (φ(x₀) ∧ ∃x.φₙ(x)) ∨ (φ(x₀) ∧ (¬∃x.φ₁(x) ∧ … ∧ ¬∃x.φₙ(x))) → ♢∃z.ψ(x₀,z) -(φ(x₀) ∧ ∃x.φ₁(x) → ♢∃z.ψ(x₀,z)) ∧ … (φ(x₀) ∧ ∃x.φₙ(x) → ♢∃z.ψ(x₀,z)) ∧ (φ(x₀) ∧ (¬∃x₁.φ₁ ∧ … ∧ ¬∃xₙ.φₙ)) → ♢∃z.ψ(x₀,z)) +(φ(x₀) ∧ ∃x.φ₁(x) → ♢∃z.ψ(x₀,z)) ∧ … (φ(x₀) ∧ ∃x.φₙ(x) → ♢∃z.ψ(x₀,z)) + ∧ (φ(x₀) ∧ (¬∃x.φ₁(x) ∧ … ∧ ¬∃x.φₙ(x)) → ♢∃z.ψ(x₀,z)) ``` -Note that the remainder can be rewritten using the following equivalences: - +assuming that `⌈φ(x₀) ∧ φᵢ(x)⌉ ≡ (x = tᵢ(x₀)) ∧ pᵢ(x₀, x)` for each `i`, +the above is equivalent with: ``` -φ(x₀) ∧ (¬∃x.φ₁(x) ∧ … ∧ ¬∃x.φₙ(x)) → ♢ψ(x₀,z) -(φ(x₀) ∧ ¬∃x.φ₁(x)) ∧ … ∧ (φ(x₀) ∧ ¬∃x.φₙ(x)) → ♢ψ(x₀,z) -(φ(x₀) ∧ ¬∃x.⌈φ(x₀) ∧ φ₁(x)⌉) ∧ … ∧ (φ(x₀) ∧ ¬∃x.⌈φ(x₀)∧φₙ(x)⌉) → ♢ψ(x₀,z) -φ(x₀) ∧ (¬∃x.⌈φ(x₀) ∧ φ₁(x)⌉ ∧ … ∧ ¬∃x.⌈φ(x₀)∧φₙ(x)⌉) → ♢ψ(x₀,z) +(φ₁(t₁(x₀)) ∧ p₁(x₀, t₁(x₀)) → ♢∃z.ψ(x₀,z)) ∧ … (φₙ(tₙ(x₀)) ∧ pₙ(x₀, tₙ(x₀)) → ♢∃z.ψ(x₀,z)) + ∧ (φ(x₀) ∧ ¬p₁(x₀, t₁(x₀)) ∧ … ∧ ¬pₙ(x₀, tₙ(x₀)) → ♢∃z.ψ(x₀,z)) ``` -In particular, part of the predicate of the remainder will include the negation -of the measure check, `¬measure(x) < measure(x₀)` instantiated with the -substitution associated with any term part of some `φᵢ(x)` matching `φ(x₀)`. - -#### Using a claim to advance the corresponding goal - -We want to prove that from the induction hypothesis `∀x. φᵢ(x) → ♢∃z.ψᵢ(x,z)` -and the derived goal `∀zᵢ.∃x.(ψᵢ(x,zᵢ) ∧ ⌈φ(x₀) ∧ φᵢ(x)⌉) → ♢∃z.ψ(x₀, z)` -we can deduce that `φ(x₀) ∧ ∃x.φᵢ(x) → ♢∃z.ψ(x₀,z)`. - -This would allow us to replace goal `φ(x₀) ∧ ∃x.φᵢ(x) → ♢∃z.ψ(x₀,z)` -with goal `∀zᵢ.∃x.(ψᵢ(x,zᵢ) ∧ ⌈φ(x₀) ∧ φᵢ(x)⌉) → ♢∃z.ψ(x₀,z)`. - -_Proof:_ - -The main step of our proof is to prove -`φ(x₀) ∧ ∃x.φᵢ(x) → ♢∃x.((∃zᵢ.ψᵢ(x,z)) ∧ ⌈φ(x₀) ∧ φᵢ(x)⌉)` -from `∀x. φᵢ(x) → ♢∃z.ψᵢ(x,z)`. - -Assume `⌈φ(x₀) ∧ φᵢ(x)⌉ = (x=tᵢ(x₀))∧ pᵢ(x, x₀)` with `tᵢ(x₀)` functional and -free of `x` and `pᵢ(x₀,x)` predicate. - -Then, +This can be split into proving a goal for each extended claim, +``` +φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → ♢∃z.ψ(x₀,z) +``` +and one for the remainder ``` -φᵢ(tᵢ) → ♢∃z.ψᵢ(tᵢ, z) // by induction hypothesis ∀x.φᵢ(x) → ♢∃z.ψᵢ(x,z) instantiated to x := tᵢ -φᵢ(tᵢ) ∧ p(x₀,tᵢ) → (♢∃z.ψᵢ(tᵢ, z)) ∧ p(x₀,tᵢ) // framing -φᵢ(tᵢ) ∧ p(x₀,tᵢ) → ♢((∃z.ψᵢ(tᵢ, z)) ∧ p(x₀,tᵢ)) // predicate properties -∃x.φᵢ(x) ∧ x=tᵢ ∧ p(x₀,x) → ♢∃x.((∃z.ψᵢ(x,z)) ∧ x=tᵢ ∧ p(x₀,x)) // substitution properties -∃x.φᵢ(x) ∧ ⌈φ(x₀)∧φᵢ(x)⌉ → ♢∃x.((∃z.ψᵢ(x,z)) ∧ ⌈φ(x₀)∧φᵢ(x)⌉) // definition of ⌈φ(x₀)∧φᵢ(x)⌉ -φ(x₀) ∧ ∃x.φᵢ(x) ∧ ⌈φ(x₀)∧φᵢ(x)⌉ → ♢∃x.((∃z.ψᵢ(x,z)) ∧ ⌈φ(x₀)∧φᵢ(x)⌉) // Strengthening -φ(x₀) ∧ ∃x.⌈φ(x₀) ∧ φᵢ(x) ∧ ⌈φ(x₀)∧φᵢ(x)⌉⌉ → ♢∃x.((∃z.ψᵢ(x,z)) ∧ ⌈φ(x₀)∧φᵢ(x)⌉) // φ is functional -φ(x₀) ∧ ∃x.(⌈φ(x₀) ∧ φᵢ(x)⌉ ∧ ⌈φ(x₀)∧φᵢ(x)⌉) → ♢∃x.((∃z.ψᵢ(x,z)) ∧ ⌈φ(x₀)∧φᵢ(x)⌉) // predicate properties -φ(x₀) ∧ ∃x.⌈φ(x₀) ∧ φᵢ(x)⌉ → ♢∃x.((∃z.ψᵢ(x,z)) ∧ ⌈φ(x₀)∧φᵢ(x)⌉) // idempotency -φ(x₀) ∧ ∃x.φᵢ(x) → ♢∃x.((∃z.ψᵢ(x,z)) ∧ ⌈φ(x₀)∧φᵢ(x)⌉) // φ is functional +φ(x₀) ∧ ¬p₁(x₀, t₁(x₀)) ∧ … ∧ ¬pₙ(x₀, tₙ(x₀) → ♢∃z.ψ(x₀,z)) ``` -#### Summary of applying circularities +Note that, in particular, part of the predicate of the remainder will include +the negation of the measure check for each induction hypothesis, of the form +`¬measure(tᵢ(x₀)) < measure(x₀)`. -By applying the circularities, we will replace the existing goal with a set -consisting of a goal for each circularity (some with the hypothesis equivalent -with `⟂`) and a remainder. +#### Using a claim to advance the corresponding goal -For a given induction hypothesis ``∀x. φᵢ(x) → ♢∃z.ψᵢ(x,z)`, -since `φ(x₀)` and `φᵢ(x)` are both function-like patterns (constrained terms), -we can assume that `⌈φ(x₀) ∧ φᵢ(x)⌉` can be written of the form -`(x=tᵢ(x₀)) ∧ pᵢ(x, x₀)` with `tᵢ(x₀)` functional and free of `x` and -`pᵢ(x₀,x)` a predicate (which can be bottom to account for unification failure). +Assume `φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → ♢∃z.ψ(x₀,z)` goal to be proven +and let `∀x. φᵢ(x) → ♢∃z.ψᵢ(x,z)` be the corresponding extended claim. +By instatiating the claim with `x := tᵢ(x₀)`, we obtain +`φᵢ(tᵢ(x₀)) → ♢∃z.ψᵢ(tᵢ(x₀),z)`; then, by framing, we obtain +`φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → (♢∃z.ψᵢ(tᵢ(x₀),z)) ∧ pᵢ(x₀, tᵢ(x₀))`. +Next, by predicate properties, we can obtain that +`φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → ♢∃z.(ψᵢ(tᵢ(x₀),z) ∧ pᵢ(x₀, tᵢ(x₀)))`. -Then the derived goal associated to this induction hypothesis will be -`∀zᵢ.∃x.(ψᵢ(x,zᵢ) ∧ ⌈φ(x₀) ∧ φᵢ(x)⌉) → ♢∃z.ψ(x₀,z)`, which, using the above -identity, is equivalent to +We can use transitivity of `→` to replace the initial goal with +`♢∃z.ψᵢ(tᵢ(x₀),z) ∧ pᵢ(x₀, tᵢ(x₀)) → ♢∃z.ψ(x₀,z)` +This goal can soundly be replaced with +`∀z.ψᵢ(tᵢ(x₀),z) ∧ pᵢ(x₀, tᵢ(x₀)) → ♢∃z.ψ(x₀,z)` +as proving this goal would ensure that the above also holds. -``` -∀zᵢ.∃x.(ψᵢ(x,zᵢ) ∧ (x=tᵢ(x₀)) ∧ pᵢ(x, x₀)) → ♢∃z.ψ(x₀,z) -∀zᵢ.∃x.(ψᵢ(tᵢ(x₀),zᵢ) ∧ pᵢ(tᵢ(x₀), x₀)) → ♢∃z.ψ(x₀,z) -∀zᵢ.ψᵢ(tᵢ(x₀),zᵢ) ∧ pᵢ(tᵢ(x₀), x₀) → ♢∃z.ψ(x₀,z) -``` +#### Summary of applying extended claims -Using the fact that the variables `zᵢ` only appear in the lhs, we can -instantiate them to arbitrary (but fixed) symbolic variables `z₀`, and then -let `φ(x₀)` denote ψᵢ(tᵢ(x₀),z₀) ∧ pᵢ(tᵢ(x₀), x₀)` for the next phase of the -algorithm. +By applying the extended claims, we will replace the existing goal with a set +consisting of a goal for each extended claim (some with the hypothesis equivalent +with `⟂`) and a remainder. +- Goals associated to extended claims: `∀z.ψᵢ(tᵢ(x₀),z) ∧ pᵢ(x₀, tᵢ(x₀)) → ♢∃z.ψ(x₀,z)` +- Goal associated to the remainder: `φ(x₀) ∧ ¬p₁(x₀, t₁(x₀)) ∧ … ∧ ¬pₙ(x₀, tₙ(x₀) → ♢∃z.ψ(x₀,z))` + By abuse of notation, let `φ(x₀)` denote `φ(x₀) ∧ ¬p₁(x₀, t₁(x₀)) ∧ … ∧ ¬pₙ(x₀, tₙ(x₀)` ### Applying axioms -We're back now to `φ(x₀) → (○♢∃z.ψ(x₀,z)) ∧ •⊤`, which is equivalent to +The remainder from the above step denotes the case in which the conclusion +doesn't hold now, and neither of the extended claims can be applied. + +We'll try therefore to apply one step from the semantics. +Let `φ(x₀) → ♢∃z.ψ(x₀,z))` be the remainder goal. We can unfold `♢` to obtain +the equivalent `φ(x₀) → ∃z.ψ(x₀,z) ∨ ((○♢∃z.ψ(x₀,z)) ∧ •⊤)`. Since we know +that conclusion doesn't hold for `φ(x₀)`, we can replace the goal by +`φ(x₀) → (○♢∃z.ψ(x₀,z)) ∧ •⊤`, which is equivalent to `(φ(x₀) → ○♢∃z.ψ(x₀, z)) ∧ (φ(x₀) → •⊤)` Therefore we need to check two things: @@ -362,7 +305,7 @@ we can derive `φ(x₀) → ○♢∃z.ψ(x₀,z)` This would allow us to replace the goal `φ(x₀) → ○♢∃z.ψ(x₀,z)` with the set of goals ``` -{ ∀zᵢ.∃xᵢ.ψᵢ(xᵢ,zᵢ) ∧ ⌈φ(x₀) ∧ φᵢ(xᵢ)⌉ → ♢∃z.ψ(x₀,z) : 1 ≤ i ≤ n } +{ ∀zᵢ.ψᵢ(tᵢ(x₀),zᵢ) ∧ pᵢ(tᵢ(x₀)) → ♢∃z.ψ(x₀,z) : 1 ≤ i ≤ n } ``` _Proof:_ @@ -381,9 +324,89 @@ o ⋁ᵢ ∃xᵢ.⌈φ(x₀) ∧ φᵢ(xᵢ)⌉ ∧ ∃zᵢ.ψᵢ(xᵢ,zᵢ) → #### Summary of applying the claims -- Check that the remainder `φ(x₀) ∧ ¬∃x₁.φ₁(x₁) ∧ … ∧ ¬∃xₙ.φₙ(xₙ)` is equivalent to `⟂` +- Check that the remainder `φ(x₀) ∧ ¬p₁(t₁(x₀)) ∧ … ∧ ¬pₙ(tₙ(x₀)))` is equivalent to `⟂` - Replace the goal `φ(x₀) → ○♢∃z.ψ(x₀,z)` by the set of goals ``` - { ∀zᵢ.∃xᵢ.ψᵢ(xᵢ,zᵢ) ∧ ⌈φ(x₀) ∧ φᵢ(xᵢ)⌉ → ♢∃z.ψ(x₀,z) : 1 ≤ i ≤ n } + { ∀zᵢ.ψᵢ(tᵢ(x₀),zᵢ) ∧ pᵢ(tᵢ(x₀)) → ♢∃z.ψ(x₀,z) : 1 ≤ i ≤ n } ``` +## Algorithms +------------- + +To apply circularities we have to ensure that the measure has decreased. +However, whenever circularities may be applied, we want to apply them +immediately (to allow skipping over loops/recursive calls), and to only apply +regular rules on the parts on which circularities cannot apply. + +On the other hand, care should be taken when choosing the measure, to ensure +it actually holds whenever one needs to reenter a loop/call a recursive +function. Failing to have a good such measure would result in the circularities +never being applied and the proof looping (and branching) forever. + + +### Algorithm `proveAllPath` + +__Input:__ + +- set of variables `x` +- claim group `(φ₁(x) → ♢∃z.ψ₁(x,z)) ∧ ... ∧ (φₙ(x) → ♢∃z.ψₙ(x,z))` +- decreasing `measure(x)` + +__Output:__ Proved or Unproved + +* Fix an instance `x₀` for the variables `x` +* Let `claims ::= { ∀ x . φᵢ(x) ∧ measure(x) =Int 0` + * Let `claimsᵢ ::= claims ∪ { claimᵢ₁, ..., claimᵢₖ }` + * Let `Goals := { φᵢ(x₀) }` + * While `Goals` is not empty: + * Extract and remove `goal` of the form `φ` from `Goals` + * Let `goalᵣₑₘ := φ ∧ ¬∃z.⌈φ ∧ ψᵢ⌉` + * If `goalᵣₑₘ` is bottom (`goalᵣₑₘ ≡ ⊥`) + * continue to the next goal + * `(Goals', goal'ᵣₑₘ) := derivePar(goalᵣₑₘ, claimsᵢ)` + * Let `(Goals'', goal''ᵣₑₘ) := derivePar(goal'ᵣₑₘ, axioms)` + * If `goal''ᵣₑₘ` is not trivially valid (its lhs is not equivalent to `⊥`) + * Return `Unprovable` + * Let `Goals := Goals ∪ Goals' ∪ Goals''` +* Return `Provable` + +__Note:__ Since the derivation process can continue indefinitely, one could add +a bound on the total number of (levels of) expansions attempted before +returning `Unprovable`. + +__Note__: If the unfication condition `⌈φ ∧ ψ⌉ = (z=t)∧ p` +with `t` functional, `p` predicate, and `t` free of `z`. +Then `goalᵣₑₘ := φ ∧ ¬∃z.⌈φ ∧ ψ⌉` +is equivalent to `φ ∧ ¬pᵢ[tᵢ/xᵢ]`. + +### Algorithm `derivePar` + +__Input:__: goal `φ` and set of tuples `{ (xᵢ,φᵢ,zᵢ,ψᵢ) : 1 ≤ i ≤ n }` representing either + +* extended claims `{ ∀xᵢ.φᵢ → ♢∃zᵢ.ψᵢ : 1 ≤ i ≤ n }`, or +* axioms `{ ∀xᵢ.φᵢ → •∃zᵢ.ψᵢ : 1 ≤ i ≤ n }` + +__Output:__ `(Goals, goalᵣₑₘ)` + +* Let `goalᵣₑₘ := φ ∧ ¬∃x₁.⌈φ∧φ₁⌉ ∧ … ∧ ¬∃xₙ.⌈φ∧φₙ⌉` +* Let `Goals := { ∀z₁.(∃x₁.ψ₁ ∧ ⌈φ∧φ₁⌉), … , ∀zₙ.(∃xₙ.ψₙ ∧ ⌈φ∧φₙ⌉) }` + +__Note__: `∀zᵢ.(∃xᵢ.ψᵢ ∧ ⌈φ∧φᵢ⌉)` is obtained from +`(∃xᵢ.(∃zᵢ.ψᵢ) ∧ ⌈φ∧φᵢ⌉) → ♢∃z.ψ` + +__Note__: If the unfication condition `⌈φ ∧ φᵢ⌉ = (xᵢ=tᵢ)∧ pᵢ` +with `tᵢ` functional, `pᵢ` predicate, and `tᵢ` free of `xi`. +Then the goal `∀zᵢ.(∃xᵢ.ψᵢ ∧ ⌈φ∧φᵢ⌉) → ♢∃z.ψ` +is equivalent to `∀zᵢ.ψᵢ[tᵢ/xᵢ] ∧ pᵢ[tᵢ/xᵢ] → ♢∃z.ψ`. + +Similarly `goalᵣₑₘ := (φ ∧ ¬∃x₁.⌈φ∧φ₁⌉ ∧ … ∧ ¬∃xₙ.⌈φ∧φₙ⌉)` +is equivalent to `(φ ∧ ⋀ⱼ ¬pⱼ[tⱼ/xⱼ])` +where `j` ranges over the set `{ i : 1 ≤ i ≤ n, φ unifies with φᵢ }`. + +__Note__: If `φ` does not unify with `φᵢ`, then `⌈φ∧φᵢ⌉ = ⊥`, hence +the goal `∀x∪zᵢ.(∃xᵢ.ψᵢ ∧ ⌈φᵢʳᵉᵐ∧φᵢ⌉) → ♢∃z.ψ` is equivalent to +`∀x.⊥ → ♢∃z.ψ` which can be discharged immediately. Also, in the +remainder `¬∃x₁.⌈φ∧φ₁⌉ = ⊤` so the conjunct can be removed. + From 08ab519f125f94a99b7278d8c307fbb73c1f3f03 Mon Sep 17 00:00:00 2001 From: Traian Florin Serbanuta Date: Thu, 5 May 2022 14:02:19 +0300 Subject: [PATCH 3/9] Addressing review comments --- ...orectness-All-Path-Reachability-Proofs.md} | 187 ++++++++++-------- 1 file changed, 110 insertions(+), 77 deletions(-) rename docs/{2022-04-07-Full-Corectness-All-Path-Reachability-Proofs.md => 2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md} (66%) diff --git a/docs/2022-04-07-Full-Corectness-All-Path-Reachability-Proofs.md b/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md similarity index 66% rename from docs/2022-04-07-Full-Corectness-All-Path-Reachability-Proofs.md rename to docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md index 82129870fb..01249d5991 100644 --- a/docs/2022-04-07-Full-Corectness-All-Path-Reachability-Proofs.md +++ b/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md @@ -1,9 +1,7 @@ -Proving Full Correctness All-Path Reachability Claims +Proving Total Corectness All-Path Reachability Claims ===================================================== -This document details Full Correctness All-Path Reachability without solving the -most-general-unifier (MGU) problem. -MGU will be detailed in a separate document. +This document details Total Corectness All-Path Reachability. _Prepared by Traian Șerbănuță, based on [proving All-Path Reachability claims](2019-03-28-All-Path-Reachability-Proofs.md)_ @@ -11,39 +9,74 @@ claims](2019-03-28-All-Path-Reachability-Proofs.md)_ Definitions ----------- +In the following, by abuse of notation, we will identify a formula with the set +of configurations it denotes, thus equality between formulae would mean that +they are equisatisfiable (they denote the same set of configurations). + ### All-path finally -Given a formula `φ`, let `♢φ` denote the formula “all-path finally” `φ`, +Given a formula `φ`, let `AFφ` denote the formula “all-path finally” `φ`, defined by: ``` -♢φ := μX.φ ∨ (○X ∧ •⊤) +AFφ := μX.φ ∨ (○X ∧ •⊤) ``` -one consequence of the above is that `♢φ ≡ φ ∨ (○♢φ ∧ •⊤)`. +#### Semantics of `AFφ` + +By the definition above, `AFφ` is semantically defined as `LFP(G)`, the +least-fix-point of the following mapping: -Given this definition of all-path finally, a full correctness all-path -reachability claim ``` -∀x.φ(x) → ♢∃z.ψ(x,z) +G(X) := φ ∨ (○X ∧ •⊤) ``` -basically states that if `φ(x)` holds for a configuration `γ`, for some `x`, -then `P(γ)` holds, where `P(G)` is recursively defined on configurations as: -* there exists `z` such that `ψ(x,z)` holds for `G` -* or - * `G` is not stuck (`G → • T`) and - * `P(G')` for all configurations `G'` in which `G` can transition -__Note:__ -Using the least fix-point (`μ`) instead of the greatest fix-point (`ν`) -restricts paths to finite ones. Therefore, the intepretation of a reachability -claim guarantees full-correctness, as it requires that the conclusion is -reached in a finite number of steps. +Note that `G(X)` can be interpreted as the union between the set of +configurations for which `φ` holds and those which are not stuck and whose all +possible transitions lead into `X`. + +Since `AFφ` is a fixed-point of `G`, the identity `G(AFφ) = AFφ` holds, whence +`AFφ = φ ∨ (○AFφ ∧ •⊤)`. + +Moreover, `G` is monotone (`X` occurs in a positive position) and we can show +that the conditions of Kleene's fixed-point theorem are satisfied: +`Gⁿ(⊥) ⊆ Gⁿ⁺¹(⊥)`, because `Gⁿ(⊥)` denotes the set of configurations for which +on all paths, in at most `n-1` steps, `φ` holds. + +Let us argue the above by induction on `n-1`. +- Base case: `G(⊥) = φ ∨ (○⊥ ∧ •⊤) = φ ∨ (¬•¬⊥ ∧ •⊤) = φ ∨ (¬•⊤ ∧ •⊤) = φ ∨ ⊥ = φ`, + so `G(⊥)` is the set of configurations for which `φ` holds. +- Induction case: Assuming `Gⁿ(⊥)` denotes the set of configurations for which + on all paths, in at most `n-1` steps, `φ` holds, `Gⁿ⁺¹(⊥) = G(Gⁿ(⊥))` will be + the union between the set of configurations for which `φ` holds and those + which are not stuck and whose all possible transitions lead into the set of + configurations for which on all paths, in at most `n-1` steps, `φ` holds, but + these are precisely the configurations for which on all paths, in at most `n` + steps, `φ` holds. + +From Kleene's theorem, `AFφ = ⋁ₙGⁿ(⊥)`, whence, a configuration is in `AFφ` iff +it is in `Gⁿ(⊥)` for some positive integer `n`. By the characterization of +`Gⁿ(⊥)` presented above, it follows that `AFφ` denotes the set of configurations +for which on all paths, in a finite number of steps, `φ` holds. + +### Total corectness all-path reachability claims + +Given this definition of all-path finally, a total corectness all-path +reachability claim is of the form +``` +∀x.φ(x) → AF∃z.ψ(x,z) +``` +and basically states that from any configuration `γ` satisfying `φ(x)` +for some `x`, a configuration satisfying `ψ(x,z)` for some `z` will be reached +in a finite number of steps on any path. + +Since the configuration is reached after a finite number of steps, +such reachability claims guarantee total corectness. Problem Description ------------------- -Given a set of reachability claims, of the form `∀x.φ(x) → ♢∃z.ψ(x,z)`, +Given a set of reachability claims, of the form `∀x.φ(x) → AF∃z.ψ(x,z)`, we are trying to prove all of them together, by well-founded induction on a given `measure` defined on the quantified variables `x`. @@ -68,7 +101,7 @@ claim group . . . - claim φᵢ(x) → ♢∃zᵢ.ψᵢ(x,zᵢ) [using(claimᵢ₁, ..., claimᵢₖ)] + claim φᵢ(x) → AF∃zᵢ.ψᵢ(x,zᵢ) [using(claimᵢ₁, ..., claimᵢₖ)] . . . @@ -92,7 +125,7 @@ have already been proven. Assume also a given integer pattern `measure(x)`, over the same variables as the claims in the group. Since we're proving all claims together, we can gather them in a single goal, -`P(x) ::= (φ₁(x) → ♢∃z.ψ₁(x,z)) ∧ ... ∧ (φₙ(x) → ♢∃z.ψₙ(x,z))`. +`P(x) ::= (φ₁(x) → AF∃z.ψ₁(x,z)) ∧ ... ∧ (φₙ(x) → AF∃z.ψₙ(x,z))`. A well-founded induction principle allowing to prove `P` using `measure` would be of the form @@ -113,19 +146,19 @@ hypothesis `forall x, 0 <= measure(x) < measure(x0) -> P(x)`, we need to prove By first-order manipulation we can transform the induction hypothesis for `P` into a set of induction hypotheses, one for each claim: ``` -∀x. φᵢ(x) ∧ 0 ≤ measure(x) < measure(x₀) → ♢∃z.ψᵢ(x,z) +∀x. φᵢ(x) ∧ 0 ≤ measure(x) < measure(x₀) → AF∃z.ψᵢ(x,z) ``` -Similarly we can split the goal into a separate goal `φᵢ(x₀) → ♢∃z.ψᵢ(x₀,z)` +Similarly we can split the goal into a separate goal `φᵢ(x₀) → AF∃z.ψᵢ(x₀,z)` for each claim. Since we might be using the claims to advance the proof of the claim, to avoid confusion (and to reduce caring about indices) we will denote a goal with -`φ(x₀) → ♢∃z.ψ(x₀,z)` in all subsequent steps, although the exact goal might +`φ(x₀) → AF∃z.ψ(x₀,z)` in all subsequent steps, although the exact goal might change from one step to the next. Moreover, we will consider the induction hypotheses to be derived claims to -be applied as circularities, and denote them as `∀x. φᵢ(x) → ♢∃z.ψᵢ(x,z)`, +be applied as circularities, and denote them as `∀x. φᵢ(x) → AF∃z.ψᵢ(x,z)`, where `φᵢ(x)` also contains the guard `0 ≤ measure(x) < measure(x₀)`. ### Background on unification and remainders of unification @@ -182,20 +215,20 @@ First, let us eliminate the case when the conclusion holds now. We have the following sequence of equivalent claims: ``` -φ(x₀) → ♢∃z.ψ(x₀,z) -(φ(x₀) ∧ ∃z.ψ(x₀, z)) ∨ (φ(x₀) ∧ ¬∃z.ψ(x₀, z)) → ♢∃z.ψ(x₀,z) -(φ(x₀) ∧ ∃z.ψ(x₀, z) → ♢∃z.ψ(x₀,z)) ∧ (φ(x₀) ∧ ¬∃z.ψ(x₀, z) → ♢∃z.ψ(x₀,z)) +φ(x₀) → AF∃z.ψ(x₀,z) +(φ(x₀) ∧ ∃z.ψ(x₀, z)) ∨ (φ(x₀) ∧ ¬∃z.ψ(x₀, z)) → AF∃z.ψ(x₀,z) +(φ(x₀) ∧ ∃z.ψ(x₀, z) → AF∃z.ψ(x₀,z)) ∧ (φ(x₀) ∧ ¬∃z.ψ(x₀, z) → AF∃z.ψ(x₀,z)) ``` -The first conjunct, `φ(x₀) ∧ ∃z.ψ(x₀, z) → ♢∃z.ψ(x₀,z)` can be discharged by -unrolling `♢∃z.ψ(x₀,z)` to `∃z.ψ(x₀,z) φ ∨ (○♢∃z.ψ(x₀,z) ∧ •⊤)`, and then +The first conjunct, `φ(x₀) ∧ ∃z.ψ(x₀, z) → AF∃z.ψ(x₀,z)` can be discharged by +unrolling `AF∃z.ψ(x₀,z)` to `∃z.ψ(x₀,z) φ ∨ (○AF∃z.ψ(x₀,z) ∧ •⊤)`, and then using that `∃z.ψ(x₀, z)` appears in both lhs (as a conjunct) and rhs (as a disjunct). This reduces the above to proving the following remainder claim: ``` -φ(x₀) ∧ ¬∃z.ψ(x₀, z) → ♢∃z.ψ(x₀,z) +φ(x₀) ∧ ¬∃z.ψ(x₀, z) → AF∃z.ψ(x₀,z) ``` Note that `φ(x₀) ∧ ¬∃z.ψ(x₀, z)` is also an extended function-like pattern, as @@ -206,32 +239,32 @@ If `φ(x₀)` is equivalent to `⊥`, then the implication holds and we are done ### Applying (extended) claims Since both circularities (induction hypotheses) and already proven claims are of -the form `∀x.φᵢ(x) → ♢∃z.ψᵢ(x,z)`, we will refer to all as extended claims. -Let `∀x.φᵢ(x) → ♢∃z.ψᵢ(x,z)` denote the ith induction hypothesis or already +the form `∀x.φᵢ(x) → AF∃z.ψᵢ(x,z)`, we will refer to all as extended claims. +Let `∀x.φᵢ(x) → AF∃z.ψᵢ(x,z)` denote the ith induction hypothesis or already proven claim. ``` -φ(x₀) → ♢∃z.ψ(x₀,z) -φ(x₀) ∧ (∃x.φ₁(x) ∨ … ∨ ∃x.φₙ(x) ∨ (¬∃x.φ₁(x) ∧ … ∧ ¬∃x.φₙ(x))) → ♢∃z.ψ(x₀,z) -(φ(x₀) ∧ ∃x.φ₁(x)) ∨ … ∨ (φ(x₀) ∧ ∃x.φₙ(x)) ∨ (φ(x₀) ∧ (¬∃x.φ₁(x) ∧ … ∧ ¬∃x.φₙ(x))) → ♢∃z.ψ(x₀,z) -(φ(x₀) ∧ ∃x.φ₁(x) → ♢∃z.ψ(x₀,z)) ∧ … (φ(x₀) ∧ ∃x.φₙ(x) → ♢∃z.ψ(x₀,z)) - ∧ (φ(x₀) ∧ (¬∃x.φ₁(x) ∧ … ∧ ¬∃x.φₙ(x)) → ♢∃z.ψ(x₀,z)) +φ(x₀) → AF∃z.ψ(x₀,z) +φ(x₀) ∧ (∃x.φ₁(x) ∨ … ∨ ∃x.φₙ(x) ∨ (¬∃x.φ₁(x) ∧ … ∧ ¬∃x.φₙ(x))) → AF∃z.ψ(x₀,z) +(φ(x₀) ∧ ∃x.φ₁(x)) ∨ … ∨ (φ(x₀) ∧ ∃x.φₙ(x)) ∨ (φ(x₀) ∧ (¬∃x.φ₁(x) ∧ … ∧ ¬∃x.φₙ(x))) → AF∃z.ψ(x₀,z) +(φ(x₀) ∧ ∃x.φ₁(x) → AF∃z.ψ(x₀,z)) ∧ … (φ(x₀) ∧ ∃x.φₙ(x) → AF∃z.ψ(x₀,z)) + ∧ (φ(x₀) ∧ (¬∃x.φ₁(x) ∧ … ∧ ¬∃x.φₙ(x)) → AF∃z.ψ(x₀,z)) ``` assuming that `⌈φ(x₀) ∧ φᵢ(x)⌉ ≡ (x = tᵢ(x₀)) ∧ pᵢ(x₀, x)` for each `i`, the above is equivalent with: ``` -(φ₁(t₁(x₀)) ∧ p₁(x₀, t₁(x₀)) → ♢∃z.ψ(x₀,z)) ∧ … (φₙ(tₙ(x₀)) ∧ pₙ(x₀, tₙ(x₀)) → ♢∃z.ψ(x₀,z)) - ∧ (φ(x₀) ∧ ¬p₁(x₀, t₁(x₀)) ∧ … ∧ ¬pₙ(x₀, tₙ(x₀)) → ♢∃z.ψ(x₀,z)) +(φ₁(t₁(x₀)) ∧ p₁(x₀, t₁(x₀)) → AF∃z.ψ(x₀,z)) ∧ … (φₙ(tₙ(x₀)) ∧ pₙ(x₀, tₙ(x₀)) → AF∃z.ψ(x₀,z)) + ∧ (φ(x₀) ∧ ¬p₁(x₀, t₁(x₀)) ∧ … ∧ ¬pₙ(x₀, tₙ(x₀)) → AF∃z.ψ(x₀,z)) ``` This can be split into proving a goal for each extended claim, ``` -φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → ♢∃z.ψ(x₀,z) +φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → AF∃z.ψ(x₀,z) ``` and one for the remainder ``` -φ(x₀) ∧ ¬p₁(x₀, t₁(x₀)) ∧ … ∧ ¬pₙ(x₀, tₙ(x₀) → ♢∃z.ψ(x₀,z)) +φ(x₀) ∧ ¬p₁(x₀, t₁(x₀)) ∧ … ∧ ¬pₙ(x₀, tₙ(x₀) → AF∃z.ψ(x₀,z)) ``` Note that, in particular, part of the predicate of the remainder will include @@ -240,18 +273,18 @@ the negation of the measure check for each induction hypothesis, of the form #### Using a claim to advance the corresponding goal -Assume `φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → ♢∃z.ψ(x₀,z)` goal to be proven -and let `∀x. φᵢ(x) → ♢∃z.ψᵢ(x,z)` be the corresponding extended claim. +Assume `φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → AF∃z.ψ(x₀,z)` goal to be proven +and let `∀x. φᵢ(x) → AF∃z.ψᵢ(x,z)` be the corresponding extended claim. By instatiating the claim with `x := tᵢ(x₀)`, we obtain -`φᵢ(tᵢ(x₀)) → ♢∃z.ψᵢ(tᵢ(x₀),z)`; then, by framing, we obtain -`φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → (♢∃z.ψᵢ(tᵢ(x₀),z)) ∧ pᵢ(x₀, tᵢ(x₀))`. +`φᵢ(tᵢ(x₀)) → AF∃z.ψᵢ(tᵢ(x₀),z)`; then, by framing, we obtain +`φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → (AF∃z.ψᵢ(tᵢ(x₀),z)) ∧ pᵢ(x₀, tᵢ(x₀))`. Next, by predicate properties, we can obtain that -`φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → ♢∃z.(ψᵢ(tᵢ(x₀),z) ∧ pᵢ(x₀, tᵢ(x₀)))`. +`φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → AF∃z.(ψᵢ(tᵢ(x₀),z) ∧ pᵢ(x₀, tᵢ(x₀)))`. We can use transitivity of `→` to replace the initial goal with -`♢∃z.ψᵢ(tᵢ(x₀),z) ∧ pᵢ(x₀, tᵢ(x₀)) → ♢∃z.ψ(x₀,z)` +`AF∃z.ψᵢ(tᵢ(x₀),z) ∧ pᵢ(x₀, tᵢ(x₀)) → AF∃z.ψ(x₀,z)` This goal can soundly be replaced with -`∀z.ψᵢ(tᵢ(x₀),z) ∧ pᵢ(x₀, tᵢ(x₀)) → ♢∃z.ψ(x₀,z)` +`∀z.ψᵢ(tᵢ(x₀),z) ∧ pᵢ(x₀, tᵢ(x₀)) → AF∃z.ψ(x₀,z)` as proving this goal would ensure that the above also holds. #### Summary of applying extended claims @@ -260,8 +293,8 @@ By applying the extended claims, we will replace the existing goal with a set consisting of a goal for each extended claim (some with the hypothesis equivalent with `⟂`) and a remainder. -- Goals associated to extended claims: `∀z.ψᵢ(tᵢ(x₀),z) ∧ pᵢ(x₀, tᵢ(x₀)) → ♢∃z.ψ(x₀,z)` -- Goal associated to the remainder: `φ(x₀) ∧ ¬p₁(x₀, t₁(x₀)) ∧ … ∧ ¬pₙ(x₀, tₙ(x₀) → ♢∃z.ψ(x₀,z))` +- Goals associated to extended claims: `∀z.ψᵢ(tᵢ(x₀),z) ∧ pᵢ(x₀, tᵢ(x₀)) → AF∃z.ψ(x₀,z)` +- Goal associated to the remainder: `φ(x₀) ∧ ¬p₁(x₀, t₁(x₀)) ∧ … ∧ ¬pₙ(x₀, tₙ(x₀) → AF∃z.ψ(x₀,z))` By abuse of notation, let `φ(x₀)` denote `φ(x₀) ∧ ¬p₁(x₀, t₁(x₀)) ∧ … ∧ ¬pₙ(x₀, tₙ(x₀)` ### Applying axioms @@ -270,16 +303,16 @@ The remainder from the above step denotes the case in which the conclusion doesn't hold now, and neither of the extended claims can be applied. We'll try therefore to apply one step from the semantics. -Let `φ(x₀) → ♢∃z.ψ(x₀,z))` be the remainder goal. We can unfold `♢` to obtain -the equivalent `φ(x₀) → ∃z.ψ(x₀,z) ∨ ((○♢∃z.ψ(x₀,z)) ∧ •⊤)`. Since we know +Let `φ(x₀) → AF∃z.ψ(x₀,z))` be the remainder goal. We can unfold `AF` to obtain +the equivalent `φ(x₀) → ∃z.ψ(x₀,z) ∨ ((○AF∃z.ψ(x₀,z)) ∧ •⊤)`. Since we know that conclusion doesn't hold for `φ(x₀)`, we can replace the goal by -`φ(x₀) → (○♢∃z.ψ(x₀,z)) ∧ •⊤`, which is equivalent to -`(φ(x₀) → ○♢∃z.ψ(x₀, z)) ∧ (φ(x₀) → •⊤)` +`φ(x₀) → (○AF∃z.ψ(x₀,z)) ∧ •⊤`, which is equivalent to +`(φ(x₀) → ○AF∃z.ψ(x₀, z)) ∧ (φ(x₀) → •⊤)` Therefore we need to check two things: 1. That `φ(x₀)` is not stuck -1. That `φ(x₀) → ○♢∃z.ψ` +1. That `φ(x₀) → ○AF∃z.ψ` Assume `∀xᵢ.φᵢ(xᵢ) → •∃zᵢ.ψᵢ(xᵢ,zᵢ), 1 ≤ i ≤ n` are all the one-step axioms in the definition, and `P -> o ⋁ᵢ ∃xᵢ.⌈P ∧ φᵢ(xᵢ)⌉ ∧ ∃zᵢ.ψᵢ(xᵢ,zᵢ)` @@ -298,14 +331,14 @@ to apply all axioms (i.e., the lhs of the last conjunct) is not equivalent to ` We want to prove that from the STEP rule and ``` -(∀z₁.∃x₁.ψ₁(x₁,z₁) ∧ ⌈φ(x₀) ∧ φ₁(x₁)⌉ → ♢∃z.ψ(x₀,z)) ∧ … ∧ (∀zₙ.∃xₙ.ψₙ(xₙ,zₙ) ∧ ⌈φ(x₀) ∧ φₙ(xₙ)⌉ → ♢∃z.ψ(x₀,z)) +(∀z₁.∃x₁.ψ₁(x₁,z₁) ∧ ⌈φ(x₀) ∧ φ₁(x₁)⌉ → AF∃z.ψ(x₀,z)) ∧ … ∧ (∀zₙ.∃xₙ.ψₙ(xₙ,zₙ) ∧ ⌈φ(x₀) ∧ φₙ(xₙ)⌉ → AF∃z.ψ(x₀,z)) ``` -we can derive `φ(x₀) → ○♢∃z.ψ(x₀,z)` +we can derive `φ(x₀) → ○AF∃z.ψ(x₀,z)` -This would allow us to replace the goal `φ(x₀) → ○♢∃z.ψ(x₀,z)` with the set of goals +This would allow us to replace the goal `φ(x₀) → ○AF∃z.ψ(x₀,z)` with the set of goals ``` -{ ∀zᵢ.ψᵢ(tᵢ(x₀),zᵢ) ∧ pᵢ(tᵢ(x₀)) → ♢∃z.ψ(x₀,z) : 1 ≤ i ≤ n } +{ ∀zᵢ.ψᵢ(tᵢ(x₀),zᵢ) ∧ pᵢ(tᵢ(x₀)) → AF∃z.ψ(x₀,z) : 1 ≤ i ≤ n } ``` _Proof:_ @@ -317,17 +350,17 @@ Apply `(STEP)` on `φ(x₀)`, and we obtain that We can replace our goal succesively with: ``` -o ⋁ᵢ ∃xᵢ.⌈φ(x₀) ∧ φᵢ(xᵢ)⌉ ∧ ∃zᵢ.ψᵢ(xᵢ,zᵢ) → ○♢∃z.ψ(x₀, z) // transitivity of → -⋁ᵢ ∃xᵢ.⌈φ(x₀) ∧ φᵢ(xᵢ)⌉ ∧ ∃zᵢ.ψᵢ(xᵢ,zᵢ) → ♢∃z.ψ(x₀, z) // framing on ○ -∃xᵢ.⌈φ(x₀) ∧ φᵢ(xᵢ)⌉ ∧ ∃zᵢ.ψᵢ(xᵢ,zᵢ) → ♢∃z.ψ(x₀, z) for all i +o ⋁ᵢ ∃xᵢ.⌈φ(x₀) ∧ φᵢ(xᵢ)⌉ ∧ ∃zᵢ.ψᵢ(xᵢ,zᵢ) → ○AF∃z.ψ(x₀, z) // transitivity of → +⋁ᵢ ∃xᵢ.⌈φ(x₀) ∧ φᵢ(xᵢ)⌉ ∧ ∃zᵢ.ψᵢ(xᵢ,zᵢ) → AF∃z.ψ(x₀, z) // framing on ○ +∃xᵢ.⌈φ(x₀) ∧ φᵢ(xᵢ)⌉ ∧ ∃zᵢ.ψᵢ(xᵢ,zᵢ) → AF∃z.ψ(x₀, z) for all i ``` #### Summary of applying the claims - Check that the remainder `φ(x₀) ∧ ¬p₁(t₁(x₀)) ∧ … ∧ ¬pₙ(tₙ(x₀)))` is equivalent to `⟂` -- Replace the goal `φ(x₀) → ○♢∃z.ψ(x₀,z)` by the set of goals +- Replace the goal `φ(x₀) → ○AF∃z.ψ(x₀,z)` by the set of goals ``` - { ∀zᵢ.ψᵢ(tᵢ(x₀),zᵢ) ∧ pᵢ(tᵢ(x₀)) → ♢∃z.ψ(x₀,z) : 1 ≤ i ≤ n } + { ∀zᵢ.ψᵢ(tᵢ(x₀),zᵢ) ∧ pᵢ(tᵢ(x₀)) → AF∃z.ψ(x₀,z) : 1 ≤ i ≤ n } ``` ## Algorithms @@ -349,14 +382,14 @@ never being applied and the proof looping (and branching) forever. __Input:__ - set of variables `x` -- claim group `(φ₁(x) → ♢∃z.ψ₁(x,z)) ∧ ... ∧ (φₙ(x) → ♢∃z.ψₙ(x,z))` +- claim group `(φ₁(x) → AF∃z.ψ₁(x,z)) ∧ ... ∧ (φₙ(x) → AF∃z.ψₙ(x,z))` - decreasing `measure(x)` __Output:__ Proved or Unproved * Fix an instance `x₀` for the variables `x` -* Let `claims ::= { ∀ x . φᵢ(x) ∧ measure(x) =Int 0` * Let `claimsᵢ ::= claims ∪ { claimᵢ₁, ..., claimᵢₖ }` * Let `Goals := { φᵢ(x₀) }` @@ -385,7 +418,7 @@ is equivalent to `φ ∧ ¬pᵢ[tᵢ/xᵢ]`. __Input:__: goal `φ` and set of tuples `{ (xᵢ,φᵢ,zᵢ,ψᵢ) : 1 ≤ i ≤ n }` representing either -* extended claims `{ ∀xᵢ.φᵢ → ♢∃zᵢ.ψᵢ : 1 ≤ i ≤ n }`, or +* extended claims `{ ∀xᵢ.φᵢ → AF∃zᵢ.ψᵢ : 1 ≤ i ≤ n }`, or * axioms `{ ∀xᵢ.φᵢ → •∃zᵢ.ψᵢ : 1 ≤ i ≤ n }` __Output:__ `(Goals, goalᵣₑₘ)` @@ -394,19 +427,19 @@ __Output:__ `(Goals, goalᵣₑₘ)` * Let `Goals := { ∀z₁.(∃x₁.ψ₁ ∧ ⌈φ∧φ₁⌉), … , ∀zₙ.(∃xₙ.ψₙ ∧ ⌈φ∧φₙ⌉) }` __Note__: `∀zᵢ.(∃xᵢ.ψᵢ ∧ ⌈φ∧φᵢ⌉)` is obtained from -`(∃xᵢ.(∃zᵢ.ψᵢ) ∧ ⌈φ∧φᵢ⌉) → ♢∃z.ψ` +`(∃xᵢ.(∃zᵢ.ψᵢ) ∧ ⌈φ∧φᵢ⌉) → AF∃z.ψ` __Note__: If the unfication condition `⌈φ ∧ φᵢ⌉ = (xᵢ=tᵢ)∧ pᵢ` with `tᵢ` functional, `pᵢ` predicate, and `tᵢ` free of `xi`. -Then the goal `∀zᵢ.(∃xᵢ.ψᵢ ∧ ⌈φ∧φᵢ⌉) → ♢∃z.ψ` -is equivalent to `∀zᵢ.ψᵢ[tᵢ/xᵢ] ∧ pᵢ[tᵢ/xᵢ] → ♢∃z.ψ`. +Then the goal `∀zᵢ.(∃xᵢ.ψᵢ ∧ ⌈φ∧φᵢ⌉) → AF∃z.ψ` +is equivalent to `∀zᵢ.ψᵢ[tᵢ/xᵢ] ∧ pᵢ[tᵢ/xᵢ] → AF∃z.ψ`. Similarly `goalᵣₑₘ := (φ ∧ ¬∃x₁.⌈φ∧φ₁⌉ ∧ … ∧ ¬∃xₙ.⌈φ∧φₙ⌉)` is equivalent to `(φ ∧ ⋀ⱼ ¬pⱼ[tⱼ/xⱼ])` where `j` ranges over the set `{ i : 1 ≤ i ≤ n, φ unifies with φᵢ }`. __Note__: If `φ` does not unify with `φᵢ`, then `⌈φ∧φᵢ⌉ = ⊥`, hence -the goal `∀x∪zᵢ.(∃xᵢ.ψᵢ ∧ ⌈φᵢʳᵉᵐ∧φᵢ⌉) → ♢∃z.ψ` is equivalent to -`∀x.⊥ → ♢∃z.ψ` which can be discharged immediately. Also, in the +the goal `∀x∪zᵢ.(∃xᵢ.ψᵢ ∧ ⌈φᵢʳᵉᵐ∧φᵢ⌉) → AF∃z.ψ` is equivalent to +`∀x.⊥ → AF∃z.ψ` which can be discharged immediately. Also, in the remainder `¬∃x₁.⌈φ∧φ₁⌉ = ⊤` so the conjunct can be removed. From edef26b129a0efb8878b08671cb3a8094b57d65e Mon Sep 17 00:00:00 2001 From: Traian-Florin Serbanuta Date: Tue, 29 Nov 2022 12:58:13 +0200 Subject: [PATCH 4/9] More proofs --- ...Corectness-All-Path-Reachability-Proofs.md | 302 +++++++++++++----- 1 file changed, 226 insertions(+), 76 deletions(-) diff --git a/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md b/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md index 01249d5991..c225b30fa2 100644 --- a/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md +++ b/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md @@ -9,80 +9,230 @@ claims](2019-03-28-All-Path-Reachability-Proofs.md)_ Definitions ----------- -In the following, by abuse of notation, we will identify a formula with the set -of configurations it denotes, thus equality between formulae would mean that -they are equisatisfiable (they denote the same set of configurations). - ### All-path finally -Given a formula `φ`, let `AFφ` denote the formula “all-path finally” `φ`, -defined by: +Given a formula `φ`, let `AFφ` denote the formula “all-path finally” `φ`, whose +intended semantics is: "the set of configurations for which on all paths, +in a finite number of steps, `φ` holds". +Let us will first show that `AFφ` can be described by the formula ``` AFφ := μX.φ ∨ (○X ∧ •⊤) ``` -#### Semantics of `AFφ` - -By the definition above, `AFφ` is semantically defined as `LFP(G)`, the -least-fix-point of the following mapping: - -``` -G(X) := φ ∨ (○X ∧ •⊤) -``` - -Note that `G(X)` can be interpreted as the union between the set of -configurations for which `φ` holds and those which are not stuck and whose all -possible transitions lead into `X`. - -Since `AFφ` is a fixed-point of `G`, the identity `G(AFφ) = AFφ` holds, whence -`AFφ = φ ∨ (○AFφ ∧ •⊤)`. - -Moreover, `G` is monotone (`X` occurs in a positive position) and we can show -that the conditions of Kleene's fixed-point theorem are satisfied: -`Gⁿ(⊥) ⊆ Gⁿ⁺¹(⊥)`, because `Gⁿ(⊥)` denotes the set of configurations for which -on all paths, in at most `n-1` steps, `φ` holds. - -Let us argue the above by induction on `n-1`. -- Base case: `G(⊥) = φ ∨ (○⊥ ∧ •⊤) = φ ∨ (¬•¬⊥ ∧ •⊤) = φ ∨ (¬•⊤ ∧ •⊤) = φ ∨ ⊥ = φ`, - so `G(⊥)` is the set of configurations for which `φ` holds. -- Induction case: Assuming `Gⁿ(⊥)` denotes the set of configurations for which - on all paths, in at most `n-1` steps, `φ` holds, `Gⁿ⁺¹(⊥) = G(Gⁿ(⊥))` will be - the union between the set of configurations for which `φ` holds and those - which are not stuck and whose all possible transitions lead into the set of - configurations for which on all paths, in at most `n-1` steps, `φ` holds, but - these are precisely the configurations for which on all paths, in at most `n` - steps, `φ` holds. - -From Kleene's theorem, `AFφ = ⋁ₙGⁿ(⊥)`, whence, a configuration is in `AFφ` iff -it is in `Gⁿ(⊥)` for some positive integer `n`. By the characterization of -`Gⁿ(⊥)` presented above, it follows that `AFφ` denotes the set of configurations -for which on all paths, in a finite number of steps, `φ` holds. +Let `Top` be the set of all configurations, and let `Prev` be the point-wise +extension of the function mapping a configuration to the set of all +configurations which can reach the given configuration in one step. +and `∁` be the complement operator on sets. + +The semantics of `μX.φ ∨ (○X ∧ •⊤)` is `LFP(G)` where +``` +G(X) := ⟦φ⟧ ∪ ( ∁(Prev(∁(X))) ∩ Prev(Top) ) +``` +Note that, since `X` is positively occurring in the scope of `μ`, `G` is +monotone, so the `LFP(G)` exists and can be defined according to the +Knaster-Tarski formula, as the intersection of all pre-fixpoints of `G`, +that is, all `A` such that `G(A) ⊆ A`. + +Let us also note that `x ∈ G(A)` iff `φ` holds for `x` or `∅ ⊂ Prev⁻¹({x}) ⊆ A`. +Indeed, +``` +x ∈ G(A) ⟺ × ∈ ⟦φ⟧ ∪ ( ∁(Prev(∁(A))) ∩ Prev(Top) +⟺ × ∈ ⟦φ⟧ or (x ∈ ∁(Prev(∁(A))) and x ∈ Prev(Top)) +⟺ × ∈ ⟦φ⟧ or (¬ x ∈ Prev(∁(A)) and ∅ ⊂ Prev⁻¹({x})) +⟺ × ∈ ⟦φ⟧ or (¬ (∃y y ∈ ∁(A) ∧ x ∈ Prev(y)) and ∅ ⊂ Prev⁻¹({x})) +⟺ × ∈ ⟦φ⟧ or (¬ (∃y ¬y ∈ A ∧ x ∈ Prev(y)) and ∅ ⊂ Prev⁻¹({x})) +⟺ × ∈ ⟦φ⟧ or ((∀y y ∈ A ∨ ¬ x ∈ Prev(y)) and ∅ ⊂ Prev⁻¹({x})) +⟺ × ∈ ⟦φ⟧ or ((∀y x ∈ Prev(y) ⟹ y ∈ A) and ∅ ⊂ Prev⁻¹({x})) +⟺ × ∈ ⟦φ⟧ or (Prev⁻¹({x}) ⊆ A and ∅ ⊂ Prev⁻¹({x})) +⟺ × ∈ ⟦φ⟧ or (∅ ⊂ Prev⁻¹({x}) ⊆ A) +``` + +Let `stuck x` be defined as `Prev⁻¹(x) = ∅` and let `x τ y` be defined +as `y ∈ Prev⁻¹({x})`. +We can also express `∅ ⊂ Prev⁻¹({x}) ⊆ A` in terms +of `stuck` and transitions, as `¬ stuck x ∧ ∀y x τ y → y ∈ A`. +Hence, `x ∈ G(A)` if either `x` matches `ϕ`, or `x` is not stuck and all +its transitions go into `A`. + +We can coinductively define (the possibly infinite) complete traces of the +transition system determined by `Prev⁻¹` starting in an element `a` as being: +either just `a`, if `stuck a`, or `a` followed by a trace starting in `b` for +some `b` such that `a τ b`. +Given this definition, the trace semantics for `AF ϕ` is +``` +⟦AF ϕ⟧ ::= { a | forall tr trace starting in a, exists b in tr such that b ∈ ⟦ϕ⟧ } +``` + +Let us first argue that `⟦AF ϕ⟧` is a pre-fixpoint of `G`, i.e., that +`G(⟦AF ϕ⟧) ⊆ ⟦AF ϕ⟧`. +Take `a ∈ G(⟦AF ϕ⟧)`. Then either `a ∈ ⟦ϕ⟧` or `¬ stuck a` and for all `b` +such that `a τ b`, `b ∈ ⟦AF ϕ⟧`. +Let `tr` be a complete trace starting in `a`. +If `a ∈ ⟦ϕ⟧`, then we can choose precisely `a` as the witness on that trace +for which `ϕ` holds. +Otherwise, `¬ stuck a` and for all `b` such that `a τ b`, `b ∈ ⟦AF ϕ⟧`. +Since `¬ stuck a` it must be that `tr` cannot be just `a` (it's complete), so +there must exist a `b` such that `a τ b` and `b` is the start of a trace `tr'` +such that `tr = a ⋅ tr'`. However, since `a τ b`, it follows that`b ∈ ⟦AF ϕ⟧`, +so `tr'` must contain a witness for which `ϕ` holds; that witness is also a +witness for `tr`. + +Let us now argue that `⟦AF ϕ⟧` is a post-fixpoint of `G`, i.e., that +`⟦AF ϕ⟧ ⊆ G(⟦AF ϕ⟧)`. +Take `a ∈ ⟦AF ϕ⟧`. We need to prove that either `a ∈ ⟦ϕ⟧` or `¬ stuck a` and +for all `b` such that `a τ b`, `b ∈ ⟦AF ϕ⟧`, +If `ϕ` holds for `a` then we're done. Assume `a ∉ ⟦ϕ⟧`. +Then it must be that `¬ stuck a`, since otherwise `a` would be a complete trace +starting in `a` with no witness for which `ϕ` holds. +Let now `b` be such `a τ b`. We need to show that `b ∈ ⟦AF ϕ⟧`. Let `tr` be a +complete trace starting in `b`. Then `a ⋅ tr` is a complete trace starting in `a`. +Since `a ∈ ⟦AF ϕ⟧`, there must be a witness in `a ⋅ tr` for which `ϕ` holds. +However, since `ϕ` doesn't hold for `a`, the witness must be part of `tr` +Since `tr` was chosen arbitrarily, it must be that `a ∈ ⟦AF ϕ⟧`. + +Therefore, `⟦AF ϕ⟧` is a fixpoint for `G`. To show that it is the LFP of `G` it +suffices to prove that it is included in any pre-fixpoint of `G`. +Let `A` be a pre-fixpoint of `G`, i.e., `G(A) ⊆ A`. That means that +(1) `A` contains all configurations matching `ϕ`; and +(2) `A` contains all configurations which are not stuck and transition on all + paths into `A` +Assume by contradiction that there exists `a ∈ ⟦AF ϕ⟧` such that `a ∉ A`. +We will coinductively construct a complete trace starting in `a` with no +witness in `A`. Since `A` contains all configurations for which `ϕ` holds, +this would contradict the fact that `a ∈ ⟦AF ϕ⟧`. +- if `stuck a` is stuck, then take the complete trace `a` +- if `¬ stuck a`, since `a ∉ A`, it means that (2) is false; hence it exists + a transition `a τ b` such that `b ∉ A`. Then take the complete trace + `a ⋅ tr` where `tr` is obtained by applying the above process for `b ∉ A`. + +Hence, `⟦AF ϕ⟧` is the LFP of `G`. Let us now study when this LFP can be +expressed according to Kleene's formula, i.e., when `LFP(G) = ⋃ₙGⁿ(∅)`. + +Given a complete trace `tr`, let `trₙ` be the `n`th element of the trace, if +it exists. + +Let us now argue that, for any natural `n`, `Gⁿ⁺¹(∅)` denotes the set of +configurations for which, in at most `n` steps, on all paths, `φ` holds, i.e., +``` +Gⁿ⁺¹(∅) = { a | forall tr trace starting in a, exists k ≤ n such that trₖ ∈ ⟦ϕ⟧ } +``` +We do that by induction on `n`: +- Base case: + ``` + G(∅) = ⟦φ⟧ ∪ ( ∁(Prev(∁(∅))) ∩ Prev(Top) ) + = ⟦φ⟧ ∪ ( ∁(Prev(Top)) ∩ Prev(Top) ) + = ⟦φ⟧ ∪ ∅ + = ⟦φ⟧ + = {a | a ∈ ⟦ϕ⟧} + = { a | forall tr trace starting in a, exists k ≤ 0 such that trₖ ∈ ⟦ϕ⟧} + ``` +- Induction case. + `a ∈ Gⁿ⁺²(∅) = G(Gⁿ⁺¹(∅))` iff `φ` holds for `a` or `¬ stuck a` and forall b + such that `a τ b`, `b ∈ Gⁿ⁺¹(∅)`. + Let `tr` be a complete trace starting in `a`. If the trace is just `a`, + then it must be that `a` is stuck, therefore `\phi` holds for `a` and since + `0 ≤ n+1` we are done. Otherwise assume `tr = a ⋅ tr'` such that `tr'` is a + complete trace starting in a configuration `b`. Then `a τ b`, hence `b ∈ Gⁿ⁺¹(∅)`. + By the induction hypothesis, there exists `k ≤ n` such that `tr'ₖ ∈ ⟦ϕ⟧`, hence + `trₖ₊₁ ∈ ⟦ϕ⟧`. + Conversely, let `a` be such that forall `tr` trace starting in a, there exists + `k ≤ 0` such that `trₖ ∈ ⟦ϕ⟧`. If `a ∈ ⟦ϕ⟧`, then `a ∈ G(Gⁿ⁺¹(∅))`. Suppose + `a ∉ ⟦ϕ⟧`. Then `¬ stuck a` (otherwise `a` would be a trace starting in `a` + for which the hypothesis would not hold). Let `b` be such `a τ b`. + +Since `G` is monotone, we can deduce that `Gⁿ(∅) ⊆ Gⁿ⁺¹(∅)` +(obviously `∅ ⊆ G(∅)` and then by applying monotone G `n` times). +Therefore, the limit `⋁ₙGⁿ(∅)` exists. + +By the characterization of `Gⁿ(∅)` presented above, it follows that `⋁ₙGⁿ(∅)` +denotes the set of configurations for which there exists `n` such that in at +most `n` steps, on all paths, `φ` holds, i.e., +``` +⋁ₙGⁿ(∅) = { a | ∃ n, a ∈ Gⁿ⁺¹(∅)} + = { a | ∃n ∀tr tr₀ = a → ∃k k ≤ n ∧ trₖ ∈ ⟦ϕ⟧ } +``` +Note that there is a slight difference from the semantics intended for `AF ϕ`: +`⟦AF ϕ⟧ = { a | ∀tr tr₀ = a → ∃k trₖ ∈ ⟦ϕ⟧` + +Nevertheless, it is relatively easy to see that `⋁ₙGⁿ(∅)` is a subset of `⟦AF ϕ⟧`, +hence, if we show that it is a fixpoint, then they would be equal. +Also, it's easy to see that `⋁ₙGⁿ(∅)` is a post-fixpoint. +We have that for all `n`, `Gⁿ(∅) ⊆ ⋁ₙGⁿ(∅)` and since `G` is monotone, +`Gⁿ⁺¹(∅) ⊆ G(⋁ₙGⁿ(∅))`. Also, obviously `G⁰(∅) = ∅ ⊆ G(⋁ₙGⁿ(∅))`. +Therefore, `⋁ₙGⁿ(∅) ⊆ G(⋁ₙGⁿ(∅))`. + +It remains to show that `⋁ₙGⁿ(∅)` is a pre-fixpoint, i.e., that +`G(⋁ₙGⁿ(∅)) ⊆ ⋁ₙGⁿ(∅)`, or `G(⋁ₙGⁿ(∅)) ∖ ⋁ₙGⁿ(∅) = ∅`. +We have that: +``` +x ∈ G(⋁ₙGⁿ(∅)) ∖ ⋁ₙGⁿ(∅) +⟺ x ∈ G(⋁ₙGⁿ(∅)) and x ∉ ⋁ₙGⁿ(∅) +⟺ (x ∈ ⟦φ⟧ or ¬ stuck x and ∀y x τ y → y ∈ ⋁ₙGⁿ(∅)) and x ∉ ⋁ₙGⁿ(∅) +⟺ ¬ stuck x and (∀y x τ y → y ∈ ⋁ₙGⁿ(∅)) and x ∉ ⋁ₙGⁿ(∅) (since ⟦φ⟧ ⊆ ⋁ₙGⁿ(∅)) +``` + +Given the above relation, we deduce that a sufficient condition ensuring that +`G(⋁ₙGⁿ(∅)) ∖ ⋁ₙGⁿ(∅) = ∅` is that the transition system is finitely branching, +i.e., that `Prev⁻¹({x})` is finite for any `x`. Indeed, suppose +there exists `x ∈ G(⋁ₙGⁿ(∅)) ∖ ⋁ₙGⁿ(∅)`. Then, it must hold that +`¬ stuck x` and `(∀y x τ y → y ∈ ⋁ₙGⁿ(∅))` and `x ∉ ⋁ₙGⁿ(∅)` +Let `k`, `y₁`, ..., `yₖ` be such that `Prev⁻¹({x}) = {y₁, ..., yₖ}`. +For any `i`, `yᵢ ∈ Prev⁻¹({x})`, hence `x τ yᵢ`, therefore `∃nᵢ yᵢ ∈ Gⁿⁱ(∅)`. +Let `n₁`, ..., `nₖ` be such that `yᵢ ∈ Gⁿⁱ(∅)` for any `1≤i≤k`. +Let `m = 𝐦𝐚𝐱 {n₁, ... , nₖ}`. Since `(Gⁿ(∅))ₙ` is an ascending chain, +it follows that `yᵢ ∈ Gᵐ(∅)` for any `1≤i≤k`, +whence `x ∈ Gᵐ⁺¹(∅)`, contradiction with the fact that `x ∉ ⋁ₙGⁿ(∅)`. + +Nevertheless, before continuing, let +us give an example of a system and property for which the above construction is +not a fixpoint. + +#### Counterexample for `⟦AF ϕ⟧ = ⋁ₙGⁿ(∅)` + +Consider the following K theory + +``` +syntax KItem ::= "x" + +rule Y:Int => Y -Int 1 requires Y>0 +rule x => ?Y:Int ensures Y >= 0 +``` + +and the claim `x → AF 0` + +It is easy to see that any trace originating in `x` will reach `0` in a finite +number of steps. However, there is no bound on the number of steps needed for `x` +to reach `0`. ### Total corectness all-path reachability claims -Given this definition of all-path finally, a total corectness all-path +Given this definition of all-path finally, a total correctness all-path reachability claim is of the form ``` -∀x.φ(x) → AF∃z.ψ(x,z) +∀x.φ(x) → AF ∃z.ψ(x,z) ``` and basically states that from any configuration `γ` satisfying `φ(x)` for some `x`, a configuration satisfying `ψ(x,z)` for some `z` will be reached in a finite number of steps on any path. +If the system is finitely branching, the claim becomes stronger: +for any configuration `γ` satisfying `φ(x)` for some `x`, there exists a bound +on the number of steps required to reach a configuration satisfying `ψ(x,z)` +for some `z` on any path. Since the configuration is reached after a finite number of steps, -such reachability claims guarantee total corectness. +such reachability claims guarantee termination, thus total correctness. Problem Description ------------------- -Given a set of reachability claims, of the form `∀x.φ(x) → AF∃z.ψ(x,z)`, +Given a set of reachability claims, of the form `∀x.φ(x) → AF ∃z.ψ(x,z)`, we are trying to prove all of them together, by well-founded induction on a given `measure` defined on the quantified variables `x`. The well-founded induction argument requiring the `measure` to decrease before -applying a claim as a circularity replaces the coinductive argument requiring -that progress is made before applying a circularity. +applying a claim as an induction hypothesis replaces the coinductive argument +requiring that progress is made before applying a circularity. ## Proposal of syntax changes @@ -101,7 +251,7 @@ claim group . . . - claim φᵢ(x) → AF∃zᵢ.ψᵢ(x,zᵢ) [using(claimᵢ₁, ..., claimᵢₖ)] + claim φᵢ(x) → AF ∃zᵢ.ψᵢ(x,zᵢ) [using(claimᵢ₁, ..., claimᵢₖ)] . . . @@ -125,7 +275,7 @@ have already been proven. Assume also a given integer pattern `measure(x)`, over the same variables as the claims in the group. Since we're proving all claims together, we can gather them in a single goal, -`P(x) ::= (φ₁(x) → AF∃z.ψ₁(x,z)) ∧ ... ∧ (φₙ(x) → AF∃z.ψₙ(x,z))`. +`P(x) ::= (φ₁(x) → AF ∃z.ψ₁(x,z)) ∧ ... ∧ (φₙ(x) → AF ∃z.ψₙ(x,z))`. A well-founded induction principle allowing to prove `P` using `measure` would be of the form @@ -146,19 +296,19 @@ hypothesis `forall x, 0 <= measure(x) < measure(x0) -> P(x)`, we need to prove By first-order manipulation we can transform the induction hypothesis for `P` into a set of induction hypotheses, one for each claim: ``` -∀x. φᵢ(x) ∧ 0 ≤ measure(x) < measure(x₀) → AF∃z.ψᵢ(x,z) +∀x. φᵢ(x) ∧ 0 ≤ measure(x) < measure(x₀) → AF ∃z.ψᵢ(x,z) ``` -Similarly we can split the goal into a separate goal `φᵢ(x₀) → AF∃z.ψᵢ(x₀,z)` +Similarly we can split the goal into a separate goal `φᵢ(x₀) → AF ∃z.ψᵢ(x₀,z)` for each claim. Since we might be using the claims to advance the proof of the claim, to avoid confusion (and to reduce caring about indices) we will denote a goal with -`φ(x₀) → AF∃z.ψ(x₀,z)` in all subsequent steps, although the exact goal might +`φ(x₀) → AF ∃z.ψ(x₀,z)` in all subsequent steps, although the exact goal might change from one step to the next. Moreover, we will consider the induction hypotheses to be derived claims to -be applied as circularities, and denote them as `∀x. φᵢ(x) → AF∃z.ψᵢ(x,z)`, +be applied as circularities, and denote them as `∀x. φᵢ(x) → AF ∃z.ψᵢ(x,z)`, where `φᵢ(x)` also contains the guard `0 ≤ measure(x) < measure(x₀)`. ### Background on unification and remainders of unification @@ -215,9 +365,9 @@ First, let us eliminate the case when the conclusion holds now. We have the following sequence of equivalent claims: ``` -φ(x₀) → AF∃z.ψ(x₀,z) -(φ(x₀) ∧ ∃z.ψ(x₀, z)) ∨ (φ(x₀) ∧ ¬∃z.ψ(x₀, z)) → AF∃z.ψ(x₀,z) -(φ(x₀) ∧ ∃z.ψ(x₀, z) → AF∃z.ψ(x₀,z)) ∧ (φ(x₀) ∧ ¬∃z.ψ(x₀, z) → AF∃z.ψ(x₀,z)) +φ(x₀) → AF ∃z.ψ(x₀,z) +(φ(x₀) ∧ ∃z.ψ(x₀, z)) ∨ (φ(x₀) ∧ ¬∃z.ψ(x₀, z)) → AF ∃z.ψ(x₀,z) +(φ(x₀) ∧ ∃z.ψ(x₀, z) → AF ∃z.ψ(x₀,z)) ∧ (φ(x₀) ∧ ¬∃z.ψ(x₀, z) → AF ∃z.ψ(x₀,z)) ``` The first conjunct, `φ(x₀) ∧ ∃z.ψ(x₀, z) → AF∃z.ψ(x₀,z)` can be discharged by @@ -239,28 +389,28 @@ If `φ(x₀)` is equivalent to `⊥`, then the implication holds and we are done ### Applying (extended) claims Since both circularities (induction hypotheses) and already proven claims are of -the form `∀x.φᵢ(x) → AF∃z.ψᵢ(x,z)`, we will refer to all as extended claims. -Let `∀x.φᵢ(x) → AF∃z.ψᵢ(x,z)` denote the ith induction hypothesis or already +the form `∀x.φᵢ(x) → AF ∃z.ψᵢ(x,z)`, we will refer to all as extended claims. +Let `∀x.φᵢ(x) → AF ∃z.ψᵢ(x,z)` denote the ith induction hypothesis or already proven claim. ``` -φ(x₀) → AF∃z.ψ(x₀,z) -φ(x₀) ∧ (∃x.φ₁(x) ∨ … ∨ ∃x.φₙ(x) ∨ (¬∃x.φ₁(x) ∧ … ∧ ¬∃x.φₙ(x))) → AF∃z.ψ(x₀,z) -(φ(x₀) ∧ ∃x.φ₁(x)) ∨ … ∨ (φ(x₀) ∧ ∃x.φₙ(x)) ∨ (φ(x₀) ∧ (¬∃x.φ₁(x) ∧ … ∧ ¬∃x.φₙ(x))) → AF∃z.ψ(x₀,z) -(φ(x₀) ∧ ∃x.φ₁(x) → AF∃z.ψ(x₀,z)) ∧ … (φ(x₀) ∧ ∃x.φₙ(x) → AF∃z.ψ(x₀,z)) - ∧ (φ(x₀) ∧ (¬∃x.φ₁(x) ∧ … ∧ ¬∃x.φₙ(x)) → AF∃z.ψ(x₀,z)) +φ(x₀) → AF ∃z.ψ(x₀,z) +φ(x₀) ∧ (∃x.φ₁(x) ∨ … ∨ ∃x.φₙ(x) ∨ (¬∃x.φ₁(x) ∧ … ∧ ¬∃x.φₙ(x))) → AF ∃z.ψ(x₀,z) +(φ(x₀) ∧ ∃x.φ₁(x)) ∨ … ∨ (φ(x₀) ∧ ∃x.φₙ(x)) ∨ (φ(x₀) ∧ (¬∃x.φ₁(x) ∧ … ∧ ¬∃x.φₙ(x))) → AF ∃z.ψ(x₀,z) +(φ(x₀) ∧ ∃x.φ₁(x) → AF ∃z.ψ(x₀,z)) ∧ … (φ(x₀) ∧ ∃x.φₙ(x) → AF ∃z.ψ(x₀,z)) + ∧ (φ(x₀) ∧ (¬∃x.φ₁(x) ∧ … ∧ ¬∃x.φₙ(x)) → AF ∃z.ψ(x₀,z)) ``` assuming that `⌈φ(x₀) ∧ φᵢ(x)⌉ ≡ (x = tᵢ(x₀)) ∧ pᵢ(x₀, x)` for each `i`, the above is equivalent with: ``` -(φ₁(t₁(x₀)) ∧ p₁(x₀, t₁(x₀)) → AF∃z.ψ(x₀,z)) ∧ … (φₙ(tₙ(x₀)) ∧ pₙ(x₀, tₙ(x₀)) → AF∃z.ψ(x₀,z)) - ∧ (φ(x₀) ∧ ¬p₁(x₀, t₁(x₀)) ∧ … ∧ ¬pₙ(x₀, tₙ(x₀)) → AF∃z.ψ(x₀,z)) +(φ₁(t₁(x₀)) ∧ p₁(x₀, t₁(x₀)) → AF ∃z.ψ(x₀,z)) ∧ … (φₙ(tₙ(x₀)) ∧ pₙ(x₀, tₙ(x₀)) → AF∃z.ψ(x₀,z)) + ∧ (φ(x₀) ∧ ¬p₁(x₀, t₁(x₀)) ∧ … ∧ ¬pₙ(x₀, tₙ(x₀)) → AF ∃z.ψ(x₀,z)) ``` This can be split into proving a goal for each extended claim, ``` -φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → AF∃z.ψ(x₀,z) +φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → AF ∃z.ψ(x₀,z) ``` and one for the remainder ``` @@ -273,18 +423,18 @@ the negation of the measure check for each induction hypothesis, of the form #### Using a claim to advance the corresponding goal -Assume `φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → AF∃z.ψ(x₀,z)` goal to be proven -and let `∀x. φᵢ(x) → AF∃z.ψᵢ(x,z)` be the corresponding extended claim. +Assume `φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → AF ∃z.ψ(x₀,z)` goal to be proven +and let `∀x. φᵢ(x) → AF ∃z.ψᵢ(x,z)` be the corresponding extended claim. By instatiating the claim with `x := tᵢ(x₀)`, we obtain -`φᵢ(tᵢ(x₀)) → AF∃z.ψᵢ(tᵢ(x₀),z)`; then, by framing, we obtain -`φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → (AF∃z.ψᵢ(tᵢ(x₀),z)) ∧ pᵢ(x₀, tᵢ(x₀))`. +`φᵢ(tᵢ(x₀)) → AF ∃z.ψᵢ(tᵢ(x₀),z)`; then, by framing, we obtain +`φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → (AF ∃z.ψᵢ(tᵢ(x₀),z)) ∧ pᵢ(x₀, tᵢ(x₀))`. Next, by predicate properties, we can obtain that -`φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → AF∃z.(ψᵢ(tᵢ(x₀),z) ∧ pᵢ(x₀, tᵢ(x₀)))`. +`φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → AF ∃z.(ψᵢ(tᵢ(x₀),z) ∧ pᵢ(x₀, tᵢ(x₀)))`. We can use transitivity of `→` to replace the initial goal with -`AF∃z.ψᵢ(tᵢ(x₀),z) ∧ pᵢ(x₀, tᵢ(x₀)) → AF∃z.ψ(x₀,z)` +`AF ∃z.ψᵢ(tᵢ(x₀),z) ∧ pᵢ(x₀, tᵢ(x₀)) → AF ∃z.ψ(x₀,z)` This goal can soundly be replaced with -`∀z.ψᵢ(tᵢ(x₀),z) ∧ pᵢ(x₀, tᵢ(x₀)) → AF∃z.ψ(x₀,z)` +`∀z.ψᵢ(tᵢ(x₀),z) ∧ pᵢ(x₀, tᵢ(x₀)) → AF ∃z.ψ(x₀,z)` as proving this goal would ensure that the above also holds. #### Summary of applying extended claims @@ -293,8 +443,8 @@ By applying the extended claims, we will replace the existing goal with a set consisting of a goal for each extended claim (some with the hypothesis equivalent with `⟂`) and a remainder. -- Goals associated to extended claims: `∀z.ψᵢ(tᵢ(x₀),z) ∧ pᵢ(x₀, tᵢ(x₀)) → AF∃z.ψ(x₀,z)` -- Goal associated to the remainder: `φ(x₀) ∧ ¬p₁(x₀, t₁(x₀)) ∧ … ∧ ¬pₙ(x₀, tₙ(x₀) → AF∃z.ψ(x₀,z))` +- Goals associated to extended claims: `∀z.ψᵢ(tᵢ(x₀),z) ∧ pᵢ(x₀, tᵢ(x₀)) → AF ∃z.ψ(x₀,z)` +- Goal associated to the remainder: `φ(x₀) ∧ ¬p₁(x₀, t₁(x₀)) ∧ … ∧ ¬pₙ(x₀, tₙ(x₀) → AF ∃z.ψ(x₀,z))` By abuse of notation, let `φ(x₀)` denote `φ(x₀) ∧ ¬p₁(x₀, t₁(x₀)) ∧ … ∧ ¬pₙ(x₀, tₙ(x₀)` ### Applying axioms From 7e659e8bf3ffcdd5442784d6cb6ce95e939bd449 Mon Sep 17 00:00:00 2001 From: Traian-Florin Serbanuta Date: Tue, 29 Nov 2022 17:00:32 +0200 Subject: [PATCH 5/9] Typos --- ...Corectness-All-Path-Reachability-Proofs.md | 40 ++++++++++--------- 1 file changed, 21 insertions(+), 19 deletions(-) diff --git a/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md b/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md index c225b30fa2..2dd415d80f 100644 --- a/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md +++ b/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md @@ -1,10 +1,10 @@ -Proving Total Corectness All-Path Reachability Claims +Proving Total Correctness All-Path Reachability Claims ===================================================== -This document details Total Corectness All-Path Reachability. +This document details Total Correctness All-Path Reachability. -_Prepared by Traian Șerbănuță, based on [proving All-Path Reachability -claims](2019-03-28-All-Path-Reachability-Proofs.md)_ +_Prepared by Traian Șerbănuță and Virgil Șerbănuță, +based on [proving All-Path Reachability claims](2019-03-28-All-Path-Reachability-Proofs.md)_ Definitions ----------- @@ -188,7 +188,7 @@ Nevertheless, before continuing, let us give an example of a system and property for which the above construction is not a fixpoint. -#### Counterexample for `⟦AF ϕ⟧ = ⋁ₙGⁿ(∅)` +### Counterexample for `⟦AF ϕ⟧ = ⋁ₙGⁿ(∅)` Consider the following K theory @@ -205,10 +205,10 @@ It is easy to see that any trace originating in `x` will reach `0` in a finite number of steps. However, there is no bound on the number of steps needed for `x` to reach `0`. -### Total corectness all-path reachability claims +### Total correctness all-path reachability claims -Given this definition of all-path finally, a total correctness all-path -reachability claim is of the form +Given the definition of all-path finally discussed in the section above, +a total correctness all-path reachability claim is of the form ``` ∀x.φ(x) → AF ∃z.ψ(x,z) ``` @@ -230,9 +230,9 @@ Given a set of reachability claims, of the form `∀x.φ(x) → AF ∃z.ψ(x,z)` we are trying to prove all of them together, by well-founded induction on a given `measure` defined on the quantified variables `x`. -The well-founded induction argument requiring the `measure` to decrease before -applying a claim as an induction hypothesis replaces the coinductive argument -requiring that progress is made before applying a circularity. +The well-founded induction argument, which requires the `measure` to decrease before +applying a claim as an induction hypothesis, will replace the coinductive argument, +which requires that progress is made before applying a circularity. ## Proposal of syntax changes @@ -240,9 +240,9 @@ requiring that progress is made before applying a circularity. needed to complete their proof; this induces a dependency relation - claims which are part of a dependency cycle (including self-dependencies) would need to be specified together as a "claim group" -- a claim group would need to provide a metric on their input variables, which - would be used as part of the decreasingness guard whenever one tries to apply - a claim from the group during the proof of one the claims in the group +- a claim group would need to provide a metric on their input variables; + this metric must decrease whenever one tries to apply a claim from the group + while proving a claim from the same group A claim group would be something like ``` @@ -267,12 +267,13 @@ variables would need to be implemented. ## Approach -For the algorithms derived by the present approach, please see next section. +For the algorithms derived from the present approach, please check the next section. Assume we want to prove a group of claims defined over the same set of variables -`x`. Further assume that all claims not in group on which these claims depend -have already been proven. Assume also a given integer pattern `measure(x)`, -over the same variables as the claims in the group. +`x`. Further assume that all other claims (which are not in the current group) + on which these claims depend have already been proven. + Assume also a given integer pattern `measure(x)`, over the same variables as + the claims in the group. Since we're proving all claims together, we can gather them in a single goal, `P(x) ::= (φ₁(x) → AF ∃z.ψ₁(x,z)) ∧ ... ∧ (φₙ(x) → AF ∃z.ψₙ(x,z))`. @@ -322,7 +323,8 @@ allows their term part `t` to be undefined. _Extended constructor patterns_ will be those extended function-like patterns for which `t` is a functional term, composed out of constructor-like symbols -and variables. +and variables. This definition can be extended to include AC constructors, e.g. +map concatenation __Note:__ From 8510629c43d6ab0e6a80917c623d301d1d4251bb Mon Sep 17 00:00:00 2001 From: Traian-Florin Serbanuta Date: Tue, 29 Nov 2022 18:10:27 +0200 Subject: [PATCH 6/9] Refactoring --- ...Corectness-All-Path-Reachability-Proofs.md | 274 +++++++++--------- 1 file changed, 143 insertions(+), 131 deletions(-) diff --git a/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md b/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md index 2dd415d80f..7f068ea111 100644 --- a/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md +++ b/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md @@ -15,10 +15,8 @@ Given a formula `φ`, let `AFφ` denote the formula “all-path finally” `φ`, intended semantics is: "the set of configurations for which on all paths, in a finite number of steps, `φ` holds". -Let us will first show that `AFφ` can be described by the formula -``` -AFφ := μX.φ ∨ (○X ∧ •⊤) -``` +In this section we will show that `AFφ` can be captured by the interpretation of +the fixed-point `μX.φ ∨ (○X ∧ •⊤)` Let `Top` be the set of all configurations, and let `Prev` be the point-wise extension of the function mapping a configuration to the set of all @@ -31,7 +29,7 @@ G(X) := ⟦φ⟧ ∪ ( ∁(Prev(∁(X))) ∩ Prev(Top) ) ``` Note that, since `X` is positively occurring in the scope of `μ`, `G` is monotone, so the `LFP(G)` exists and can be defined according to the -Knaster-Tarski formula, as the intersection of all pre-fixpoints of `G`, +Knaster-Tarski formula, as the intersection of all pre-fixed-points of `G`, that is, all `A` such that `G(A) ⊆ A`. Let us also note that `x ∈ G(A)` iff `φ` holds for `x` or `∅ ⊂ Prev⁻¹({x}) ⊆ A`. @@ -52,158 +50,66 @@ Let `stuck x` be defined as `Prev⁻¹(x) = ∅` and let `x τ y` be defined as `y ∈ Prev⁻¹({x})`. We can also express `∅ ⊂ Prev⁻¹({x}) ⊆ A` in terms of `stuck` and transitions, as `¬ stuck x ∧ ∀y x τ y → y ∈ A`. -Hence, `x ∈ G(A)` if either `x` matches `ϕ`, or `x` is not stuck and all +Hence, `x ∈ G(A)` if either `x` matches `φ`, or `x` is not stuck and all its transitions go into `A`. We can coinductively define (the possibly infinite) complete traces of the transition system determined by `Prev⁻¹` starting in an element `a` as being: either just `a`, if `stuck a`, or `a` followed by a trace starting in `b` for some `b` such that `a τ b`. -Given this definition, the trace semantics for `AF ϕ` is +Given this definition, the trace semantics for `AF φ` is ``` -⟦AF ϕ⟧ ::= { a | forall tr trace starting in a, exists b in tr such that b ∈ ⟦ϕ⟧ } +⟦AF φ⟧ ::= { a | forall tr trace starting in a, exists b in tr such that b ∈ ⟦φ⟧ } ``` -Let us first argue that `⟦AF ϕ⟧` is a pre-fixpoint of `G`, i.e., that -`G(⟦AF ϕ⟧) ⊆ ⟦AF ϕ⟧`. -Take `a ∈ G(⟦AF ϕ⟧)`. Then either `a ∈ ⟦ϕ⟧` or `¬ stuck a` and for all `b` -such that `a τ b`, `b ∈ ⟦AF ϕ⟧`. +Let us first argue that `⟦AF φ⟧` is a pre-fixed-point of `G`, i.e., that +`G(⟦AF φ⟧) ⊆ ⟦AF φ⟧`. +Take `a ∈ G(⟦AF φ⟧)`. Then either `a ∈ ⟦φ⟧` or `¬ stuck a` and for all `b` +such that `a τ b`, `b ∈ ⟦AF φ⟧`. Let `tr` be a complete trace starting in `a`. -If `a ∈ ⟦ϕ⟧`, then we can choose precisely `a` as the witness on that trace -for which `ϕ` holds. -Otherwise, `¬ stuck a` and for all `b` such that `a τ b`, `b ∈ ⟦AF ϕ⟧`. +If `a ∈ ⟦φ⟧`, then we can choose precisely `a` as the witness on that trace +for which `φ` holds. +Otherwise, `¬ stuck a` and for all `b` such that `a τ b`, `b ∈ ⟦AF φ⟧`. Since `¬ stuck a` it must be that `tr` cannot be just `a` (it's complete), so there must exist a `b` such that `a τ b` and `b` is the start of a trace `tr'` -such that `tr = a ⋅ tr'`. However, since `a τ b`, it follows that`b ∈ ⟦AF ϕ⟧`, -so `tr'` must contain a witness for which `ϕ` holds; that witness is also a +such that `tr = a ⋅ tr'`. However, since `a τ b`, it follows that`b ∈ ⟦AF φ⟧`, +so `tr'` must contain a witness for which `φ` holds; that witness is also a witness for `tr`. -Let us now argue that `⟦AF ϕ⟧` is a post-fixpoint of `G`, i.e., that -`⟦AF ϕ⟧ ⊆ G(⟦AF ϕ⟧)`. -Take `a ∈ ⟦AF ϕ⟧`. We need to prove that either `a ∈ ⟦ϕ⟧` or `¬ stuck a` and -for all `b` such that `a τ b`, `b ∈ ⟦AF ϕ⟧`, -If `ϕ` holds for `a` then we're done. Assume `a ∉ ⟦ϕ⟧`. +Let us now argue that `⟦AF φ⟧` is a post-fixed-point of `G`, i.e., that +`⟦AF φ⟧ ⊆ G(⟦AF φ⟧)`. +Take `a ∈ ⟦AF φ⟧`. We need to prove that either `a ∈ ⟦φ⟧` or `¬ stuck a` and +for all `b` such that `a τ b`, `b ∈ ⟦AF φ⟧`, +If `φ` holds for `a` then we're done. Assume `a ∉ ⟦φ⟧`. Then it must be that `¬ stuck a`, since otherwise `a` would be a complete trace -starting in `a` with no witness for which `ϕ` holds. -Let now `b` be such `a τ b`. We need to show that `b ∈ ⟦AF ϕ⟧`. Let `tr` be a +starting in `a` with no witness for which `φ` holds. +Let now `b` be such `a τ b`. We need to show that `b ∈ ⟦AF φ⟧`. Let `tr` be a complete trace starting in `b`. Then `a ⋅ tr` is a complete trace starting in `a`. -Since `a ∈ ⟦AF ϕ⟧`, there must be a witness in `a ⋅ tr` for which `ϕ` holds. -However, since `ϕ` doesn't hold for `a`, the witness must be part of `tr` -Since `tr` was chosen arbitrarily, it must be that `a ∈ ⟦AF ϕ⟧`. - -Therefore, `⟦AF ϕ⟧` is a fixpoint for `G`. To show that it is the LFP of `G` it -suffices to prove that it is included in any pre-fixpoint of `G`. -Let `A` be a pre-fixpoint of `G`, i.e., `G(A) ⊆ A`. That means that -(1) `A` contains all configurations matching `ϕ`; and +Since `a ∈ ⟦AF φ⟧`, there must be a witness in `a ⋅ tr` for which `φ` holds. +However, since `φ` doesn't hold for `a`, the witness must be part of `tr` +Since `tr` was chosen arbitrarily, it must be that `a ∈ ⟦AF φ⟧`. + +Therefore, `⟦AF φ⟧` is a fixed-point for `G`. To show that it is the LFP of `G` it +suffices to prove that it is included in any pre-fixed-point of `G`. +Let `A` be a pre-fixed-point of `G`, i.e., `G(A) ⊆ A`. That means that +(1) `A` contains all configurations matching `φ`; and (2) `A` contains all configurations which are not stuck and transition on all paths into `A` -Assume by contradiction that there exists `a ∈ ⟦AF ϕ⟧` such that `a ∉ A`. +Assume by contradiction that there exists `a ∈ ⟦AF φ⟧` such that `a ∉ A`. We will coinductively construct a complete trace starting in `a` with no -witness in `A`. Since `A` contains all configurations for which `ϕ` holds, -this would contradict the fact that `a ∈ ⟦AF ϕ⟧`. +witness in `A`. Since `A` contains all configurations for which `φ` holds, +this would contradict the fact that `a ∈ ⟦AF φ⟧`. - if `stuck a` is stuck, then take the complete trace `a` - if `¬ stuck a`, since `a ∉ A`, it means that (2) is false; hence it exists a transition `a τ b` such that `b ∉ A`. Then take the complete trace `a ⋅ tr` where `tr` is obtained by applying the above process for `b ∉ A`. -Hence, `⟦AF ϕ⟧` is the LFP of `G`. Let us now study when this LFP can be -expressed according to Kleene's formula, i.e., when `LFP(G) = ⋃ₙGⁿ(∅)`. - -Given a complete trace `tr`, let `trₙ` be the `n`th element of the trace, if -it exists. - -Let us now argue that, for any natural `n`, `Gⁿ⁺¹(∅)` denotes the set of -configurations for which, in at most `n` steps, on all paths, `φ` holds, i.e., -``` -Gⁿ⁺¹(∅) = { a | forall tr trace starting in a, exists k ≤ n such that trₖ ∈ ⟦ϕ⟧ } -``` -We do that by induction on `n`: -- Base case: - ``` - G(∅) = ⟦φ⟧ ∪ ( ∁(Prev(∁(∅))) ∩ Prev(Top) ) - = ⟦φ⟧ ∪ ( ∁(Prev(Top)) ∩ Prev(Top) ) - = ⟦φ⟧ ∪ ∅ - = ⟦φ⟧ - = {a | a ∈ ⟦ϕ⟧} - = { a | forall tr trace starting in a, exists k ≤ 0 such that trₖ ∈ ⟦ϕ⟧} - ``` -- Induction case. - `a ∈ Gⁿ⁺²(∅) = G(Gⁿ⁺¹(∅))` iff `φ` holds for `a` or `¬ stuck a` and forall b - such that `a τ b`, `b ∈ Gⁿ⁺¹(∅)`. - Let `tr` be a complete trace starting in `a`. If the trace is just `a`, - then it must be that `a` is stuck, therefore `\phi` holds for `a` and since - `0 ≤ n+1` we are done. Otherwise assume `tr = a ⋅ tr'` such that `tr'` is a - complete trace starting in a configuration `b`. Then `a τ b`, hence `b ∈ Gⁿ⁺¹(∅)`. - By the induction hypothesis, there exists `k ≤ n` such that `tr'ₖ ∈ ⟦ϕ⟧`, hence - `trₖ₊₁ ∈ ⟦ϕ⟧`. - Conversely, let `a` be such that forall `tr` trace starting in a, there exists - `k ≤ 0` such that `trₖ ∈ ⟦ϕ⟧`. If `a ∈ ⟦ϕ⟧`, then `a ∈ G(Gⁿ⁺¹(∅))`. Suppose - `a ∉ ⟦ϕ⟧`. Then `¬ stuck a` (otherwise `a` would be a trace starting in `a` - for which the hypothesis would not hold). Let `b` be such `a τ b`. - -Since `G` is monotone, we can deduce that `Gⁿ(∅) ⊆ Gⁿ⁺¹(∅)` -(obviously `∅ ⊆ G(∅)` and then by applying monotone G `n` times). -Therefore, the limit `⋁ₙGⁿ(∅)` exists. - -By the characterization of `Gⁿ(∅)` presented above, it follows that `⋁ₙGⁿ(∅)` -denotes the set of configurations for which there exists `n` such that in at -most `n` steps, on all paths, `φ` holds, i.e., -``` -⋁ₙGⁿ(∅) = { a | ∃ n, a ∈ Gⁿ⁺¹(∅)} - = { a | ∃n ∀tr tr₀ = a → ∃k k ≤ n ∧ trₖ ∈ ⟦ϕ⟧ } -``` -Note that there is a slight difference from the semantics intended for `AF ϕ`: -`⟦AF ϕ⟧ = { a | ∀tr tr₀ = a → ∃k trₖ ∈ ⟦ϕ⟧` - -Nevertheless, it is relatively easy to see that `⋁ₙGⁿ(∅)` is a subset of `⟦AF ϕ⟧`, -hence, if we show that it is a fixpoint, then they would be equal. -Also, it's easy to see that `⋁ₙGⁿ(∅)` is a post-fixpoint. -We have that for all `n`, `Gⁿ(∅) ⊆ ⋁ₙGⁿ(∅)` and since `G` is monotone, -`Gⁿ⁺¹(∅) ⊆ G(⋁ₙGⁿ(∅))`. Also, obviously `G⁰(∅) = ∅ ⊆ G(⋁ₙGⁿ(∅))`. -Therefore, `⋁ₙGⁿ(∅) ⊆ G(⋁ₙGⁿ(∅))`. - -It remains to show that `⋁ₙGⁿ(∅)` is a pre-fixpoint, i.e., that -`G(⋁ₙGⁿ(∅)) ⊆ ⋁ₙGⁿ(∅)`, or `G(⋁ₙGⁿ(∅)) ∖ ⋁ₙGⁿ(∅) = ∅`. -We have that: -``` -x ∈ G(⋁ₙGⁿ(∅)) ∖ ⋁ₙGⁿ(∅) -⟺ x ∈ G(⋁ₙGⁿ(∅)) and x ∉ ⋁ₙGⁿ(∅) -⟺ (x ∈ ⟦φ⟧ or ¬ stuck x and ∀y x τ y → y ∈ ⋁ₙGⁿ(∅)) and x ∉ ⋁ₙGⁿ(∅) -⟺ ¬ stuck x and (∀y x τ y → y ∈ ⋁ₙGⁿ(∅)) and x ∉ ⋁ₙGⁿ(∅) (since ⟦φ⟧ ⊆ ⋁ₙGⁿ(∅)) -``` - -Given the above relation, we deduce that a sufficient condition ensuring that -`G(⋁ₙGⁿ(∅)) ∖ ⋁ₙGⁿ(∅) = ∅` is that the transition system is finitely branching, -i.e., that `Prev⁻¹({x})` is finite for any `x`. Indeed, suppose -there exists `x ∈ G(⋁ₙGⁿ(∅)) ∖ ⋁ₙGⁿ(∅)`. Then, it must hold that -`¬ stuck x` and `(∀y x τ y → y ∈ ⋁ₙGⁿ(∅))` and `x ∉ ⋁ₙGⁿ(∅)` -Let `k`, `y₁`, ..., `yₖ` be such that `Prev⁻¹({x}) = {y₁, ..., yₖ}`. -For any `i`, `yᵢ ∈ Prev⁻¹({x})`, hence `x τ yᵢ`, therefore `∃nᵢ yᵢ ∈ Gⁿⁱ(∅)`. -Let `n₁`, ..., `nₖ` be such that `yᵢ ∈ Gⁿⁱ(∅)` for any `1≤i≤k`. -Let `m = 𝐦𝐚𝐱 {n₁, ... , nₖ}`. Since `(Gⁿ(∅))ₙ` is an ascending chain, -it follows that `yᵢ ∈ Gᵐ(∅)` for any `1≤i≤k`, -whence `x ∈ Gᵐ⁺¹(∅)`, contradiction with the fact that `x ∉ ⋁ₙGⁿ(∅)`. - -Nevertheless, before continuing, let -us give an example of a system and property for which the above construction is -not a fixpoint. - -### Counterexample for `⟦AF ϕ⟧ = ⋁ₙGⁿ(∅)` - -Consider the following K theory - -``` -syntax KItem ::= "x" - -rule Y:Int => Y -Int 1 requires Y>0 -rule x => ?Y:Int ensures Y >= 0 -``` +Hence, `⟦AF φ⟧ = ⟦μX.φ ∨ (○X ∧ •⊤)⟧`. -and the claim `x → AF 0` +Justified by the above, in the sequel we will use `AF φ` to denote `μX.φ ∨ (○X ∧ •⊤)`. -It is easy to see that any trace originating in `x` will reach `0` in a finite -number of steps. However, there is no bound on the number of steps needed for `x` -to reach `0`. +A consequence of the above is that, by the deduction rules associated with `μ`, +`AF φ` can always be "unrolled" to `φ ∨ (○ AF φ ∧ •⊤)`. ### Total correctness all-path reachability claims @@ -595,3 +501,109 @@ the goal `∀x∪zᵢ.(∃xᵢ.ψᵢ ∧ ⌈φᵢʳᵉᵐ∧φᵢ⌉) → AF∃z `∀x.⊥ → AF∃z.ψ` which can be discharged immediately. Also, in the remainder `¬∃x₁.⌈φ∧φ₁⌉ = ⊤` so the conjunct can be removed. + +## Appendix: Always finally as a Kleene fixed-point + +Note that this appendix bears no relevance for the rest of the document; it is +kept here only for being related to an initial approach to this document. + +Let us study when ⟦AF φ⟧ can be expressed according to Kleene's +least-fixed-point formula, i.e., when `LFP(G) = ⋃ₙGⁿ(∅)`. + +Given a complete trace `tr`, let `trₙ` be the `n`th element of the trace, if +it exists. + +Let us now argue that, for any natural `n`, `Gⁿ⁺¹(∅)` denotes the set of +configurations for which, in at most `n` steps, on all paths, `φ` holds, i.e., +``` +Gⁿ⁺¹(∅) = { a | forall tr trace starting in a, exists k ≤ n such that trₖ ∈ ⟦φ⟧ } +``` +We do that by induction on `n`: +- Base case: + ``` + G(∅) = ⟦φ⟧ ∪ ( ∁(Prev(∁(∅))) ∩ Prev(Top) ) + = ⟦φ⟧ ∪ ( ∁(Prev(Top)) ∩ Prev(Top) ) + = ⟦φ⟧ ∪ ∅ + = ⟦φ⟧ + = {a | a ∈ ⟦φ⟧} + = { a | forall tr trace starting in a, exists k ≤ 0 such that trₖ ∈ ⟦φ⟧} + ``` +- Induction case. + `a ∈ Gⁿ⁺²(∅) = G(Gⁿ⁺¹(∅))` iff `φ` holds for `a` or `¬ stuck a` and forall b + such that `a τ b`, `b ∈ Gⁿ⁺¹(∅)`. + Let `tr` be a complete trace starting in `a`. If the trace is just `a`, + then it must be that `a` is stuck, therefore `\phi` holds for `a` and since + `0 ≤ n+1` we are done. Otherwise assume `tr = a ⋅ tr'` such that `tr'` is a + complete trace starting in a configuration `b`. Then `a τ b`, hence `b ∈ Gⁿ⁺¹(∅)`. + By the induction hypothesis, there exists `k ≤ n` such that `tr'ₖ ∈ ⟦φ⟧`, hence + `trₖ₊₁ ∈ ⟦φ⟧`. + Conversely, let `a` be such that forall `tr` trace starting in a, there exists + `k ≤ 0` such that `trₖ ∈ ⟦φ⟧`. If `a ∈ ⟦φ⟧`, then `a ∈ G(Gⁿ⁺¹(∅))`. Suppose + `a ∉ ⟦φ⟧`. Then `¬ stuck a` (otherwise `a` would be a trace starting in `a` + for which the hypothesis would not hold). Let `b` be such `a τ b`. + +Since `G` is monotone, we can deduce that `Gⁿ(∅) ⊆ Gⁿ⁺¹(∅)` +(obviously `∅ ⊆ G(∅)` and then by applying monotone G `n` times). +Therefore, the limit `⋁ₙGⁿ(∅)` exists. + +By the characterization of `Gⁿ(∅)` presented above, it follows that `⋁ₙGⁿ(∅)` +denotes the set of configurations for which there exists `n` such that in at +most `n` steps, on all paths, `φ` holds, i.e., +``` +⋁ₙGⁿ(∅) = { a | ∃ n, a ∈ Gⁿ⁺¹(∅)} + = { a | ∃n ∀tr tr₀ = a → ∃k k ≤ n ∧ trₖ ∈ ⟦φ⟧ } +``` +Note that there is a slight difference from the semantics intended for `AF φ`: +`⟦AF φ⟧ = { a | ∀tr tr₀ = a → ∃k trₖ ∈ ⟦φ⟧` + +Nevertheless, it is relatively easy to see that `⋁ₙGⁿ(∅)` is a subset of `⟦AF φ⟧`, +hence, if we show that it is a fixed-point, then they would be equal. +Also, it's easy to see that `⋁ₙGⁿ(∅)` is a post-fixed-point. +We have that for all `n`, `Gⁿ(∅) ⊆ ⋁ₙGⁿ(∅)` and since `G` is monotone, +`Gⁿ⁺¹(∅) ⊆ G(⋁ₙGⁿ(∅))`. Also, obviously `G⁰(∅) = ∅ ⊆ G(⋁ₙGⁿ(∅))`. +Therefore, `⋁ₙGⁿ(∅) ⊆ G(⋁ₙGⁿ(∅))`. + +It remains to show that `⋁ₙGⁿ(∅)` is a pre-fixed-point, i.e., that +`G(⋁ₙGⁿ(∅)) ⊆ ⋁ₙGⁿ(∅)`, or `G(⋁ₙGⁿ(∅)) ∖ ⋁ₙGⁿ(∅) = ∅`. +We have that: +``` +x ∈ G(⋁ₙGⁿ(∅)) ∖ ⋁ₙGⁿ(∅) +⟺ x ∈ G(⋁ₙGⁿ(∅)) and x ∉ ⋁ₙGⁿ(∅) +⟺ (x ∈ ⟦φ⟧ or ¬ stuck x and ∀y x τ y → y ∈ ⋁ₙGⁿ(∅)) and x ∉ ⋁ₙGⁿ(∅) +⟺ ¬ stuck x and (∀y x τ y → y ∈ ⋁ₙGⁿ(∅)) and x ∉ ⋁ₙGⁿ(∅) (since ⟦φ⟧ ⊆ ⋁ₙGⁿ(∅)) +``` + +Given the above relation, we deduce that a sufficient condition ensuring that +`G(⋁ₙGⁿ(∅)) ∖ ⋁ₙGⁿ(∅) = ∅` is that the transition system is finitely branching, +i.e., that `Prev⁻¹({x})` is finite for any `x`. Indeed, suppose +there exists `x ∈ G(⋁ₙGⁿ(∅)) ∖ ⋁ₙGⁿ(∅)`. Then, it must hold that +`¬ stuck x` and `(∀y x τ y → y ∈ ⋁ₙGⁿ(∅))` and `x ∉ ⋁ₙGⁿ(∅)` +Let `k`, `y₁`, ..., `yₖ` be such that `Prev⁻¹({x}) = {y₁, ..., yₖ}`. +For any `i`, `yᵢ ∈ Prev⁻¹({x})`, hence `x τ yᵢ`, therefore `∃nᵢ yᵢ ∈ Gⁿⁱ(∅)`. +Let `n₁`, ..., `nₖ` be such that `yᵢ ∈ Gⁿⁱ(∅)` for any `1≤i≤k`. +Let `m = 𝐦𝐚𝐱 {n₁, ... , nₖ}`. Since `(Gⁿ(∅))ₙ` is an ascending chain, +it follows that `yᵢ ∈ Gᵐ(∅)` for any `1≤i≤k`, +whence `x ∈ Gᵐ⁺¹(∅)`, contradiction with the fact that `x ∉ ⋁ₙGⁿ(∅)`. + +Nevertheless, before continuing, let +us give an example of a system and property for which the above construction is +not a fixed-point. + +#### Counterexample for `⟦AF φ⟧ = ⋁ₙGⁿ(∅)` + +Consider the following K theory + +``` +syntax KItem ::= "x" + +rule Y:Int => Y -Int 1 requires Y>0 +rule x => Y:Int ensures Y >= 0 +``` +(note that Y is free on the right-hand-side in the second rule, meaning that X +can transition into any positive integer). + +and the claim `x → AF 0` + +It is easy to see that any trace originating in `x` will reach `0` in a finite +number of steps. However, there is no bound on the number of steps needed for `x` +to reach `0`. From 711ea10a0d5de5617cbb987e87a35c0f98d4a063 Mon Sep 17 00:00:00 2001 From: Traian Florin Serbanuta Date: Tue, 13 Dec 2022 16:50:43 +0200 Subject: [PATCH 7/9] Reorganizing; using a well-founded relation instead of Cfg` be defined as the interpretation of `∙`, that is, +`Prev(S) := ⟦∙ X⟧ₓ₌ₛ` + +We define the relation `τ` on `Cfg` by `a τ b := a ∈ Prev({b})`. +We define the unary predicates `reducible` and `stuck` on `Cfg` by +`reducible a := exists b, a τ b` and `stuck a := ¬ reducible a`. +Note that `stuck a ⟺ Prev⁻¹({a}) = ∅`. + +We can define the set of complete, possibly infinite, traces of the transition +system determined by `Prev⁻¹` starting in an element `a`, called `Traces(a)`, +coinductively, by: +- `a ∈ Traces(a)`, if `stuck a` + (the singleton trace containing just `a`); +- `a ⋅ tr ∈ Traces(a)` for any `b` such that `a τ b` and any `tr ∈ Traces(b)` + (the trace starting with `a` and continuing with trace `tr`). Given a formula `φ`, let `AFφ` denote the formula “all-path finally” `φ`, whose intended semantics is: "the set of configurations for which on all paths, in a finite number of steps, `φ` holds". -In this section we will show that `AFφ` can be captured by the interpretation of -the fixed-point `μX.φ ∨ (○X ∧ •⊤)` +Given a trace `tr` and a natural number `n`, let `trₙ` be the `n`'th element on +trace `tr`, a partial function inductively defined by +``` +a₀ = a +a⋅tr₀ = a +a⋅trₙ₊₁ = trₙ +aₙ₊₁ = ⊥ +``` +Note that for any `tr ∈ Traces(a)`, `tr₀ = a`. -Let `Top` be the set of all configurations, and let `Prev` be the point-wise -extension of the function mapping a configuration to the set of all -configurations which can reach the given configuration in one step. -and `∁` be the complement operator on sets. +Given this definition, the trace semantics for `AF φ` is +``` +⟦AF φ⟧ ::= { a | forall tr ∈ Traces(a), exists n, such that trₙ ∈ ⟦φ⟧ } +``` + +Note that in the definitions above we have abused the notation for `⟦AF φ⟧`, +as `AF φ` is not (yet) a ML formula. + +### All-path finally as a ML formula + +In this section we will show that `AFφ` can actually be captured by ML formula, +namely the fixed-point `μX.φ ∨ (○X ∧ •⊤)`, where `○` is defined as the dual +of `∙`, i.e., `○φ := ¬∙¬φ` The semantics of `μX.φ ∨ (○X ∧ •⊤)` is `LFP(G)` where ``` -G(X) := ⟦φ⟧ ∪ ( ∁(Prev(∁(X))) ∩ Prev(Top) ) +G(X) := ⟦φ⟧ ∪ ( ∁(Prev(∁(X))) ∩ Prev(Cfg) ) ``` Note that, since `X` is positively occurring in the scope of `μ`, `G` is -monotone, so the `LFP(G)` exists and can be defined according to the +monotone, so the `LFP(G)` exists and can be defined according to the Knaster-Tarski formula, as the intersection of all pre-fixed-points of `G`, that is, all `A` such that `G(A) ⊆ A`. @@ -46,48 +90,37 @@ x ∈ G(A) ⟺ × ∈ ⟦φ⟧ ∪ ( ∁(Prev(∁(A))) ∩ Prev(Top) ⟺ × ∈ ⟦φ⟧ or (∅ ⊂ Prev⁻¹({x}) ⊆ A) ``` -Let `stuck x` be defined as `Prev⁻¹(x) = ∅` and let `x τ y` be defined -as `y ∈ Prev⁻¹({x})`. We can also express `∅ ⊂ Prev⁻¹({x}) ⊆ A` in terms -of `stuck` and transitions, as `¬ stuck x ∧ ∀y x τ y → y ∈ A`. +of `reducible` and `τ`, as `reducible x ∧ ∀y x τ y → y ∈ A`. Hence, `x ∈ G(A)` if either `x` matches `φ`, or `x` is not stuck and all its transitions go into `A`. -We can coinductively define (the possibly infinite) complete traces of the -transition system determined by `Prev⁻¹` starting in an element `a` as being: -either just `a`, if `stuck a`, or `a` followed by a trace starting in `b` for -some `b` such that `a τ b`. -Given this definition, the trace semantics for `AF φ` is -``` -⟦AF φ⟧ ::= { a | forall tr trace starting in a, exists b in tr such that b ∈ ⟦φ⟧ } -``` - Let us first argue that `⟦AF φ⟧` is a pre-fixed-point of `G`, i.e., that `G(⟦AF φ⟧) ⊆ ⟦AF φ⟧`. -Take `a ∈ G(⟦AF φ⟧)`. Then either `a ∈ ⟦φ⟧` or `¬ stuck a` and for all `b` +Take `a ∈ G(⟦AF φ⟧)`. Then either `a ∈ ⟦φ⟧` or `reducible a` and for all `b` such that `a τ b`, `b ∈ ⟦AF φ⟧`. -Let `tr` be a complete trace starting in `a`. -If `a ∈ ⟦φ⟧`, then we can choose precisely `a` as the witness on that trace -for which `φ` holds. -Otherwise, `¬ stuck a` and for all `b` such that `a τ b`, `b ∈ ⟦AF φ⟧`. -Since `¬ stuck a` it must be that `tr` cannot be just `a` (it's complete), so -there must exist a `b` such that `a τ b` and `b` is the start of a trace `tr'` -such that `tr = a ⋅ tr'`. However, since `a τ b`, it follows that`b ∈ ⟦AF φ⟧`, -so `tr'` must contain a witness for which `φ` holds; that witness is also a -witness for `tr`. +If `a ∈ ⟦φ⟧`, then for any trace `tr ∈ Traces(a)`, `tr₀ ∈ ⟦φ⟧`, hence `a ∈ ⟦AF φ⟧`. +Otherwise, `reducible a` and for all `b` such that `a τ b`, `b ∈ ⟦AF φ⟧`. +Take `tr ∈ Traces(a)`. Since `reducible a` it must be that `tr` cannot be just `a` +(by definition), so there must exist a `b` such that `a τ b` and `tr' ∈ Traces(b)` +such that `tr = a ⋅ tr'`. +However, since `a τ b`, it follows that `b ∈ ⟦AF φ⟧`, so there exists `n` such that +`tr'ₙ ∈ ⟦φ⟧`, hence `trₙ₊₁ ∈ ⟦φ⟧`. +Since `tr` was arbitrarily chosen, it follows that `a ∈ ⟦AF φ⟧`. Let us now argue that `⟦AF φ⟧` is a post-fixed-point of `G`, i.e., that `⟦AF φ⟧ ⊆ G(⟦AF φ⟧)`. -Take `a ∈ ⟦AF φ⟧`. We need to prove that either `a ∈ ⟦φ⟧` or `¬ stuck a` and +Take `a ∈ ⟦AF φ⟧`. We need to prove that either `a ∈ ⟦φ⟧` or `reducible a` and for all `b` such that `a τ b`, `b ∈ ⟦AF φ⟧`, -If `φ` holds for `a` then we're done. Assume `a ∉ ⟦φ⟧`. -Then it must be that `¬ stuck a`, since otherwise `a` would be a complete trace -starting in `a` with no witness for which `φ` holds. -Let now `b` be such `a τ b`. We need to show that `b ∈ ⟦AF φ⟧`. Let `tr` be a -complete trace starting in `b`. Then `a ⋅ tr` is a complete trace starting in `a`. -Since `a ∈ ⟦AF φ⟧`, there must be a witness in `a ⋅ tr` for which `φ` holds. -However, since `φ` doesn't hold for `a`, the witness must be part of `tr` -Since `tr` was chosen arbitrarily, it must be that `a ∈ ⟦AF φ⟧`. +If `a ∈ ⟦φ⟧` then we're done. Assume next that `a ∉ ⟦φ⟧`. +Then it must be that `reducible a`, since otherwise `a ∈ Traces(a)` and there +exists no `n` such that `aₙ ∈ ⟦φ⟧`. +Let now `b` be such `a τ b`. We need to show that `b ∈ ⟦AF φ⟧`. +Take `tr ∈ Traces(b)`. Then `a ⋅ tr ∈ Traces(a)`. +Since `a ∈ ⟦AF φ⟧`, there exists n such that `(a ⋅ tr)ₙ ∈ ⟦φ⟧`. +However, since `tr₀ = a ∉ ⟦φ⟧`, it means there exists `m` such that +`n = m + 1`, hence, `trₘ = (a ⋅ tr)ₙ ∈ ⟦φ⟧`. +Since `tr` was chosen arbitrarily, it follows that `a ∈ ⟦AF φ⟧`. Therefore, `⟦AF φ⟧` is a fixed-point for `G`. To show that it is the LFP of `G` it suffices to prove that it is included in any pre-fixed-point of `G`. @@ -96,13 +129,15 @@ Let `A` be a pre-fixed-point of `G`, i.e., `G(A) ⊆ A`. That means that (2) `A` contains all configurations which are not stuck and transition on all paths into `A` Assume by contradiction that there exists `a ∈ ⟦AF φ⟧` such that `a ∉ A`. -We will coinductively construct a complete trace starting in `a` with no -witness in `A`. Since `A` contains all configurations for which `φ` holds, -this would contradict the fact that `a ∈ ⟦AF φ⟧`. +We will coinductively construct a complete trace `tr ∈ Traces(a)` such that +for any natural number `n` for which `trₙ` is defined, `trₙ ∉ A`. +Since `A` contains all configurations for which `φ` holds, +this would contradict the fact that `a ∈ ⟦AF φ⟧`. - if `stuck a` is stuck, then take the complete trace `a` -- if `¬ stuck a`, since `a ∉ A`, it means that (2) is false; hence it exists - a transition `a τ b` such that `b ∉ A`. Then take the complete trace - `a ⋅ tr` where `tr` is obtained by applying the above process for `b ∉ A`. +- if `reducible a`, since `a ∉ A`, it means there exists + a transition `a τ b` such that `b ∉ A` (otherwise it would contradict (2)). + Then take the complete trace `a ⋅ tr` where `tr` is obtained by applying the + above process for `b ∉ A`. Hence, `⟦AF φ⟧ = ⟦μX.φ ∨ (○X ∧ •⊤)⟧`. @@ -111,75 +146,35 @@ Justified by the above, in the sequel we will use `AF φ` to denote `μX.φ ∨ A consequence of the above is that, by the deduction rules associated with `μ`, `AF φ` can always be "unrolled" to `φ ∨ (○ AF φ ∧ •⊤)`. -### Total correctness all-path reachability claims +### All-path finally reachability claims Given the definition of all-path finally discussed in the section above, -a total correctness all-path reachability claim is of the form +an all-path finally reachability claim is of the form ``` -∀x.φ(x) → AF ∃z.ψ(x,z) +φ(x) → AF ∃z.ψ(x,z) ``` and basically states that from any configuration `γ` satisfying `φ(x)` for some `x`, a configuration satisfying `ψ(x,z)` for some `z` will be reached in a finite number of steps on any path. -If the system is finitely branching, the claim becomes stronger: -for any configuration `γ` satisfying `φ(x)` for some `x`, there exists a bound -on the number of steps required to reach a configuration satisfying `ψ(x,z)` -for some `z` on any path. -Since the configuration is reached after a finite number of steps, -such reachability claims guarantee termination, thus total correctness. +Since the desired configuration is reached after a finite number of steps, +such reachability claims guarantee total correctness. Problem Description ------------------- -Given a set of reachability claims, of the form `∀x.φ(x) → AF ∃z.ψ(x,z)`, +Given a set of reachability claims, of the form `φᵢ(xᵢ) → AF ∃z.ψᵢ(xᵢ,z)`, we are trying to prove all of them together, by well-founded induction on a -given `measure` defined on the quantified variables `x`. +relation `≺` given `measure(x)` defined on some variables `x` such that `x ⊆ xᵢ`. The well-founded induction argument, which requires the `measure` to decrease before applying a claim as an induction hypothesis, will replace the coinductive argument, which requires that progress is made before applying a circularity. -## Proposal of syntax changes - -- claims need to mention the other claims (including themselves) which are - needed to complete their proof; this induces a dependency relation -- claims which are part of a dependency cycle (including self-dependencies) - would need to be specified together as a "claim group" -- a claim group would need to provide a metric on their input variables; - this metric must decrease whenever one tries to apply a claim from the group - while proving a claim from the same group - -A claim group would be something like -``` -claim group - decreasing measure(x) - - . . . - - claim φᵢ(x) → AF ∃zᵢ.ψᵢ(x,zᵢ) [using(claimᵢ₁, ..., claimᵢₖ)] - - . . . - -end claim group -``` -where the claims referred to by the `using` attribute mention dependencies which -are not part of the cycle. - -TODO(virgil): wouldn't it work to use the existing module syntax? -if so, `import` statements could replace `using` attributed. -Still, syntax for `decreasing` statements, and accounting for sharing the -variables would need to be implemented. - ## Approach -For the algorithms derived from the present approach, please check the next section. - -Assume we want to prove a group of claims defined over the same set of variables -`x`. Further assume that all other claims (which are not in the current group) - on which these claims depend have already been proven. - Assume also a given integer pattern `measure(x)`, over the same variables as - the claims in the group. +Without reducing generality, we can assume that the patterns `φᵢ` (for all `i`) +and `measure` share the same set of variables `x`. Since we're proving all claims together, we can gather them in a single goal, `P(x) ::= (φ₁(x) → AF ∃z.ψ₁(x,z)) ∧ ... ∧ (φₙ(x) → AF ∃z.ψₙ(x,z))`. @@ -188,22 +183,22 @@ A well-founded induction principle allowing to prove `P` using `measure` would be of the form ``` - forall x0, (forall x, 0 <= measure(x) < measure(x0) -> P(x)) -> P(x0) + forall x0, (forall x, measure(x) ≺ measure(x0) -> P(x)) -> P(x0) --------------------------------------------------------------------- forall x, P(x) ``` By the above induction principle, to prove `forall x, P(x)` it suffices to prove -`forall x0, (forall x, 0 <= measure(x) < measure(x0) -> P(x)) -> P(x0)` +`forall x0, (forall x, measure(x) ≺ measure(x0) -> P(x)) -> P(x0)` -Fixing an arbitrary instance `x₀` of the variables and assuming the induction -hypothesis `forall x, 0 <= measure(x) < measure(x0) -> P(x)`, we need to prove +Hence, fixing an arbitrary instance `x₀` of the variables and assuming the induction +hypothesis `forall x, measure(x) ≺ measure(x0) -> P(x)`, we need to prove `P(x₀)`. By first-order manipulation we can transform the induction hypothesis for `P` into a set of induction hypotheses, one for each claim: ``` -∀x. φᵢ(x) ∧ 0 ≤ measure(x) < measure(x₀) → AF ∃z.ψᵢ(x,z) +∀x. φᵢ(x) ∧ measure(x) ≺ measure(x₀) → AF ∃z.ψᵢ(x,z) ``` Similarly we can split the goal into a separate goal `φᵢ(x₀) → AF ∃z.ψᵢ(x₀,z)` @@ -216,7 +211,7 @@ change from one step to the next. Moreover, we will consider the induction hypotheses to be derived claims to be applied as circularities, and denote them as `∀x. φᵢ(x) → AF ∃z.ψᵢ(x,z)`, -where `φᵢ(x)` also contains the guard `0 ≤ measure(x) < measure(x₀)`. +where `φᵢ(x)` also contains the guard `measure(x) ≺ measure(x₀)`. ### Background on unification and remainders of unification @@ -255,7 +250,7 @@ Note that `p` can be `⟂` to signify that unification failed. Hence, whenever `φ` is an extended function-like pattern and `ψ(z)` is an extended constructor-like pattern, we have the following equivalent patterns: ``` -φ ≡ φ ∧ ⊤ ≡ φ ∧ (∃z.ψ(z) ∨ ¬∃z.ψ(z)) ≡ (φ ∧ ∃z.ψ(z)) ∨ (φ ∧ ¬∃z.ψ(z)) ≡ +φ ≡ φ ∧ ⊤ ≡ φ ∧ (∃z.ψ(z) ∨ ¬∃z.ψ(z)) ≡ (φ ∧ ∃z.ψ(z)) ∨ (φ ∧ ¬∃z.ψ(z)) ≡ (∃z.φ ∧ ψ(z)) ∨ (φ ∧ ¬∃z.⌈φ ∧ ψ(z)⌉) ≡ (∃z.ψ(z) ∧ ⌈φ ∧ ψ(z)⌉) ∨ (φ ∧ ¬∃z.⌈φ ∧ ψ(z)⌉) ≡ (∃z.ψ(z) ∧ (z = t) ∧ p(z)) ∨ (φ ∧ ¬∃z.(z = t) ∧ p(z)) ≡ @@ -327,11 +322,11 @@ and one for the remainder Note that, in particular, part of the predicate of the remainder will include the negation of the measure check for each induction hypothesis, of the form -`¬measure(tᵢ(x₀)) < measure(x₀)`. +`¬measure(tᵢ(x₀)) ≺ measure(x₀)`. #### Using a claim to advance the corresponding goal -Assume `φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → AF ∃z.ψ(x₀,z)` goal to be proven +Assume `φᵢ(tᵢ(x₀)) ∧ pᵢ(x₀, tᵢ(x₀)) → AF ∃z.ψ(x₀,z)` goal to be proven and let `∀x. φᵢ(x) → AF ∃z.ψᵢ(x,z)` be the corresponding extended claim. By instatiating the claim with `x := tᵢ(x₀)`, we obtain `φᵢ(tᵢ(x₀)) → AF ∃z.ψᵢ(tᵢ(x₀),z)`; then, by framing, we obtain @@ -387,7 +382,7 @@ Since all but the last conjunct are guaranteed to hold (because of the rewrite axioms), `φ` is stuck if the remainder after attempting to apply all axioms (i.e., the lhs of the last conjunct) is not equivalent to `⊥`. -We want to prove that from the STEP rule and +We want to prove that from the STEP rule and ``` (∀z₁.∃x₁.ψ₁(x₁,z₁) ∧ ⌈φ(x₀) ∧ φ₁(x₁)⌉ → AF∃z.ψ(x₀,z)) ∧ … ∧ (∀zₙ.∃xₙ.ψₙ(xₙ,zₙ) ∧ ⌈φ(x₀) ∧ φₙ(xₙ)⌉ → AF∃z.ψ(x₀,z)) ``` @@ -408,7 +403,7 @@ Apply `(STEP)` on `φ(x₀)`, and we obtain that We can replace our goal succesively with: ``` -o ⋁ᵢ ∃xᵢ.⌈φ(x₀) ∧ φᵢ(xᵢ)⌉ ∧ ∃zᵢ.ψᵢ(xᵢ,zᵢ) → ○AF∃z.ψ(x₀, z) // transitivity of → +o ⋁ᵢ ∃xᵢ.⌈φ(x₀) ∧ φᵢ(xᵢ)⌉ ∧ ∃zᵢ.ψᵢ(xᵢ,zᵢ) → ○AF∃z.ψ(x₀, z) // transitivity of → ⋁ᵢ ∃xᵢ.⌈φ(x₀) ∧ φᵢ(xᵢ)⌉ ∧ ∃zᵢ.ψᵢ(xᵢ,zᵢ) → AF∃z.ψ(x₀, z) // framing on ○ ∃xᵢ.⌈φ(x₀) ∧ φᵢ(xᵢ)⌉ ∧ ∃zᵢ.ψᵢ(xᵢ,zᵢ) → AF∃z.ψ(x₀, z) for all i ``` @@ -441,14 +436,13 @@ __Input:__ - set of variables `x` - claim group `(φ₁(x) → AF∃z.ψ₁(x,z)) ∧ ... ∧ (φₙ(x) → AF∃z.ψₙ(x,z))` -- decreasing `measure(x)` +- decreasing `measure(x)` using `R` __Output:__ Proved or Unproved * Fix an instance `x₀` for the variables `x` -* Let `claims ::= { ∀ x . φᵢ(x) ∧ measure(x) =Int 0` * Let `claimsᵢ ::= claims ∪ { claimᵢ₁, ..., claimᵢₖ }` * Let `Goals := { φᵢ(x₀) }` * While `Goals` is not empty: @@ -501,7 +495,36 @@ the goal `∀x∪zᵢ.(∃xᵢ.ψᵢ ∧ ⌈φᵢʳᵉᵐ∧φᵢ⌉) → AF∃z `∀x.⊥ → AF∃z.ψ` which can be discharged immediately. Also, in the remainder `¬∃x₁.⌈φ∧φ₁⌉ = ⊤` so the conjunct can be removed. - +## Proposal of syntax changes to the K Frontend + +- claims need to mention the other claims (including themselves) which are + needed to complete their proof; this induces a dependency relation +- claims which are part of a dependency cycle (including self-dependencies) + would need to be specified together as a "claim group" +- a claim group would need to provide a metric on their input variables; + this metric must decrease whenever one tries to apply a claim from the group + while proving a claim from the same group + +A claim group would be something like +``` +claim group Grp + imports claims from Grp₁, .. Grpₙ + decreasing measure(x) using R + + . . . + + claim φᵢ(xᵢ) → AF ∃zᵢ.ψᵢ(xᵢ,zᵢ) + + . . . + +end claim group +``` +where we require that: +- the claim import dependency graph contains no cycles; +- the variables in `x` are part of the variables `xᵢ` for each claim in the group; +- `measure(x)` is a (provably) functional pattern +- `R` is a (provably) well-founded relation on the sort of `measure(x)` + ## Appendix: Always finally as a Kleene fixed-point Note that this appendix bears no relevance for the rest of the document; it is @@ -511,7 +534,7 @@ Let us study when ⟦AF φ⟧ can be expressed according to Kleene's least-fixed-point formula, i.e., when `LFP(G) = ⋃ₙGⁿ(∅)`. Given a complete trace `tr`, let `trₙ` be the `n`th element of the trace, if -it exists. +it exists. Let us now argue that, for any natural `n`, `Gⁿ⁺¹(∅)` denotes the set of configurations for which, in at most `n` steps, on all paths, `φ` holds, i.e., @@ -575,16 +598,22 @@ x ∈ G(⋁ₙGⁿ(∅)) ∖ ⋁ₙGⁿ(∅) Given the above relation, we deduce that a sufficient condition ensuring that `G(⋁ₙGⁿ(∅)) ∖ ⋁ₙGⁿ(∅) = ∅` is that the transition system is finitely branching, -i.e., that `Prev⁻¹({x})` is finite for any `x`. Indeed, suppose +i.e., that `Prev⁻¹({x})` is finite for any `x`. Indeed, suppose there exists `x ∈ G(⋁ₙGⁿ(∅)) ∖ ⋁ₙGⁿ(∅)`. Then, it must hold that -`¬ stuck x` and `(∀y x τ y → y ∈ ⋁ₙGⁿ(∅))` and `x ∉ ⋁ₙGⁿ(∅)` +`¬ stuck x` and `(∀y x τ y → y ∈ ⋁ₙGⁿ(∅))` and `x ∉ ⋁ₙGⁿ(∅)` Let `k`, `y₁`, ..., `yₖ` be such that `Prev⁻¹({x}) = {y₁, ..., yₖ}`. For any `i`, `yᵢ ∈ Prev⁻¹({x})`, hence `x τ yᵢ`, therefore `∃nᵢ yᵢ ∈ Gⁿⁱ(∅)`. Let `n₁`, ..., `nₖ` be such that `yᵢ ∈ Gⁿⁱ(∅)` for any `1≤i≤k`. Let `m = 𝐦𝐚𝐱 {n₁, ... , nₖ}`. Since `(Gⁿ(∅))ₙ` is an ascending chain, -it follows that `yᵢ ∈ Gᵐ(∅)` for any `1≤i≤k`, +it follows that `yᵢ ∈ Gᵐ(∅)` for any `1≤i≤k`, whence `x ∈ Gᵐ⁺¹(∅)`, contradiction with the fact that `x ∉ ⋁ₙGⁿ(∅)`. +Hence, if the transition system is finitely branching, we have a stronger +interpretation for an always-finally reachability claim `∀x.φ(x) → AF ∃z.ψ(x,z)`: +for any configuration `γ` satisfying `φ(x)` for some `x`, there exists a bound +on the number of steps required to reach a configuration satisfying `ψ(x,z)` +for some `z` on any path. + Nevertheless, before continuing, let us give an example of a system and property for which the above construction is not a fixed-point. @@ -594,16 +623,16 @@ not a fixed-point. Consider the following K theory ``` -syntax KItem ::= "x" +syntax KItem ::= "start" rule Y:Int => Y -Int 1 requires Y>0 -rule x => Y:Int ensures Y >= 0 +rule start => Y:Int ensures Y >= 0 ``` -(note that Y is free on the right-hand-side in the second rule, meaning that X -can transition into any positive integer). +(note that Y is free on the right-hand-side in the second rule, meaning that +`start` can transition into any positive integer). -and the claim `x → AF 0` +and the claim `start → AF 0` -It is easy to see that any trace originating in `x` will reach `0` in a finite -number of steps. However, there is no bound on the number of steps needed for `x` -to reach `0`. +It is easy to see that any trace originating in `start` will reach `0` in a finite +number of steps. However, there is no bound on the number of steps needed for +`start` to reach `0`. From a2948d1170ce18f778dfa0ec8fe355a4585313c8 Mon Sep 17 00:00:00 2001 From: Traian Florin Serbanuta Date: Thu, 15 Dec 2022 16:35:46 +0200 Subject: [PATCH 8/9] Progress --- ...Corectness-All-Path-Reachability-Proofs.md | 62 ++++++++++++++----- 1 file changed, 48 insertions(+), 14 deletions(-) diff --git a/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md b/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md index 60d5d31307..b699782e8b 100644 --- a/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md +++ b/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md @@ -61,6 +61,21 @@ Given this definition, the trace semantics for `AF φ` is Note that in the definitions above we have abused the notation for `⟦AF φ⟧`, as `AF φ` is not (yet) a ML formula. +### Rewriting rules + +Within this setting, rewrite rules can be encoded as axioms of the form +``` +φ(x) → ∙ ψ(x) +``` + +Note that in any model containing such an axiom, for any valuation, +`⟦φ(x)⟧ ⊆ Prev(⟦ψ(x)⟧)`, i.e., for any `a ∈ ⟦φ(x)⟧` there exists `b ∈ ⟦ψ(x)⟧` +such that `a τ b`. +That is, any configurations described by `φ(x)` can transition in one step +to a configuration described by `ψ(x)`. + +We would like to assume that interpretation `Prev` + ### All-path finally as a ML formula In this section we will show that `AFφ` can actually be captured by ML formula, @@ -164,41 +179,45 @@ Problem Description ------------------- Given a set of reachability claims, of the form `φᵢ(xᵢ) → AF ∃z.ψᵢ(xᵢ,z)`, -we are trying to prove all of them together, by well-founded induction on a -relation `≺` given `measure(x)` defined on some variables `x` such that `x ⊆ xᵢ`. +we are trying to prove all of them together, by induction on a well-founded +relation `≺` on tupples of sorts corresponding to a set of variables `x` +such that `x ⊆ xᵢ` (in a fixed order). For example, such a relation can be +provided by means of a `measure` function having as domain the above mentioned +tupples and as codomain a sort equipped with a well-founded ordering. -The well-founded induction argument, which requires the `measure` to decrease before -applying a claim as an induction hypothesis, will replace the coinductive argument, -which requires that progress is made before applying a circularity. +The well-founded induction argument, which requires the instance of variables +to decrease before applying a claim as an induction hypothesis, will replace +the coinductive argument, which requires that progress is made before applying +a circularity. ## Approach -Without reducing generality, we can assume that the patterns `φᵢ` (for all `i`) -and `measure` share the same set of variables `x`. +Without loss of generality, we can assume that the patterns `φᵢ` (for all `i`) +share the same set of variables `x`. Since we're proving all claims together, we can gather them in a single goal, `P(x) ::= (φ₁(x) → AF ∃z.ψ₁(x,z)) ∧ ... ∧ (φₙ(x) → AF ∃z.ψₙ(x,z))`. -A well-founded induction principle allowing to prove `P` using `measure` would +A well-founded induction principle allowing to prove `P` using `≺` would be of the form ``` - forall x0, (forall x, measure(x) ≺ measure(x0) -> P(x)) -> P(x0) - --------------------------------------------------------------------- - forall x, P(x) + forall x0, (forall x, x ≺ x0 -> P(x)) -> P(x0) + ---------------------------------------------- + forall x, P(x) ``` By the above induction principle, to prove `forall x, P(x)` it suffices to prove -`forall x0, (forall x, measure(x) ≺ measure(x0) -> P(x)) -> P(x0)` +`forall x0, (forall x, x ≺ x0 -> P(x)) -> P(x0)` Hence, fixing an arbitrary instance `x₀` of the variables and assuming the induction -hypothesis `forall x, measure(x) ≺ measure(x0) -> P(x)`, we need to prove +hypothesis `forall x, x ≺ x₀ -> P(x)`, we need to prove `P(x₀)`. By first-order manipulation we can transform the induction hypothesis for `P` into a set of induction hypotheses, one for each claim: ``` -∀x. φᵢ(x) ∧ measure(x) ≺ measure(x₀) → AF ∃z.ψᵢ(x,z) +∀x. φᵢ(x) ∧ x ≺ x₀ → AF ∃z.ψᵢ(x,z) ``` Similarly we can split the goal into a separate goal `φᵢ(x₀) → AF ∃z.ψᵢ(x₀,z)` @@ -213,6 +232,21 @@ Moreover, we will consider the induction hypotheses to be derived claims to be applied as circularities, and denote them as `∀x. φᵢ(x) → AF ∃z.ψᵢ(x,z)`, where `φᵢ(x)` also contains the guard `measure(x) ≺ measure(x₀)`. +Given + + +Hence, instead of the circularity rule of Reachability logic we will add +the following rule: + + +``` +for all j, Γₓ₀ ∪ {φₖ(x) ∧ x ≺ x₀ → AF ∃zₖ ψₖ(x,zₖ)}ₖ ⊢ φⱼ(x₀) → AF ∃zⱼ ψⱼ(x₀,zⱼ) +------------------------------------------------------------------------------------------------, + Γ ⊢ φᵢ(x) → AF ∃zᵢ ψᵢ(x,zᵢ) +``` +where, + + ### Background on unification and remainders of unification Similarly to the All-Path Reachability document, we assume all pattern variables From c50215caec97bf59dfb5e008dc96da6df15a0f3c Mon Sep 17 00:00:00 2001 From: Traian Florin Serbanuta Date: Fri, 16 Dec 2022 18:05:35 +0200 Subject: [PATCH 9/9] rules of inference for AF claims --- ...Corectness-All-Path-Reachability-Proofs.md | 317 ++++++++++++------ 1 file changed, 219 insertions(+), 98 deletions(-) diff --git a/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md b/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md index b699782e8b..cc36e3ffdf 100644 --- a/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md +++ b/docs/2022-04-07-Total-Corectness-All-Path-Reachability-Proofs.md @@ -15,12 +15,12 @@ For any pattern `φ`, set variable `X`, and subset `S` of the model (of the righ let `⟦φ⟧ₓ₌ₛ` denote the interpretation of `φ` in the model using the fixed interpretation with the exception that set variable `X` is interpreted as `S`. -### Reducibility, Transitions, Traces +### Accessibility in one step. Transitions Assume that an ML signature contains a _next_ operator `•` (on the sort of configurations). -The intuition for `∙ φ` is that it comprises all configurations which can -transition to `φ` in a single step. +The intuition for `∙ φ` is that it comprises all configurations which can, +in one step, transition to a configuration satisfying `φ`. Let `Cfg` be the interpretation of the configurations sort in the model. Let `Prev : Cfg -> Cfg` be defined as the interpretation of `∙`, that is, @@ -31,6 +31,22 @@ We define the unary predicates `reducible` and `stuck` on `Cfg` by `reducible a := exists b, a τ b` and `stuck a := ¬ reducible a`. Note that `stuck a ⟺ Prev⁻¹({a}) = ∅`. +The set of `reducible` configurations, `Prev(Cfg)`, can be expressed as the +interpretation of pattern `∙ ⊤`. + +### Rewriting axioms + +Within this setting, rewrite rules can be encoded as axioms of the form +`φ(x) → ∙ ψ(x)`, which constrain the interpretation of `Prev` in models. + +Note that in any model satisfying such an axiom, for any valuation, it must be that +`⟦φ(x)⟧ ⊆ Prev(⟦ψ(x)⟧)`, i.e., for any `a ∈ ⟦φ(x)⟧` there exists `b ∈ ⟦ψ(x)⟧` +such that `a τ b`. +That is, any configuration described by `φ(x)` can transition in one step +to a configuration described by `ψ(x)`. + +### Traces + We can define the set of complete, possibly infinite, traces of the transition system determined by `Prev⁻¹` starting in an element `a`, called `Traces(a)`, coinductively, by: @@ -59,22 +75,212 @@ Given this definition, the trace semantics for `AF φ` is ``` Note that in the definitions above we have abused the notation for `⟦AF φ⟧`, -as `AF φ` is not (yet) a ML formula. +as `AF φ` is not (yet) a ML formula; we will continue to do so in the following +sections, while mentioning that a proper expression of `AF φ` as a ML formula +will be presented later in the document. -### Rewriting rules +### All-path finally reachability claims + +Given the definition of all-path finally discussed in the section above, +an all-path finally reachability claim is of the form `φ → AF ψ` (where `φ` and +`ψ` may contain free variables) and basically states that from any configuration +`γ` satisfying `φ`, a configuration satisfying `ψ` will be reached +in a finite number of steps on any path. + +Since the desired configuration is reached after a finite number of steps, +such reachability claims guarantee total correctness. + +Problem Description +------------------- + +Given an axiomatization of a transition system as a set of rewrite axioms of the +form presented above, we want to devise a set of rules to allow us to prove +reachability claims, with the following observations: +- the proof of a claim can be reduced to proving other claims +- we might need to use a claim to prove itself (loops, recursive functions) +- there might be mutually-dependent claims (mutually-recursive functions) + +To be more specific, we want a set of rules to derive judgements of the form +`Γ ⊢ᴬ φ → AF ψ`; here `Γ` is the rewrite system context, of the form +`Γ := (Σ, Γₛ, Γᵣ, Γₕ)`, where +- `Σ` is the signature containing constructors, functions and predicates used to + decribe and (statically) manipulate configurations and datatypes. +- `Γₛ` are "structural" axioms, used to describe the static semantics of + configurations and datatypes +- `Γᵣ` contains the rewrite axioms +- `Γₕ` contains trusted reachability claims + + +Approach +-------- + +We will first present the rules, then argue about their soundness w.r.t. the +model interpretations. + + +### Proper Rules + +#### Rule of Consequence -Within this setting, rewrite rules can be encoded as axioms of the form ``` -φ(x) → ∙ ψ(x) +Γₛ ⊢ᴹᴸ φ → φ' Γ ⊢ᴬ φ' → AF ψ' Γₛ ⊢ᴹᴸ ψ' → ψ +------------------------------------------------ + Γ ⊢ᴬ φ → AF ψ ``` -Note that in any model containing such an axiom, for any valuation, -`⟦φ(x)⟧ ⊆ Prev(⟦ψ(x)⟧)`, i.e., for any `a ∈ ⟦φ(x)⟧` there exists `b ∈ ⟦ψ(x)⟧` -such that `a τ b`. -That is, any configurations described by `φ(x)` can transition in one step -to a configuration described by `ψ(x)`. +#### Rule of Reflexivity + + +``` + ✓ +-------------- + Γ ⊢ᴬ φ → AF φ +``` + +#### Rule of Transitivity + + +``` + Γ ⊢ᴬ φ → AF χ Γ ⊢ᴬ χ → AF ψ +------------------------------ + Γ ⊢ᴬ φ → AF ψ +``` + +#### Rule of Disjunction + +Disjunction on the hypothesis generates a claim for each disjunct: +``` +Γ ⊢ᴬ φ₁ → AF ψ Γ ⊢ᴬ φ₂ → AF ψ +------------------------------- + Γ ⊢ᴬ φ₁ ∨ φ₂ → AF ψ +``` + +#### Rule of Generalization + +Existential quantification of the hypothesis can be removed +``` + Γ ⊢ᴬ φ(y) → AF ψ +------------------- +Γ ⊢ᴬ ∃y.φ(y) → AF ψ +``` + +#### Rule of Trusted Claim + +``` + ✓ +--------------- where φ → AF ψ ∈ Γₜ + Γ ⊢ᴬ φ → AF ψ +``` + +#### Rule of STEP +Assuming that the transition system only admits transitions which are specified +by the rules in `Γᵣ`, we can state the following one-step rule: +``` + Γₛ ⊢ᴹᴸ φ ∧ ⋀ᵢ¬∃xᵢ.φᵢ(xᵢ) → ⊥ +------------------------------------------ if Γᵣ=⋃ᵢ{φᵢ(xᵢ) → ∙ ψᵢ(xᵢ)} +Γ ⊢ᴬ φ → AF ⋁ᵢ(∃xᵢ. ⌈φ ∧ φᵢ(xᵢ)⌉ ∧ ψᵢ(xᵢ)) +``` + +#### Rule of Induction +Let Γₕ = ⋃ᵢ{φᵢ(x) → AF ψᵢ(x)} be a set of claims indexed by the same variables `x`. +Assume a fixed order among the variables of `x`, and let `≺` be a well-founded +order on tupples of the sorts of the variables in `x` (in the assumed fixed order). +For a given context `Γ`, let `Γ'=(Σ', Γ'ₛ, Γᵣ, Γ'ₜ)` be defined by: +- `Σ' = Σ ∪ Σ≺ ∪ c₀`, where `c₀` is a fresh set of constants corresponding to the + variables in `x`, of the appropriate sorts (and in the same fixed order) and + `Σ≺` may contain additional symbols needed to axiomatize `≺` +- `Γ'ₛ = Γₛ ∪ Γ≺ ∪ Γₓ`, where `Γ≺` contains axioms for defining `≺` and + `Γₓ` contains an axiom of the form `∃z.z = c` for any constant `c` in `c₀` +- `Γ'ₜ = Γₜ ∪ ⋃ᵢ{φᵢ(x) ∧ x ≺ c₀ → AF ψᵢ(x)}` + +Given the above, the rule of induction for (Γₕ, x, ≺) is +``` +for all j, Γ' ⊢ᴬ φⱼ(c₀) → AF ψⱼ(c₀) +---------------------------------------, where Γₕ = ⋃ⱼ{φⱼ(x) → AF ψⱼ(x)} + Γ ⊢ φᵢ(x) → AF ψᵢ(x) +``` + + +### Derived rules + +#### Rule of Eliminating the Conclusion + +We can always filter out the portion of the hypothesis for which the conclusion +already holds +``` +Γ ⊢ᴬ φ(x)∧¬∃z.ψ(x,z) → AF ∃z.ψ(x,z) +----------------------------------- + Γ ⊢ᴬ φ(x) → AF ∃z.ψ(x,z) +``` + + like a set of already proven/ trusted reachability claims, we +want to prove a set of reachability claims, of the form `φᵢ(x) → AF ∃zᵢ.ψᵢ(x,zᵢ)`, +sharing the same set of free variables, we are trying to prove all of them together, +by induction on a well-founded relation `≺` on tupples of sorts corresponding to +the set of variables `x` (in a fixed order). For example, such a relation can be +provided by means of a `measure` function having as domain the above mentioned +tupples and as codomain a sort equipped with a well-founded ordering. + +The well-founded induction argument, which requires the instance of variables +to decrease before applying a claim as an induction hypothesis, will replace +the coinductive argument, which requires that progress is made before applying +a circularity. + +## Approach + +Without loss of generality, we can assume that the patterns `φᵢ` (for all `i`) +share the same set of variables `x`. + +Since we're proving all claims together, we can gather them in a single goal, +`P(x) ::= (φ₁(x) → AF ∃z.ψ₁(x,z)) ∧ ... ∧ (φₙ(x) → AF ∃z.ψₙ(x,z))`. + +A well-founded induction principle allowing to prove `P` using `≺` would +be of the form + +``` + forall x0, (forall x, x ≺ x0 -> P(x)) -> P(x0) + ---------------------------------------------- + forall x, P(x) +``` + +By the above induction principle, to prove `forall x, P(x)` it suffices to prove +`forall x0, (forall x, x ≺ x0 -> P(x)) -> P(x0)` + +Hence, fixing an arbitrary instance `x₀` of the variables and assuming the induction +hypothesis `forall x, x ≺ x₀ -> P(x)`, we need to prove +`P(x₀)`. + +By first-order manipulation we can transform the induction hypothesis for `P` +into a set of induction hypotheses, one for each claim: +``` +∀x. φᵢ(x) ∧ x ≺ x₀ → AF ∃z.ψᵢ(x,z) +``` + +Similarly we can split the goal into a separate goal `φᵢ(x₀) → AF ∃z.ψᵢ(x₀,z)` +for each claim. + +Since we might be using the claims to advance the proof of the claim, to avoid +confusion (and to reduce caring about indices) we will denote a goal with +`φ(x₀) → AF ∃z.ψ(x₀,z)` in all subsequent steps, although the exact goal might +change from one step to the next. + +Moreover, we will consider the induction hypotheses to be derived claims to +be applied as circularities, and denote them as `∀x. φᵢ(x) → AF ∃z.ψᵢ(x,z)`, +where `φᵢ(x)` also contains the guard `measure(x) ≺ measure(x₀)`. -We would like to assume that interpretation `Prev` +Given + + +Hence, instead of the circularity rule of Reachability logic we will add +the following rule: + + +``` +for all j, Γₓ₀ ∪ {φₖ(x) ∧ x ≺ x₀ → AF ∃zₖ ψₖ(x,zₖ)}ₖ ⊢ φⱼ(x₀) → AF ∃zⱼ ψⱼ(x₀,zⱼ) +------------------------------------------------------------------------------------------------, + Γ ⊢ φᵢ(x) → AF ∃zᵢ ψᵢ(x,zᵢ) +``` +where, ### All-path finally as a ML formula @@ -161,91 +367,6 @@ Justified by the above, in the sequel we will use `AF φ` to denote `μX.φ ∨ A consequence of the above is that, by the deduction rules associated with `μ`, `AF φ` can always be "unrolled" to `φ ∨ (○ AF φ ∧ •⊤)`. -### All-path finally reachability claims - -Given the definition of all-path finally discussed in the section above, -an all-path finally reachability claim is of the form -``` -φ(x) → AF ∃z.ψ(x,z) -``` -and basically states that from any configuration `γ` satisfying `φ(x)` -for some `x`, a configuration satisfying `ψ(x,z)` for some `z` will be reached -in a finite number of steps on any path. - -Since the desired configuration is reached after a finite number of steps, -such reachability claims guarantee total correctness. - -Problem Description -------------------- - -Given a set of reachability claims, of the form `φᵢ(xᵢ) → AF ∃z.ψᵢ(xᵢ,z)`, -we are trying to prove all of them together, by induction on a well-founded -relation `≺` on tupples of sorts corresponding to a set of variables `x` -such that `x ⊆ xᵢ` (in a fixed order). For example, such a relation can be -provided by means of a `measure` function having as domain the above mentioned -tupples and as codomain a sort equipped with a well-founded ordering. - -The well-founded induction argument, which requires the instance of variables -to decrease before applying a claim as an induction hypothesis, will replace -the coinductive argument, which requires that progress is made before applying -a circularity. - -## Approach - -Without loss of generality, we can assume that the patterns `φᵢ` (for all `i`) -share the same set of variables `x`. - -Since we're proving all claims together, we can gather them in a single goal, -`P(x) ::= (φ₁(x) → AF ∃z.ψ₁(x,z)) ∧ ... ∧ (φₙ(x) → AF ∃z.ψₙ(x,z))`. - -A well-founded induction principle allowing to prove `P` using `≺` would -be of the form - -``` - forall x0, (forall x, x ≺ x0 -> P(x)) -> P(x0) - ---------------------------------------------- - forall x, P(x) -``` - -By the above induction principle, to prove `forall x, P(x)` it suffices to prove -`forall x0, (forall x, x ≺ x0 -> P(x)) -> P(x0)` - -Hence, fixing an arbitrary instance `x₀` of the variables and assuming the induction -hypothesis `forall x, x ≺ x₀ -> P(x)`, we need to prove -`P(x₀)`. - -By first-order manipulation we can transform the induction hypothesis for `P` -into a set of induction hypotheses, one for each claim: -``` -∀x. φᵢ(x) ∧ x ≺ x₀ → AF ∃z.ψᵢ(x,z) -``` - -Similarly we can split the goal into a separate goal `φᵢ(x₀) → AF ∃z.ψᵢ(x₀,z)` -for each claim. - -Since we might be using the claims to advance the proof of the claim, to avoid -confusion (and to reduce caring about indices) we will denote a goal with -`φ(x₀) → AF ∃z.ψ(x₀,z)` in all subsequent steps, although the exact goal might -change from one step to the next. - -Moreover, we will consider the induction hypotheses to be derived claims to -be applied as circularities, and denote them as `∀x. φᵢ(x) → AF ∃z.ψᵢ(x,z)`, -where `φᵢ(x)` also contains the guard `measure(x) ≺ measure(x₀)`. - -Given - - -Hence, instead of the circularity rule of Reachability logic we will add -the following rule: - - -``` -for all j, Γₓ₀ ∪ {φₖ(x) ∧ x ≺ x₀ → AF ∃zₖ ψₖ(x,zₖ)}ₖ ⊢ φⱼ(x₀) → AF ∃zⱼ ψⱼ(x₀,zⱼ) -------------------------------------------------------------------------------------------------, - Γ ⊢ φᵢ(x) → AF ∃zᵢ ψᵢ(x,zᵢ) -``` -where, - ### Background on unification and remainders of unification