proof #1

tesi/tesi_unicode.org

@@ -765,3 +765,63 @@ following four rules:
    largest prefix matrix for which one of the three previous rules
    apply, and P₂ → L₂ containing the remaining rows. The algorithm is
    applied to both matrices.
+
+* Correctness of the algorithm
+Running a program tₛ or its translation 〚tₛ〛 against an input vₛ
+produces as a result a result /r/ in the following way:
+| ( 〚tₛ〛ₛ(vₛ) = Cₛ(vₛ) ) → r
+| tₛ(vₛ) → r
+Likewise
+| ( 〚tₜ〛ₜ(vₜ) = Cₜ(vₜ) ) → r
+| tₜ(vₜ) → r
+where result r ::= guard list * (Match blackbox | NoMatch | Absurd)
+and guard ::= blackbox.
+
+Having defined equivalence between two inputs of which one is
+expressed in the source language and the other in the target language
+  vₛ ≃ vₜ    (TODO define, this talks about the representation of source values in the target)
+
+we can define the equivalence between a couple of programs or a couple
+ofconstraint trees 
+| tₛ ≃ tₜ := ∀vₛ≃vₜ, tₛ(vₛ) = tₜ(vₜ)
+| Cₛ ≃ Cₜ := ∀vₛ≃vₜ, Cₛ(vₛ) = Cₜ(vₜ)
+
+The proposed equivalence algorithm that works on a couple of
+constraint trees is returns either /Yes/ or /No(vₛ, vₜ)/ where vₛ and
+vₜ are a couple of possible counter examples for which the constraint
+trees produce a different result.
+
+** Statements
+Theorem. We say that a translation of a source program to a constraint tree
+is correct when for every possible input, the source program and its
+respective constraint tree produces the same result
+
+| ∀vₛ, tₛ(vₛ) = 〚tₛ〛ₛ(vₛ)
+
+Likewise, for the target language:
+
+| ∀vₜ, tₜ(vₜ) = 〚tₜ〛ₜ(vₜ)
+
+Definition: in the presence of guards we can say that two results are
+equivalent modulo the guards queue, written /r₁ ≃gs r₂/, when:
+| (gs₁, r₁) ≃gs (gs₂, r₂)  ⇔  (gs₁, r₁) = (gs₂ ++ gs, r₂)
+
+Definition: we say that Cₜ covers the input space /S/, written
+/covers(Cₜ, S) when every value vₛ∈S is a valid input to the
+constraint tree Cₜ. (TODO: rephrase)
+
+Theorem: Given an input space /S/ and a couple of constraint trees, where
+the target constraint tree Cₜ covers the input space /S/, we say that
+the two constraint trees are equivalent when:
+
+| (equiv S Cₛ Cₜ gs = Yes) ∧ covers(Cₜ, S) ⇒ ∀vₛ≃vₜ ∈ S, Cₛ(vₛ) ≃gs Cₜ(vₜ)
+
+Similarly we say that a couple of constraint trees in the presence of
+an input space /S/ are /not/ equivalent when:
+
+| (equiv S Cₛ Cₜ gs = No(vₛ,vₜ) ∧ covers(Cₜ, S) ⇒ vₛ≃vₜ ∈ S ∧ Cₛ(vₛ) ≠gs Cₜ(vₜ)
+
+Corollary: For a full input space /S/, that is the universe of the
+target program we say:
+
+| (equiv S [|tₛ|]ₛ [|tₜ|]ₜ ∅ = Yes)  ⇔  tₛ ≃ tₜ