From 1e23f71f8c475797d34cf26faec27d5a4e67c095 Mon Sep 17 00:00:00 2001 From: Francesco Mecca Date: Sun, 29 Mar 2020 21:24:56 +0200 Subject: [PATCH] altro --- tesi/tesi_unicode.org | 42 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/tesi/tesi_unicode.org b/tesi/tesi_unicode.org index 2528b3c..9f9b7ec 100644 --- a/tesi/tesi_unicode.org +++ b/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)