diff --git a/tesi/tesi.pdf b/tesi/tesi.pdf index 683ed05..0e971de 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 462e4ba..cff2ea3 100644 --- a/tesi/tesi_unicode.org +++ b/tesi/tesi_unicode.org @@ -1,4 +1,5 @@ \begin{comment} +TODO: not all todos are explicit. Check every comment section TODO: chiedi a Gabriel se T e S vanno bene, ma prima controlla che siano coerenti * TODO Scaletta [1/6] - [X] Introduction @@ -1251,10 +1252,10 @@ $(\EquivTEX S {C_S} {C_T} G)$, defined below. * Correctness of the algorithm Running a program tₛ or its translation 〚tₛ〛 against an input vₛ produces as a result /r/ in the following way: -| ( 〚tₛ〛ₛ(vₛ) = Cₛ(vₛ) ) → r +| ( 〚tₛ〛ₛ(vₛ) ≡ Cₛ(vₛ) ) → r | tₛ(vₛ) → r Likewise -| ( 〚tₜ〛ₜ(vₜ) = Cₜ(vₜ) ) → r +| ( 〚tₜ〛ₜ(vₜ) ≡ Cₜ(vₜ) ) → r | tₜ(vₜ) → r where result r ::= guard list * (Match blackbox | NoMatch | Absurd) and guard ::= blackbox. @@ -1268,10 +1269,10 @@ of decision 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 -decision 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. +The result of the proposed equivalence algorithm is /Yes/ or /No(vₛ, +vₜ)/. In particular, in the negative case, vₛ and vₜ are a couple of +possible counter examples for which the decision trees produce a +different result. ** Statements Theorem. We say that a translation of a source program to a decision tree @@ -1312,12 +1313,12 @@ target program we say: *** Proof of the correctness of the translation from source programs to source decision trees -We define a source term tₛ as a collection of patterns pointing to blackboxes +We define the source term tₛ as a collection of patterns pointing to blackboxes | tₛ ::= (p → bb)^{i∈I} A pattern is defined as either a constructor pattern, an or pattern or a constant pattern -| p ::= | K(pᵢ)ⁱ, i ∈ I | (p|q) | n ∈ ℕ +| p ::= \vert K(pᵢ)ⁱ, i ∈ I \vert (p\vert{}q) \vert n ∈ ℕ A decision tree is defined as either a Leaf, a Failure terminal or an intermediate node with different children sharing the same accessor /a/ @@ -1327,9 +1328,9 @@ possible input values /S/. The fallback is not needed when the user doesn't use a wildcard pattern. %%% Give example of thing -| Cₛ ::= Leaf bb | Switch(a, (Kᵢ → Cᵢ)^{i∈S} , C?) -| a ::= Here | n.a -| vₛ ::= K(vᵢ)^{i∈I} | n ∈ ℕ +| Cₛ ::= Leaf bb \vert Switch(a, (Kᵢ → Cᵢ)^{i∈S} , C?) +| a ::= Here \vert n.a +| vₛ ::= K(vᵢ)^{i∈I} \vert n ∈ ℕ \begin{comment} Are K and Here clear here? @@ -1361,12 +1362,12 @@ 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 +1. [| ∅, (∅ → bbᵢ)ⁱ |] ≡ Leaf bbᵢ where i := min(I), that is a decision 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 + the first expression and (Leaf bb)(v) := Match bb +2. [| (aⱼ)ʲ, ∅ |] ≡ Failure Regarding non base cases: Let's first define @@ -1396,10 +1397,10 @@ occurs on the first row of m, plus one "wildcard submatrix" m_{wild} that matches on all values that do not start with one of those head constructors. -Intuitively, m is equivalent to its decompositionin the following -sense: if the first pattern of an input vector (v_i)^i starts with one -of the head constructors k, then running (v_i)^i against m is the same -as running it against the submatrix m_k; otherwise (its head +Intuitively, m is equivalent to its decomposition in the following +sense: if the first pattern of an input vector (vᵢ)ⁱ starts with one +of the head constructors k, then running (vᵢ)ⁱ against m is the same +as running it against the submatrix mₖ; otherwise (its head constructor is none of the k) it is equivalent to running it against the wildcard submatrix. @@ -1466,21 +1467,23 @@ TODO: put ^i∈I where needed \end{comment} \subsubsection{The trimming lemma} The trimming lemma allows to reduce the size of a decision tree given -an accessor → π relation (TODO: expand) -| ∀vₜ ∈ (a→π), Cₜ(vₜ) = C_{t/a→π(kᵢ)}(vₜ) +an accessor /a/ → π relation (TODO: expand) +| ∀vₜ ∈ (a→π), Cₜ(vₜ) = C_{t/a→π}(vₜ) We prove this by induction on Cₜ: - a. Cₜ = Leaf_{bb}: when the decision tree is a leaf terminal, we - know that - | Leaf_{bb/a→π}(v) = Leaf_{bb}(v) - That means that the result of trimming on a Leaf is the Leaf itself - b. The same applies to Failure terminal - | Failure_{/a→π}(v) = Failure(v) - c. When Cₜ = Switch(b, (π→Cᵢ)ⁱ)_{/a→π} then - we look at the accessor /a/ of the subtree Cᵢ and - we define πᵢ' = πᵢ if a≠b else πᵢ∩π - Trimming a switch node yields the following result: - | Switch(b, (π→Cᵢ)ⁱ)_{/a→π} := Switch(b, (π'ᵢ→C_{i/a→π})ⁱ) +- Cₜ = Leaf_{bb}: when the decision tree is a leaf terminal, the result of trimming on a Leaf is the Leaf itself + | Leaf_{bb/a→π}(v) = Leaf_{bb}(v) +- The same applies to Failure terminal + | Failure_{/a→π}(v) = Failure(v) +- When Cₜ = Switch(b, (π→Cᵢ)ⁱ)_{/a→π} then we look at the accessor + /a/ of the subtree Cᵢ and we define πᵢ' = πᵢ if a≠b else πᵢ∩π Trimming + a switch node yields the following result: + | Switch(b, (π→Cᵢ)^{i∈I})_{/a→π} := Switch(b, (π'ᵢ→C_{i/a→π})^{i∈I}) + +\begin{comment} +TODO: understand how to properly align lists +check that every list is aligned +\end{comment} \begin{comment} Actually in the proof.org file I transcribed: e. Unreachabe → ⊥ @@ -1488,14 +1491,14 @@ This is not correct because you don't have Unreachable nodes in target decision \end{comment} For the trimming lemma we have to prove that running the value vₜ against -the decistion tree Cₜ is the same as running vₜ against the tree +the decision tree Cₜ is the same as running vₜ against the tree C_{trim} that is the result of the trimming operation on Cₜ -| Cₜ(vₜ) = C_{trim}(vₜ) = Switch(b, (πᵢ'→C_{i/a→π})ⁱ)(vₜ) +| Cₜ(vₜ) = C_{trim}(vₜ) = Switch(b, (πᵢ'→C_{i/a→π})^{i∈I})(vₜ) We can reason by first noting that when vₜ∉(b→πᵢ)ⁱ the node must be a Failure node. -In the case where ∃k| vₜ∈(b→πₖ) then we can prove that -| C_{k/a→π}(vₜ) = Switch(b, (πᵢ'→C_{i/a→π})ⁱ)(vₜ) +In the case where ∃k \vert{} vₜ∈(b→πₖ) then we can prove that +| C_{k/a→π}(vₜ) = Switch(b, (πᵢ'→C_{i/a→π})^{i∈I})(vₜ) because when a ≠ b then πₖ'= πₖ and this means that vₜ∈πₖ' -while when a = b then πₖ'=(πₖ∩π) and vt∈πₖ' because: +while when a = b then πₖ'=(πₖ∩π) and vₜ∈πₖ' because: - by the hypothesis, vₜ∈π - we are in the case where vₜ∈πₖ So vₜ ∈ πₖ' and by induction @@ -1517,7 +1520,7 @@ Covering lemma: \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ₜ) +| equiv(S, Cₛ, Cₜ) → Yes \vert{} No(vₛ, vₜ) When the algorithm returns Yes and the input space is covered by /Cₛ/ we can say that the couple of decision trees are the same for @@ -1563,8 +1566,8 @@ I think the unreachable case should go at the end. |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ₛ, Switch(a, (πᵢ → Cₜᵢ)ⁱ)) := Forall(equiv( S∩a→π(kᵢ)), Cₛ, Cₜᵢ)ⁱ) - | equiv(S, Leaf bbₛ as Cₛ, Switch(a, (πᵢ → Cₜᵢ)ⁱ)) := Forall(equiv( S∩a→π(kᵢ)), Cₛ, Cₜᵢ)ⁱ) + | equiv(S, Failure as Cₛ, Switch(a, (πᵢ → Cₜᵢ)^{i∈I})) := Forall(equiv( S∩a→π(kᵢ)), Cₛ, Cₜᵢ)^{i∈I}) + | equiv(S, Leaf bbₛ as Cₛ, Switch(a, (πᵢ → Cₜᵢ)^{i∈I})) := Forall(equiv( S∩a→π(kᵢ)), Cₛ, Cₜᵢ)^{i∈I}) The algorithm either returns Yes for every sub-input space Sᵢ := S∩(a→π(kᵢ)) and subtree Cₜᵢ | equiv(Sᵢ, Cₛ, Cₜᵢ) = Yes ∀i @@ -1577,13 +1580,13 @@ I think the unreachable case should go at the end. | equiv(Sᵢ, Cₛ, Cₜᵢ) = No(vₛ, vₜ) for some minimal k∈I 4. When we have a Switch on the right we define πₙ as the domain of values not covered but the union of the constructors kᵢ - | πₙ = ¬(⋃π(kᵢ)ⁱ) + | πₙ = ¬(⋃π(kᵢ)^{i∈I}) The algorithm proceeds by trimming - | equiv(S, Switch(a, (kᵢ → Cₛᵢ)ⁱ, C_{sf}), Cₜ) := - | Forall(equiv( S∩(a→π(kᵢ)ⁱ), Cₛᵢ, C_{t/a→π(kᵢ)})ⁱ +++ equiv(S∩(a→π(kᵢ)), Cₛ, C_{a→πₙ})) + | equiv(S, Switch(a, (kᵢ → Cₛᵢ)^{i∈I}, C_{sf}), Cₜ) := + | Forall(equiv( S∩(a→π(kᵢ)^{i∈I}), Cₛᵢ, C_{t/a→π(kᵢ)})^{i∈I} +++ equiv(S∩(a→πₙ), 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 + | Forall(equiv( S∩(a→π(kᵢ)^{i∈I}), Cₛᵢ, C_{t/a→π(kᵢ)})^{i∈I} = 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