diff --git a/tesi/tesi.pdf b/tesi/tesi.pdf index aba1c5e..6644301 100644 Binary files a/tesi/tesi.pdf and b/tesi/tesi.pdf differ diff --git a/tesi/tesi_unicode.org b/tesi/tesi_unicode.org index d718580..c4409c2 100644 --- a/tesi/tesi_unicode.org +++ b/tesi/tesi_unicode.org @@ -1,4 +1,6 @@ \begin{comment} +TODO: neg is parsed incorrectly +TODO: chiedi a Gabriel se T e S vanno bene, ma prima controlla che siano coerenti * TODO Scaletta [1/6] - [X] Introduction - [-] Background [80%] @@ -1396,7 +1398,6 @@ m := ((a_i)^i ((p_{ij})^i \to e_j)^{ij}) (k_k)^k := headconstructor(p_{i0})^i \] \begin{equation} -\begin{align} Groups(m) := ( k_k \to ((a)_{0.l})^{l \in Idx(k_k)} +++ (a_i)^{i \in I\backslash \{0\} }), \\ ( if p_{0j} is k(q_l) then \\ (qₗ)^{l \in Idx(k_k)} +++ (p_{ij})^{i \in I\backslash \{0\}} \to e_j \\ @@ -1404,7 +1405,6 @@ m := ((a_i)^i ((p_{ij})^i \to e_j)^{ij}) (\_)^{l \in Idx(k_k)} +++ (p_{ij})^{i \in I\backslash \{0\}} \to e_j \\ else \bot )^j ), \\ ((a_i)^{i \in I\backslash \{0\}}, ((p_{ij})^{i \in I\backslash \{0\}} \to eⱼ if p_{0j} is \_ else \bot)^{j \in J}) -\end{align} \end{equation} Groups(m) is an auxiliary function that decomposes a matrix m into @@ -1516,7 +1516,7 @@ an accessor → π relation (In other words???) Should I swap π and π' \end{comment} -\subsubsection Proof of equivalence checking +\subsubsection{Equivalence checking} The equivalence checking algorithm takes as parameters an input space /S/, a source decision tree /Cₛ/ and a target decision tree /Cₜ/: | equiv(S, Cₛ, Cₜ) → Yes | No(vₛ, vₜ) @@ -1539,9 +1539,9 @@ We define the following | 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} +| int(k) ∈ ℕ (arity(k) = 0) +| tag(k) ∈ ℕ (arity(k) > 0) +| π(k) = {n\vert int(k) = n} x {n\vert tag(k) = n} where k is a constructor. \begin{comment} @@ -1554,51 +1554,52 @@ We proceed by case analysis: I start numbering from zero to leave the numbers as they were on the blackboard, were we skipped some things I think the unreachable case should go at the end. \end{comment} -0. in case of unreachable: Cₛ(vₛ) = Absurd(Unreachable) ≠ Cₜ(vₜ) ∀vₛ,vₜ +0. in case of unreachable: +| Cₛ(vₛ) = Absurd(Unreachable) ≠ Cₜ(vₜ) ∀vₛ,vₜ 1. In the case of an empty input space -| equiv(∅, Cₛ, Cₜ) := Yes -and that is trivial to prove because there is no pair of values (vₛ, vₜ) that could be -tested against the decision trees. -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 decision tree - /Cₛ/ that is either a Leaf terminal or a Failure terminal and a - target decision 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 + | equiv(∅, Cₛ, Cₜ) := Yes + and that is trivial to prove because there is no pair of values (vₛ, vₜ) that could be + tested against the decision trees. + In the other subcases S is always non-empty. +2. When there are /Failure/ nodes at both sides the result is /Yes/: + |equiv(S, Failure, Failure) := Yes + Given that ∀v, Failure(v) = Failure, the statement holds. +3. When we have a Leaf or a Failure at the left side: + | equiv(S, Failure as Cₛ, Node(a, (πᵢ → Cₜᵢ)ⁱ)) := Forall(equiv( S∩a→π(kᵢ)), Cₛ, Cₜᵢ)ⁱ) + | equiv(S, Leaf bbₛ as Cₛ, Node(a, (πᵢ → Cₜᵢ)ⁱ)) := Forall(equiv( S∩a→π(kᵢ)), Cₛ, Cₜᵢ)ⁱ) + The algorithm either returns Yes for every sub-input space Sᵢ := S∩(a→π(kᵢ)) 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ₜ∈(a→πₖ) → Cₜ(vₜ) = Cₜₖ(vₜ) , | vₛ≃vₜ∈S ∧ Cₛ(vₛ)≠Cₜ(vₜ) - and the result of the algorithm is + we can say that | equiv(Sᵢ, Cₛ, Cₜᵢ) = No(vₛ, vₜ) for some minimal k∈I -4. equiv(S, Node(a, (kᵢ → Cₛᵢ)ⁱ, C_{sf}), Cₜ) := - let π' = ⋃π(kᵢ) ∀i in - Forall(equiv( S∩(a→π(kᵢ)ⁱ), Cₛᵢ, C_{t/a→π(kᵢ)})ⁱ +++ equiv(S∩(a→π(kᵢ)), Cₛ, C_{/a̸¬̸π'})) - The statement holds because: - a. Forall(equiv( S∩(a→π(kᵢ)ⁱ), Cₛᵢ, C_{t/a→π(kᵢ)})ⁱ = Yes - In the yes case let's reason by case analysis: - i. When k∈(kᵢ)ⁱ - there is a k=kₖ for some k and this means that Cₛ(vₛ) = Cₛᵢ(vₛ) - By induction we know that Cₛᵢ(vₛ) = c_{t/a→πᵢ}(vₜ) - and because of the trimming lemma: - Cₜ(vₜ) = C_{t/a→πᵢ}(vₜ) - Putting all together: - Cₛ(vₛ) = Cₛᵢ(vₛ) = C_{t/a→πᵢ}(vₜ) = Cₜ(vₜ) +4. When we have a Node on the right we define πₙ as the domain of + values not covered but the union of the constructors kᵢ + | πₙ = ¬(⋃π(kᵢ)ⁱ) + The algorithm proceeds by trimming + | equiv(S, Node(a, (kᵢ → Cₛᵢ)ⁱ, C_{sf}), Cₜ) := + | Forall(equiv( S∩(a→π(kᵢ)ⁱ), Cₛᵢ, C_{t/a→π(kᵢ)})ⁱ +++ equiv(S∩(a→π(kᵢ)), Cₛ, C_{a→πₙ})) + The statement still holds and we show this by first analyzing the + /Yes/ case: + | Forall(equiv( S∩(a→π(kᵢ)ⁱ), Cₛᵢ, C_{t/a→π(kᵢ)})ⁱ = Yes + The constructor k is either included in the set of constructors kᵢ: + | k \vert k∈(kᵢ)ⁱ ∧ Cₛ(vₛ) = Cₛᵢ(vₛ) + We also know that + | (1) Cₛᵢ(vₛ) = C_{t/a→πᵢ}(vₜ) + | (2) C_{T/a→πᵢ}(vₜ) = Cₜ(vₜ) + (1) is true by induction and (2) is a consequence of the trimming lemma. + Putting everything together: + | Cₛ(vₛ) = Cₛᵢ(vₛ) = C_{T/a→πᵢ}(vₜ) = Cₜ(vₜ) - ii. when k∉(kᵢ)ⁱ ??? + When the k∉(kᵢ)ⁱ [TODO] - b. Forall(...) = No(vₛ, vₜ) - for a minimum k, equiv(Sₖ, Cₛₖ, C_{t/a→πₖ} = No(vₛ, vₜ) - then Cₛₖ(vₛ) ≠ C_{t/a→πₖ}(vₜ) and C_{t/a→πₖ}(vₜ) = Cₜ(vt) - => (Cₛₖ(vₛ) = Cₛ(vₛ)) ≠ Cₜ(vₜ) - # Same for fallback? + The auxiliary Forall function returns /No(vₛ, vₜ)/ when, for a minimum k, + | equiv(Sₖ, Cₛₖ, C_{T/a→πₖ} = No(vₛ, vₜ) + Then we can say that + | Cₛₖ(vₛ) ≠ C_{t/a→πₖ}(vₜ) + that is enough for proving that + | Cₛₖ(vₛ) ≠ (C_{t/a→πₖ}(vₜ) = Cₜ(vₜ))