From 5ebabff90de8dc84ab638016750741b2c65dac42 Mon Sep 17 00:00:00 2001
From: Francesco Mecca <me@francescomecca.eu>
Date: Wed, 1 Apr 2020 00:37:54 +0200
Subject: [PATCH] continuing with proof

---
 tesi/tesi_unicode.org | 110 +++++++++++++++++++++++++++++++++++++-----
 1 file changed, 99 insertions(+), 11 deletions(-)

diff --git a/tesi/tesi_unicode.org b/tesi/tesi_unicode.org
index f75ab47..e8fc597 100644
--- a/tesi/tesi_unicode.org
+++ b/tesi/tesi_unicode.org
@@ -960,16 +960,104 @@ Are K and Here clear here?
 
 We define the decomposition matrix /mₛ/ as
 | SMatrix mₛ := (aⱼ)^{j∈J}, ((pᵢⱼ)^{j∈J} → bbᵢ)^{i∈I}
-Given that the decomposition matrix is computed from source terms, we
-need to prove that it respects:
-| ∀(vⱼ)^{j∈J}, mₛ(vⱼ)ʲ = 〚mₛi 〛(vⱼ)ʲ
+\begin{comment}
+Correggi prendendo in considerazione l'accessor
+\end{comment}
 
-v(Here) = v
-K(vᵢ)ⁱ(k.a) = vₖ(a) if k ∈ [0;n[
+We define the constraint tree of source programs
+  [|tₛ|]
+in terms of the constraint tree of pattern matrices
+  [|mₛ|]
+by the following:
+  〚((pᵢ → bbᵢ)^{i∈I}〛 := 〚(Root), (pᵢ → bbᵢ)^{i∈I} 〛 # i ∈ I
 
-We also said that
-(Leaf bb)(v) := Match bb
-(Node(a, (kᵢ → cᵢ)ⁱ, c_{fallback}))(v)
-    let v(a) be K(vⱼ)ʲ
-        if k ∈ {Kᵢ}ⁱ then  C_{min{i}|k=kᵢ}(v)
-        else c_{fallback}(v)
+Constraint tree computed from pattern matrices respect the following invariant:
+| ∀v (vᵢ)^{i∈I} = v(aᵢ)^{i∈I} → 〚m〛(v) = m(vᵢ)^{i∈I} for m = ((aᵢ)^{i∈I}, (rᵢ)^{i∈I})
+where 
+| v(Here) = v
+| K(vᵢ)ⁱ(k.a) = vₖ(a) if k ∈ [0;n[
+\begin{comment}
+TODO: EXPLAIN
+\end{comment}
+
+We proceed to show the correctness of the invariant by a case
+analysys.
+
+Base cases:
+1. [| ∅, (∅ → bbᵢ)ⁱ |] := Leaf bbᵢ where i := min(I), that is a
+   constraint tree [|ms|] defined by an empty accessor and empty
+   patterns pointing to blackboxes /bbᵢ/. This respects the invariant
+   because a decomposition matrix in the case of empty rows returns
+   the first expression and we known that (Leaf bb)(v) := Match bb
+2. [| (aⱼ)ʲ, ∅ |] := Failure 
+
+Regarding non base cases:
+We define
+| let Idx(k) = [0; arity(k)[
+| let First(∅) = ⊥
+| let First((aⱼ)ʲ) = a_{min(j)} ## where j ∈ J ≠ ∅
+
+
+
+
+** Proof of equivalence checking
+
+The equivalence checking algorithm takes as parameters an input space
+/S/, a source constraint tree /Cₛ/ and a target constraint tree /Cₜ/:
+| equiv(S, Cₛ, Cₜ) → Yes | No(vₛ, vₜ)
+
+When the algorithm returns Yes and the input space is covered by /Cₛ/
+we can say that the couple of constraint trees are the same for
+every couple of source value /vₛ/ and target value /vₜ/ that are equivalent.
+\begin{comment}
+Define "covered"
+Is it correct to say the same? How to correctly distinguish in words ≊ and = ?
+\end{comment}
+| equiv(S, Cₛ, Cₜ) = Yes and cover(Cₜ, S) → ∀ vₛ ≊ vₜ∈S ∧ Cₛ(vₛ) = Cₜ(vₜ)
+In the case where the algorithm returns No we have at least a couple
+of counter example values vₛ and vₜ for which the two constraint trees
+outputs a different result.
+| equiv(S, Cₛ, Cₜ) = No(vₛ,vₜ) and cover(Cₜ, S) → ∀ vₛ ≊ vₜ∈S ∧ Cₛ(vₛ) ≠ Cₜ(vₜ)
+
+We define  the following
+| Forall(Yes) = Yes
+| Forall(Yes::l) = Forall(l)
+| Forall(No(vₛ,vₜ)::_) = No(vₛ,vₜ)
+There exists and are injective:
+|  int(k)∈ℕ (ar(k) = 0) 
+|  tag(k)∈ℕ (ar(k) > 0) 
+|  π(k) = {n|int(k) = n} x {n|tag{k} = n}
+where k is a constructor.
+
+\begin{comment}
+TODO: explain:
+∀v∈a→π, C_{/a→π}(v) = C(v)
+\end{comment}
+
+We proceed by case analysis:
+1. equiv(∅, Cₛ, Cₜ) := Yes
+\begin{comment}
+Devo spiegarlo?
+\end{comment}
+In the other subcases S is always non-empty.
+2. equiv(S, Failure, Failure) := Yes
+   the statement holds because of equality between Failure nodes in
+   the case of every possible value /v/.
+3. The result of the subcase where we have a source constraint tree
+   /Cₛ/ that is either a Leaf terminal or a Failure terminal and a
+   target constraint tree defined by an accessor /a/ and a positive
+   number of couples constraint πᵢ and children nodes Cₜᵢ. The output
+   the output of the algorithm is:
+   | equiv(S, (Leaf bbₛ|Failure) as Cₛ, Node(a, (πᵢ → Cₜᵢ)ⁱ)) :=  Forall(equiv( S∩a→π(kᵢ)), Cₛ, Cₜᵢ)ⁱ)
+   The statement holds because defined let Sᵢ := S∩(a→πᵢ)
+   either the algorithm is true for every sub-input space Sᵢ and
+   subtree Cₜᵢ
+   | equiv(Sᵢ, Cₛ, Cₜᵢ) = Yes ∀i
+   or we have a counter example vₛ, vₜ for which
+   | vₛ≊vₜ∈Sₖ ∧ cₛ(vₛ) ≠ Cₜₖ(vₜ)
+   then because 
+   | vₜ∈(a→πₖ) ⇒ Cₜ(vₜ) = Cₜₖ(vₜ)
+   then
+   | vₛ≊vₜ∈S ∧ Cₛ(vₛ)≠Cₜ(vₜ) 
+   and the result of the algorithm is
+   | equiv(Sᵢ, Cₛ, Cₜᵢ) = No(vₛ, vₜ) for some minimal k∈I