diff --git a/tesi/conv.py b/tesi/conv.py index 8922bfe..a2ef3e6 100644 --- a/tesi/conv.py +++ b/tesi/conv.py @@ -7,7 +7,7 @@ try: except: allsymbols = json.load(open('../unicode-latex.json')) -mysymbols = ['≡', '≠', '≼', '→', '←', '⊀', '⋠', '≺', '∀', 'ε', '₀', '₂', '₁', '₃', '₄', 'ₐ', 'ₖ', 'ₘ', 'ₙ', 'ᵢ', 'ⁱ', '⋮', 'ₛ', 'ₜ', '≃', '⇔', '∧', '∅', 'ℕ', 'ⱼ', 'ʲ', '⊥', 'π', 'α', 'β', '∞', 'σ', '≤', '⊈', '∧', '∨', '∃', '⇒', '∩', '∉', '⋃', 'ᵏ', 'ₗ', 'ˡ', 'ₒ', 'ᵣ', 'ᴵ', '≈', '⊆' ] +mysymbols = ['≡', '≠', '≼', '→', '←', '⊀', '⋠', '≺', '∀', 'ε', '₀', '₂', '₁', '₃', '₄', 'ₐ', 'ₖ', 'ᵥ', 'ₘ', 'ₙ', 'ᵢ', 'ⁱ', '⋮', 'ₛ', 'ₜ', '≃', '⇔', '∧', '∅', 'ℕ', 'ⱼ', 'ʲ', '⊥', 'π', 'α', 'β', '∞', 'σ', '≤', '⊈', '∧', '∨', '∃', '⇒', '∩', '∉', '⋃', 'ᵏ', 'ₗ', 'ˡ', 'ₒ', 'ᵣ', 'ᴵ', '≈', '⊆' ] extrasymbols = {'〚': '\llbracket', '〛': r'\rrbracket', '̸': '\neg', '¬̸': '\neg', '∈': '\in ', 'ₛ': '_S', 'ₜ': '_T'} symbols = {s: allsymbols[s] for s in mysymbols} diff --git a/tesi/drafts/partial-decomposition-proof.org b/tesi/drafts/partial-decomposition-proof.org new file mode 100644 index 0000000..a339387 --- /dev/null +++ b/tesi/drafts/partial-decomposition-proof.org @@ -0,0 +1,139 @@ +# done +Auxiliary operations: + + index family of a constructor + Idx(K) := [0; arity(K)[ + + head of an ordered family (we write x for any object here, value, pattern etc.) + head((xᵢ)^{i ∈ I}) = x_min(I) + + tail of an ordered family + tail((xᵢ)^{i ∈ I}) := (xᵢ)^{i ≠ min(I)} + + head constructor of a value or pattern + constr(K(xᵢ)ⁱ) = K + constr(_) = ⊥ + constr(x) = ⊥ + + first non-⊥ element of an ordered family + First((xᵢ)ⁱ) := ⊥ if ∀i, xᵢ = ⊥ + First((xᵢ)ⁱ) := x_min{i | xᵢ ≠ ⊥} if ∃i, xᵢ ≠ ⊥ +# end + +Definition of running a pattern row against a (same-size) value vector (pᵢ)ⁱ(vᵢ)ⁱ + ∅ (∅) := [] + (_, tail(pᵢ)ⁱ) (vᵢ) := tail(pᵢ)ⁱ(tail(vᵢ)ⁱ) + (x, tail(pᵢ)ⁱ) (vᵢ) := σ[x↦v₀] if tail(pᵢ)ⁱ(tail(vᵢ)ⁱ) = σ + (K(qⱼ)ʲ, tail(pᵢ)ⁱ) (K(v'ⱼ)ʲ,tail(vⱼ)ʲ) := ((qⱼ)ʲ +++ tail(pᵢ)ⁱ)((v'ⱼ)ʲ +++ tail(vᵢ)ⁱ) + (K(qⱼ)ʲ, tail(pᵢ)ⁱ) (K'(v'ₗ)ˡ,tail(vⱼ)ʲ) := ⊥ if K ≠ K' + (q₁|q₂, tail(pᵢ)ⁱ) (vᵢ)ⁱ := First((q₁,tail(pᵢ)ⁱ)(vᵢ)ⁱ, (q₂,tail(pᵢ)ⁱ)(vᵢ)ⁱ) + +Definition of group decomposition: + let constrs((pᵢ)^{i ∈ I}) = { K | K = constr(pᵢ), i ∈ I } + let Groups(m) where m = ((aᵢ)ⁱ ((pᵢⱼ)ⁱ → eⱼ)ⁱʲ) = + let (Kₖ)ᵏ = constrs(pᵢ₀)ⁱ in + ( Kₖ → + ((a₀.ₗ)ˡ +++ tail(aᵢ)ⁱ) + ( + if pₒⱼ is Kₖ(qₗ) then + (qₗ)ˡ +++ tail(pᵢⱼ)ⁱ → eⱼ + if pₒⱼ is _ then + (_)ˡ +++ tail(pᵢⱼ)ⁱ → eⱼ + else ⊥ + )ʲ + ), ( + tail(aᵢ)ⁱ, (tail(pᵢⱼ)ⁱ → eⱼ if p₀ⱼ is _ else ⊥)ʲ + ) + +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" m_{wild} +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 +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ᵣ → mᵣ)ᵏ, m_{wild}$. + For any value vector $(vᵢ)ᴵ$ such that $v₀ = K(v'ₗ)ˡ$ for some + constructor K, + we have: + \[ + if K = Kₖ for some k then + m(vᵢ)ⁱ = mₖ((v'ₗ)ˡ +++ (vᵢ)^{i∈I\{0}}) + otherwise + m(vᵢ)ⁱ = m_{wild}(vᵢ)^{i∈I\{0}} + \] + +Proof: + + Let $m$ be a matrix ((aᵢ)ⁱ, ((pᵢⱼ)ⁱ → eⱼ)ʲ) with $Groups(m) = (Kₖ → mₖ)ᵏ, m_{wild}$. + + Below we are going to assume that m is a simplified matrix: + + the first row does not with an or-pattern or a variable + + I think it would be simpler to not consider them at all in the + formalization. If we do want them, the discrepancy can be fixed + later by defining a simplification step that explodes + head-or-patterns and binds variable, and showing that it preserves + the matrix semantics. + + Let (vᵢ)ⁱ be an input matrix with v₀ = Kᵥ(v'ₗ)ˡ for some constructor Kᵥ. + + We have to show that: + - if Kₖ = Kᵥ for some Kₖ ∈ constrs(p₀ⱼ)ʲ, then + m(vᵢ)ⁱ = mₖ((v'ₗ)ˡ +++ tail(vᵢ)ⁱ) + - otherwise + m(vᵢ)ⁱ = m_{wild}(tail(vᵢ)ⁱ) + + Let us call (rₖⱼ) the j-th row of the submatrix mₖ, and rⱼ_{wild} + the j-th row of the wildcard submatrix m_{wild}. + + Our goal contains same-behavior equalities between matrices, for + a fixed input vector (vᵢ)ⁱ. It suffices to show same-behavior + equalities between each row of the matrices for this input + vector. We show that for any j, + + - if Kₖ = Kᵥ for some Kₖ ∈ constrs(p₀ⱼ)ʲ, then + (pᵢⱼ)ⁱ(vᵢ)ⁱ = rₖⱼ((v'ₗ)ˡ +++ tail(vᵢ)ⁱ + - otherwise + (pᵢⱼ)ⁱ(vᵢ)ⁱ = rⱼ_{wild} tail(vᵢ)ⁱ + + In the first case (Kᵥ is Kₖ for some Kₖ ∈ constrs(p₀ⱼ)ʲ), we + have to prove that + + (pᵢⱼ)ⁱ(vᵢ)ⁱ = rₖⱼ((v'ₗ)ˡ +++ tail(vᵢ)ⁱ + + By definition of mₖ we know that rₖⱼ is equal to + + if pₒⱼ is Kₖ(qₗ) then + (qₗ)ˡ +++ tail(pᵢⱼ)ⁱ → eⱼ + if pₒⱼ is _ then + (_)ˡ +++ tail(pᵢⱼ)ⁱ → eⱼ + else ⊥ + + By definition of (pᵢ)ⁱ(vᵢ)ⁱ we know that (pᵢⱼ)ⁱ(vᵢ) is equal to + + (K(qⱼ)ʲ, tail(pᵢⱼ)ⁱ) (K(v'ₗ)ˡ,tail(vᵢ)ⁱ) := ((qⱼ)ʲ +++ tail(pᵢⱼ)ⁱ)((v'ₗ)ˡ +++ tail(vᵢ)ⁱ) + (_, tail(pᵢⱼ)ⁱ) (vᵢ) := tail(pᵢⱼ)ⁱ(tail(vᵢ)ⁱ) + (K(qⱼ)ʲ, tail(pᵢⱼ)ⁱ) (K'(v'ₗ)ˡ,tail(vⱼ)ʲ) := ⊥ if K ≠ K' + + We prove this first case by a second case analysis on p₀ⱼ. + + TODO + + In the second case (Kᵥ is distinct from Kₖ for all Kₖ ∈ constrs(pₒⱼ)ʲ), + we have to prove that + + (pᵢⱼ)ⁱ(vᵢ)ⁱ = rⱼ_{wild} tail(vᵢ)ⁱ + + TODO diff --git a/tesi/tesi.pdf b/tesi/tesi.pdf index 841baf2..3a55c06 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 13e63cf..9fd3215 100644 --- a/tesi/tesi_unicode.org +++ b/tesi/tesi_unicode.org @@ -336,7 +336,7 @@ for content equality. \end{mathpar} If the source decision tree (left hand side) is a terminal while the -target decistion tree (right hand side) is not, the algorithm proceeds +target decisiorn tree (right hand side) is not, the algorithm proceeds by \emph{explosion} of the right hand side. Explosion means that every child of the right hand side is tested for equality against the left hand side. @@ -1316,92 +1316,120 @@ Base cases: the first expression and (Leaf bb)(v) := Match bb 2. [| (aⱼ)ʲ, ∅ |] ≡ Failure Regarding non base cases: -Let's first define -| let Idx(k) := [0; arity(k)[ -| let First(∅) := ⊥ -| let First((aⱼ)ʲ) := a_{min(j∈J≠∅)} -\[ -m := ((a_i)^i ((p_{ij})^i \to e_j)^{ij}) -\] -\[ - (k_k)^k := headconstructor(p_{i0})^i -\] -| Groups(m) := (k_{k} \to ((a)_{0.l})^{l \in Idx(k_{k})} +++ (a_{i})^{i\in{}I\DZ}), -|( -| \quad if p_{0j} is k(q_{l}) then -| \quad \quad \quad (qₗ)^{l \in Idx(k_k)} +++ (p_{ij})^{i\in{}I\DZ} \to e_{j} -| \quad if p_{0j} is "_" then -| \quad \quad \quad ("_")^{l \in Idx(k_{k})} +++ (p_{ij})^{i\in{}I\DZ} \to e_{j} -| \quad else \bot -|)^{j ∈ J}, -| ((a_{i})^{i\in{}I\DZ}, ((p_{ij})^{i\in{}I\DZ} \to eⱼ if p_{0j} is \_ else \bot)^{j\in{}J}) -Groups(m) is an auxiliary function that source a matrix m into +Let's first define some auxiliary functions +- The index family of a constructor + | Idx(K) := [0; arity(K)[ +- head of an ordered family (we write x for any object here, value, pattern etc.) + | head((xᵢ)^{i ∈ I}) = x_min(I) +- tail of an ordered family + | tail((xᵢ)^{i ∈ I}) := (xᵢ)^{i ≠ min(I)} +- head constructor of a value or pattern + | constr(K(xᵢ)ⁱ) = K + | constr(_) = ⊥ + | constr(x) = ⊥ +- first non-⊥ element of an ordered family + | First((xᵢ)ⁱ) := ⊥ \quad \quad \quad if ∀i, xᵢ = ⊥ + | First((xᵢ)ⁱ) := x_min{i \vert{} xᵢ ≠ ⊥} \quad if ∃i, xᵢ ≠ ⊥ +- definition of group decomposition: +| let constrs((pᵢ)^{i ∈ I}) = { K \vert{} K = constr(pᵢ), i ∈ I } +| let Groups(m) where m = ((aᵢ)ⁱ ((pᵢⱼ)ⁱ → eⱼ)ⁱʲ) = +| \quad let (Kₖ)ᵏ = constrs(pᵢ₀)ⁱ in +| \quad ( Kₖ → +| \quad \quad ((a₀.ₗ)ˡ +++ tail(aᵢ)ⁱ) +| \quad \quad ( +| \quad \quad if pₒⱼ is Kₖ(qₗ) then +| \quad \quad \quad (qₗ)ˡ +++ tail(pᵢⱼ)ⁱ → eⱼ +| \quad \quad if pₒⱼ is _ then +| \quad \quad \quad (_)ˡ +++ tail(pᵢⱼ)ⁱ → eⱼ +| \quad \quad else ⊥ +| \quad \quad )ʲ +| \quad ), ( +| \quad \quad tail(aᵢ)ⁱ, (tail(pᵢⱼ)ⁱ → eⱼ if p₀ⱼ is _ else ⊥)ʲ +| \quad ) +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 +Groups(m) returns one submatrix m_r for each head constructor K that 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 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 +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ₖ \text{ for some k then} -| \quad m(vᵢ)ⁱ = mₖ((v_{l}')ˡ +++ (v_{i})^{i∈I\DZ}) -| \text{else} -| \quad m(vᵢ)ⁱ = m_{wild}(vᵢ)^{i∈I\DZ} +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ₖ \text{ for some k then} + | \quad m(vᵢ)ⁱ = mₖ((v_{l}')ˡ +++ (v_{i})^{i∈I\DZ}) + | \text{else} + | \quad m(vᵢ)ⁱ = m_{wild}(vᵢ)^{i∈I\DZ} \begin{comment} TODO: fix \{0} \end{comment} *** 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ₖ)ᵏ +Let /m/ be a matrix ((aᵢ)ⁱ, ((pᵢⱼ)ⁱ → eⱼ)ʲ) with +| Groups(m) = (Kₖ → mₖ)ᵏ, m_{wild} +Below we are going to assume that m is a simplified matrix such that +the first row does not contain an or-pattern or a binding to a +variable. -Both m(vᵢ)ⁱ and mₖ(vₖ)ᵏ are defined as the first matching result of -a family over each row rⱼ of a matrix +Let (vᵢ)ⁱ be an input matrix with v₀ = Kᵥ(v'_{l})ˡ for some constructor Kᵥ. +We have to show that: +- if Kₖ = Kᵥ for some Kₖ ∈ constrs(p₀ⱼ)ʲ, then + m(vᵢ)ⁱ = mₖ((v'ₗ)ˡ +++ tail(vᵢ)ⁱ) +- otherwise + m(vᵢ)ⁱ = m_{wild}(tail(vᵢ)ⁱ) +Let us call (rₖⱼ) the j-th row of the submatrix mₖ, and rⱼ_{wild} +the j-th row of the wildcard submatrix m_{wild}. -We know, from the definition of -Groups(m), that mₖ is -| ((a){0.l})^{l∈Idx(kₖ)} +++ (aᵢ)^{i∈I\DZ}), -| ( -| \quad if p_{0j} is k(qₗ) then -| \quad \quad (qₗ)ˡ +++ (p_{ij})^{i∈I\DZ } → eⱼ -| \quad if p_{0j} is _ then -| \quad \quad (_)ˡ +++ (p_{ij})^{i∈I\DZ} → eⱼ -| \quad else ⊥ -| )^{j∈J} +Our goal contains same-behavior equalities between matrices, for +a fixed input vector (vᵢ)ⁱ. It suffices to show same-behavior +equalities between each row of the matrices for this input +vector. We show that for any j, +- if Kₖ = Kᵥ for some Kₖ ∈ constrs(p₀ⱼ)ʲ, then + | (pᵢⱼ)ⁱ(vᵢ)ⁱ = rₖⱼ((v'ₗ)ˡ +++ tail(vᵢ)ⁱ +- otherwise + | (pᵢⱼ)ⁱ(vᵢ)ⁱ = rⱼ_{wild} tail(vᵢ)ⁱ +In the first case (Kᵥ is Kₖ for some Kₖ ∈ constrs(p₀ⱼ)ʲ), we +have to prove that +| (pᵢⱼ)ⁱ(vᵢ)ⁱ = rₖⱼ((v'ₗ)ˡ +++ tail(vᵢ)ⁱ +By definition of mₖ we know that rₖⱼ is equal to +| if pₒⱼ is Kₖ(qₗ) then +| \quad (qₗ)ˡ +++ tail(pᵢⱼ)ⁱ → eⱼ +| if pₒⱼ is _ then +| \quad (_)ˡ +++ tail(pᵢⱼ)ⁱ → eⱼ +| else ⊥ +\begin{comment} +Maybe better as a table? +| pₒⱼ | rₖⱼ | +|--------+---------------------------| +| Kₖ(qₗ) | (qₗ)ˡ +++ tail(pᵢⱼ)ⁱ → eⱼ | +| _ | (_)ˡ +++ tail(pᵢⱼ)ⁱ → eⱼ | +| else | ⊥ | +\end{comment} +By definition of (pᵢ)ⁱ(vᵢ)ⁱ we know that (pᵢⱼ)ⁱ(vᵢ) is equal to +| (K(qⱼ)ʲ, tail(pᵢⱼ)ⁱ) (K(v'ₗ)ˡ,tail(vᵢ)ⁱ) := ((qⱼ)ʲ +++ tail(pᵢⱼ)ⁱ)((v'ₗ)ˡ +++ tail(vᵢ)ⁱ) +| (_, tail(pᵢⱼ)ⁱ) (vᵢ) := tail(pᵢⱼ)ⁱ(tail(vᵢ)ⁱ) +| (K(qⱼ)ʲ, tail(pᵢⱼ)ⁱ) (K'(v'ₗ)ˡ,tail(vⱼ)ʲ) := ⊥ if K ≠ K' -By definition, m(vᵢ)ⁱ is -| m(vᵢ)ⁱ = First(rⱼ(vᵢ)ⁱ)ʲ for m = ((aᵢ)ⁱ, (rⱼ)ʲ) -| (pᵢ)ⁱ (vᵢ)ⁱ = { -| \quad if p₀ = k(qₗ)ˡ, v₀ = k'(v'ₖ)ᵏ, k=Idx(k') and l=Idx(k) -| \quad \quad if k ≠ k' then ⊥ -| if k = k' then ((qₗ)ˡ +++ (pᵢ)^{i∈I\DZ}) ((v'ₖ)ᵏ +++ (vᵢ)^{i∈I\DZ} ) -| if p₀ = (q₁\vert{}q₂) then -| First( (q₁pᵢ^{i∈I\DZ}) vᵢ^{i∈I\DZ}, (q₂pᵢ^{i∈I \DZ}) vᵢ^{i∈I\DZ})} +We prove this first case by a second case analysis on p₀ⱼ. -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. +TODO -We can also show that aᵢ = (a_{0.l})ˡ +++ a_{i∈I\DZ} because v(a₀) = K(v(a){0.l})ˡ) +In the second case (Kᵥ is distinct from Kₖ for all Kₖ ∈ constrs(pₒⱼ)ʲ), +we have to prove that +| (pᵢⱼ)ⁱ(vᵢ)ⁱ = rⱼ_{wild} tail(vᵢ)ⁱ +TODO ** Target translation @@ -1597,7 +1625,7 @@ 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: +target program: | equiv(S, 〚tₛ〛ₛ, 〚tₜ〛ₜ, ∅) = Yes ⇔ tₛ ≃ tₜ