correzioni Gabriel piu` apici
This commit is contained in:
Francesco Mecca
parent
67ae30a28d
commit
1ec9393e38
2 changed files with 46 additions and 43 deletions
BIN
tesi/tesi.pdf
BIN
tesi/tesi.pdf
Binary file not shown.
|
|
@ -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
|
||||
|
|
@ -1397,9 +1398,9 @@ that matches on all values that do not start with one of those head
|
|||
constructors.
|
||||
|
||||
Intuitively, m is equivalent to its decomposition in 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
|
||||
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
|
||||
|
|
|
|||
Loading…
Reference in a new issue