14 KiB
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ₛ) → 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 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.
Statements
Theorem. We say that a translation of a source program to a decision tree is correct when for every possible input, the source program and its respective decision 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 decision tree Cₜ. (TODO: rephrase)
Theorem: Given an input space S and a couple of decision trees, where the target decision tree Cₜ covers the input space S, we say that the two decision 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 decision 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ₜ |
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
| 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 ∈ ℕ |
A decision tree is defined as either a Leaf, a Failure terminal or an intermediate node with different children sharing the same accessor a and an optional fallback. Failure is emitted only when the patterns don't cover the whole set of 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 | Node(a, (Kᵢ → Cᵢ)i∈S , C?) |
| a ::= Here | n.a |
| vₛ ::= K(vᵢ)i∈I | n ∈ ℕ |
We define the decomposition matrix mₛ as
| SMatrix mₛ := (aⱼ)j∈J, ((pij)j∈J → bbᵢ)i∈I |
We define the decision tree of source programs 〚tₛ〛 in terms of the decision tree of pattern matrices 〚mₛ〛 by the following: 〚((pᵢ → bbᵢ)i∈I〛 := 〚(Root), (pᵢ → bbᵢ)i∈I 〛
decision 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[ |
We proceed to show the correctness of the invariant by a case analysys.
Base cases:
- [| ∅, (∅ → 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
- [| (aⱼ)ʲ, ∅ |] := Failure
Regarding non base cases: Let's first define
| let Idx(k) := [0; arity(k)[ |
| let First(∅) := ⊥ |
| let First((aⱼ)ʲ) := amin(j∈J≠∅) |
\[ m := ((a_i)^i ((p_{ij})^i \to e_j)^{ij}) \] \[ (k_k)^k := headconstructor(p_{i0})^i \]
\begin{equation} 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 \\ if p_{0j} is \_ then \\ (\_)^{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{equation}Groups(m) is an auxiliary function that decomposes a matrix m into submatrices, according to the head constructor of their first pattern. Groups(m) returns one submatrix m_r for each head constructor k that occurs on the first row of m, plus one "wildcard submatrix" mwild 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 constructor is none of the k) it is equivalent to running it against the wildcard submatrix.
We formalize this intuition as follows: Lemma (Groups): Let \[m\] be a matrix with \[Groups(m) = (k_r \to m_r)^k, m_{wild}\]. For any value vector \[(v_i)^l\] such that \[v_0 = k(v'_l)^l\] for some constructor k, we have: \[ if k = kₖ for some k then m(vᵢ)ⁱ = mₖ((v'ₗ)ˡ +++ (vᵢ)^{i∈I\backslash \{0\}}) else m(vᵢ)ⁱ = m_{wild}(vᵢ)^{i∈I\backslash \{0\}} \]
Proof:
Let \[m\] be a matrix with \[Group(m) = (k_r \to m_r)^k, m_{wild}\]. Let \[(v_i)^i\] be an input matrix with \[v_0 = k(v'_l)^l\] for some k. We proceed by case analysis:
- either k is one of the kₖ for some k
- or k is none of the (kₖ)ᵏ
Both m(vᵢ)ⁱ and mₖ(vₖ)ᵏ are defined as the first matching result of a family over each row rⱼ of a matrix
We know, from the definition of Groups(m), that mₖ is \[ ((a){0.l})^{l∈Idx(kₖ)} +++ (aᵢ)^{i∈I\backslash \{0\}}), ( if p_{0j} is k(qₗ) then (qₗ)ˡ +++ (p_{ij})^{i∈I\backslash \{0\}} → eⱼ if p_{0j} is _ then (_)ˡ +++ (p_{ij})^{i∈I\backslash \{0\}} → eⱼ else ⊥ )ʲ \]
By definition, m(vᵢ)ⁱ is
m(vᵢ)ⁱ = First(rⱼ(vᵢ)ⁱ)ʲ for m = ((aᵢ)ⁱ, (rⱼ)ʲ)
(pᵢ)ⁱ (vᵢ)ⁱ = {
if p₀ = k(qₗ)ˡ, v₀ = k'(v'ₖ)ᵏ, k=Idx(k') and l=Idx(k)
if k ≠ k' then ⊥
if k = k' then ((qₗ)ˡ + (pᵢ)^{i∈I\backslash \{0\}}) ((v'ₖ)ᵏ + (vᵢ)^{i∈I\backslash \{0\}})
if p₀ = (q₁|q₂) then
First( (q₁pᵢ^{i∈I \backslash \{0\}}) vᵢ^{i∈I \backslash \{0\}}, (q₂pᵢ^{i∈I \backslash \{0\}}) vᵢ^{i∈I \backslash \{0\}} )
}
For this reason, if we can prove that
| ∀j, rⱼ(vᵢ)ⁱ = r'ⱼ((v'ₖ)ᵏ ++ (vᵢ)ⁱ) |
it follows that
| m(vᵢ)ⁱ = mₖ((v'ₖ)ᵏ ++ (vᵢ)ⁱ) |
from the above definition.
We can also show that aᵢ = a0.lˡ + a_{i∈I\backslash \{0\}} because v(a₀) = K(v(a){0.l})ˡ)
Proof of equivalence checking
⊂subsection{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ₜ) = Ct/a→π(kᵢ)(vₜ) |
We prove this by induction on Cₜ:
- Cₜ = Leafbb: when the decision tree is a leaf terminal, we
know that
| Leafbb/a→π(v) = Leafbb(v) |
That means that the result of trimming on a Leaf is the Leaf itself
- The same applies to Failure terminal
| Failure/a→π(v) = Failure(v) |
- When Cₜ = Node(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:
| Node(b, (π→Cᵢ)ⁱ)/a→π := Node(b, (π'ᵢ→Ci/a→π)ⁱ) |
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 Ctrim that is the result of the trimming operation on Cₜ
| Cₜ(vₜ) = Ctrim(vₜ) = Node(b, (πᵢ'→Ci/a→π)ⁱ)(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
| Ck/a→π(vₜ) = Node(b, (πᵢ'→Ci/a→π)ⁱ)(vₜ) |
because when a ≠ b then πₖ'= πₖ and this means that vₜ∈πₖ' while when a = b then πₖ'=(πₖ∩π) and vt∈πₖ' because:
- by the hypothesis, vₜ∈π
- we are in the case where vₜ∈πₖ
So vₜ ∈ πₖ' and by induction
| Cₖ(vₜ) = Ck/a→π(vₜ) |
We also know that ∀vₜ∈(b→πₖ) → Cₜ(vₜ) = Cₖ(vₜ) By putting together the last two steps, we have proven the trimming lemma.
\begin{comment} TODO: what should I say about covering??? I swap π and π' Covering lemma: ∀a,π covers(Cₜ,S) → covers(C_{t/a→π}, (S∩a→π)) Uᵢπⁱ ≈ Uᵢπ'∩(a→π) ≈ (Uᵢπ')∩(a→π) %% %%%%%%% Also: Should I swap π and π' ? \end{comment}⊂subsection{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ₜ) |
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 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 decision 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) ∈ ℕ (arity(k) = 0) |
| tag(k) ∈ ℕ (arity(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:
\begin{comment} 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}- in case of unreachable:
| Cₛ(vₛ) = Absurd(Unreachable) ≠ Cₜ(vₜ) ∀vₛ,vₜ |
-
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.
-
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.
-
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ₜ) , vₛ≃vₜ∈S ∧ Cₛ(vₛ)≠Cₜ(vₜ) we can say that
equiv(Sᵢ, Cₛ, Cₜᵢ) = No(vₛ, vₜ) for some minimal k∈I -
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ₛᵢ)ⁱ, Csf), Cₜ) := Forall(equiv( S∩(a→π(kᵢ)ⁱ), Cₛᵢ, Ct/a→π(kᵢ))ⁱ +equiv(S∩(a→π(kᵢ)), Cₛ, Ca→πₙ))The statement still holds and we show this by first analyzing the Yes case:
Forall(equiv( S∩(a→π(kᵢ)ⁱ), Cₛᵢ, Ct/a→π(kᵢ))ⁱ = Yes The constructor k is either included in the set of constructors kᵢ:
k | k∈(kᵢ)ⁱ ∧ Cₛ(vₛ) = Cₛᵢ(vₛ) We also know that
(1) Cₛᵢ(vₛ) = Ct/a→πᵢ(vₜ) (2) CT/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ₛ) = CT/a→πᵢ(vₜ) = Cₜ(vₜ) When the k∉(kᵢ)ⁱ [TODO]
The auxiliary Forall function returns No(vₛ, vₜ) when, for a minimum k,
equiv(Sₖ, Cₛₖ, CT/a→πₖ = No(vₛ, vₜ) Then we can say that
Cₛₖ(vₛ) ≠ Ct/a→πₖ(vₜ) that is enough for proving that
Cₛₖ(vₛ) ≠ (Ct/a→πₖ(vₜ) = Cₜ(vₜ))