altro

tesi/tesi_unicode.org

@@ -798,6 +798,7 @@ respective constraint tree produces the same result
 
 | ∀vₛ, tₛ(vₛ) = 〚tₛ〛ₛ(vₛ)
 
+
 Likewise, for the target language:
 
 | ∀vₜ, tₜ(vₜ) = 〚tₜ〛ₜ(vₜ)
@@ -825,3 +826,44 @@ 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 constraint 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 constraint 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.
+
+| Cₛ ::= Leaf bb | Node(a, (Kᵢ → Cᵢ)^{i∈S} , C?)
+| a ::= Here | n.a
+| vₛ ::= K(vᵢ)^{i∈I} | n ∈ ℕ
+
+\begin{comment}
+Are K and Here clear here?
+\end{comment}
+
+We define the decomposition matrix /mₛ/ as
+| SMatrix mₛ := (aⱼ)^{j∈J}, ((pᵢⱼ)^{j∈J} → bbᵢ)^{i∈I}
+Given that the decomposition matrix is computed from source terms, we
+need to prove that it respects:
+| ∀(vⱼ)^{j∈J}, mₛ(vⱼ)ʲ = 〚mₛi 〛(vⱼ)ʲ
+
+v(Here) = v
+K(vᵢ)ⁱ(k.a) = vₖ(a) if k ∈ [0;n[
+
+We also said that
+(Leaf bb)(v) := Match bb
+(Node(a, (kᵢ → cᵢ)ⁱ, c_{fallback}))(v)
+    let v(a) be K(vⱼ)ʲ
+        if k ∈ {Kᵢ}ⁱ then  C_{min{i}|k=kᵢ}(v)
+        else c_{fallback}(v)