diff --git a/tesi/gabriel/part4.org b/tesi/gabriel/part4.org new file mode 100644 index 0000000..5cb1a98 --- /dev/null +++ b/tesi/gabriel/part4.org @@ -0,0 +1,354 @@ +# Add headers to export only this section +* 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 ∈ ℕ + +\begin{comment} +Are K and Here clear here? +\end{comment} + +We define the decomposition matrix /mₛ/ as +| SMatrix mₛ := (aⱼ)^{j∈J}, ((p_{ij})^{j∈J} → bbᵢ)^{i∈I} +\begin{comment} +Correggi prendendo in considerazione l'accessor +\end{comment} + +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[ +\begin{comment} +TODO: EXPLAIN +\end{comment} + +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 + 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 + +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 +\] +\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" m_{wild} +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ᵢ = a_{0.l}ˡ +++ a_{i∈I\backslash \{0\}} because v(a₀) = K(v(a){0.l})ˡ) + + + + +** Proof of equivalence checking +\begin{comment} +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ₜ) +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ₜ = 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, (π'ᵢ→C_{i/a→π})ⁱ) + +\begin{comment} +Actually in the proof.org file I transcribed: + e. Unreachabe → ⊥ +This is not correct because you don't have Unreachable nodes in target decision trees +\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 +C_{trim} that is the result of the trimming operation on Cₜ +| Cₜ(vₜ) = C_{trim}(vₜ) = Node(b, (πᵢ'→C_{i/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 +| C_{k/a→π}(vₜ) = Node(b, (πᵢ'→C_{i/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ₜ) = C_{k/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} + +\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ₜ) + +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\vert int(k) = n} x {n\vert 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} +0. in case of unreachable: +| Cₛ(vₛ) = Absurd(Unreachable) ≠ Cₜ(vₜ) ∀vₛ,vₜ +1. 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. +2. 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. +3. 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 +4. 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ₛᵢ)ⁱ, C_{sf}), Cₜ) := + | Forall(equiv( S∩(a→π(kᵢ)ⁱ), Cₛᵢ, C_{t/a→π(kᵢ)})ⁱ +++ equiv(S∩(a→π(kᵢ)), 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 + The constructor k is either included in the set of constructors kᵢ: + | k \vert k∈(kᵢ)ⁱ ∧ Cₛ(vₛ) = Cₛᵢ(vₛ) + We also know that + | (1) Cₛᵢ(vₛ) = C_{t/a→πᵢ}(vₜ) + | (2) C_{T/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ₛ) = C_{T/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ₛₖ, C_{T/a→πₖ} = No(vₛ, vₜ) + Then we can say that + | Cₛₖ(vₛ) ≠ C_{t/a→πₖ}(vₜ) + that is enough for proving that + | Cₛₖ(vₛ) ≠ (C_{t/a→πₖ}(vₜ) = Cₜ(vₜ)) diff --git a/tesi/gabriel/part4.pdf b/tesi/gabriel/part4.pdf new file mode 100644 index 0000000..3c85d5a Binary files /dev/null and b/tesi/gabriel/part4.pdf differ diff --git a/tesi/gabriel/part4.tex b/tesi/gabriel/part4.tex new file mode 100644 index 0000000..1e8c80d --- /dev/null +++ b/tesi/gabriel/part4.tex @@ -0,0 +1,659 @@ +% Created 2020-04-09 Thu 01:36 +% Intended LaTeX compiler: pdflatex +\documentclass[11pt]{article} +\usepackage[utf8]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{graphicx} +\usepackage{grffile} +\usepackage{longtable} +\usepackage{wrapfig} +\usepackage{rotating} +\usepackage[normalem]{ulem} +\usepackage{amsmath} +\usepackage{textcomp} +\usepackage{amssymb} +\usepackage{capt-of} +\usepackage{hyperref} +\linespread{1.25} +\usepackage{algorithm} +\usepackage{comment} +\usepackage{algpseudocode} +\usepackage{amsmath,amssymb,amsthm} +\newtheorem{definition}{Definition} +\usepackage{mathpartir} +\usepackage{graphicx} +\usepackage{listings} +\usepackage{color} +\usepackage{stmaryrd} +\newcommand{\semTEX}[1]{{\llbracket{#1}\rrbracket}} +\newcommand{\EquivTEX}[3]{\mathsf{equiv}(#1, #2, #3)} % \equiv is already taken +\newcommand{\coversTEX}[2]{#1 \mathrel{\mathsf{covers}} #2} +\newcommand{\YesTEX}{\mathsf{Yes}} +\newcommand{\NoTEX}[2]{\mathsf{No}(#1, #2)} +\usepackage{comment} +\usepackage{mathpartir} +\usepackage{stmaryrd} % llbracket, rrbracket +\usepackage{listings} +\usepackage{notations} +\lstset{ +mathescape=true, +language=[Objective]{Caml}, +basicstyle=\ttfamily, +extendedchars=true, +showstringspaces=false, +aboveskip=\smallskipamount, +% belowskip=\smallskipamount, +columns=fullflexible, +moredelim=**[is][\color{blue}]{/*}{*/}, +moredelim=**[is][\color{green!60!black}]{/!}{!/}, +moredelim=**[is][\color{orange}]{/(}{)/}, +moredelim=[is][\color{red}]{/[}{]/}, +xleftmargin=1em, +} +\lstset{aboveskip=0.4ex,belowskip=0.4ex} +\author{Francesco Mecca} +\date{} +\hypersetup{ + pdfkeywords={}, + pdfsubject={}, + pdfcreator={Emacs 26.3 (Org mode 9.1.9)}, + pdflang={English}} +\begin{document} + +\maketitle +\begin{comment} +TODO: neg is parsed incorrectly +TODO: chiedi a Gabriel se T e S vanno bene, ma prima controlla che siano coerenti +\section{{\bfseries\sffamily TODO} Scaletta [1/6]} +\label{sec:org530707f} +\begin{itemize} +\item[{$\boxtimes$}] Introduction +\item[{$\boxminus$}] Background [80\%] +\begin{itemize} +\item[{$\boxtimes$}] Low level representation +\item[{$\boxtimes$}] Lambda code [0\%] +\item[{$\boxtimes$}] Pattern matching +\item[{$\boxtimes$}] Symbolic execution +\item[{$\square$}] Translation Validation +\end{itemize} +\item[{$\square$}] Translation validation of the Pattern Matching Compiler +\begin{itemize} +\item[{$\square$}] Source translation +\begin{itemize} +\item[{$\square$}] Formal Grammar +\item[{$\square$}] Compilation of source patterns +\item[{$\square$}] Rest? +\end{itemize} +\item[{$\square$}] Target translation +\begin{itemize} +\item[{$\square$}] Formal Grammar +\item[{$\square$}] Symbolic execution of the Lambda target +\end{itemize} +\item[{$\square$}] Equivalence between source and target +\end{itemize} +\item[{$\square$}] Proof of correctness +\item[{$\square$}] Practical results +\end{itemize} + +Magari prima pattern matching poi compilatore? + +\end{comment} +\section{Correctness of the algorithm} +\label{sec:org4188d38} +Running a program t$_S$ or its translation $\llbracket$t$_S$$\rrbracket$ against an input v$_S$ +produces as a result \emph{r} in the following way: +\begin{center} +\begin{tabular}{l} +( $\llbracket$t$_S$$\rrbracket$$_S$(v$_S$) = C$_S$(v$_S$) ) $\to$ r\\ +t$_S$(v$_S$) $\to$ r\\ +\end{tabular} +\end{center} +Likewise +\begin{center} +\begin{tabular}{l} +( $\llbracket$t$_T$$\rrbracket$$_T$(v$_T$) = C$_T$(v$_T$) ) $\to$ r\\ +t$_T$(v$_T$) $\to$ r\\ +\end{tabular} +\end{center} +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$_S$ $\simeq$ v$_T$ (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 +\begin{center} +\begin{tabular}{l} +t$_S$ $\simeq$ t$_T$ := $\forall$v$_S$$\simeq$v$_T$, t$_S$(v$_S$) = t$_T$(v$_T$)\\ +C$_S$ $\simeq$ C$_T$ := $\forall$v$_S$$\simeq$v$_T$, C$_S$(v$_S$) = C$_T$(v$_T$)\\ +\end{tabular} +\end{center} + +The proposed equivalence algorithm that works on a couple of +decision trees is returns either \emph{Yes} or \emph{No(v$_S$, v$_T$)} where v$_S$ and +v$_T$ are a couple of possible counter examples for which the constraint +trees produce a different result. + +\subsection{Statements} +\label{sec:orgccf94c1} +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 + +\begin{center} +\begin{tabular}{l} +$\forall$v$_S$, t$_S$(v$_S$) = $\llbracket$t$_S$$\rrbracket$$_S$(v$_S$)\\ +\end{tabular} +\end{center} + + +Likewise, for the target language: + +\begin{center} +\begin{tabular}{l} +$\forall$v$_T$, t$_T$(v$_T$) = $\llbracket$t$_T$$\rrbracket$$_T$(v$_T$)\\ +\end{tabular} +\end{center} + +Definition: in the presence of guards we can say that two results are +equivalent modulo the guards queue, written \emph{r$_1$ $\simeq$gs r$_2$}, when: +\begin{center} +\begin{tabular}{l} +(gs$_1$, r$_1$) $\simeq$gs (gs$_2$, r$_2$) $\Leftrightarrow$ (gs$_1$, r$_1$) = (gs$_2$ ++ gs, r$_2$)\\ +\end{tabular} +\end{center} + +Definition: we say that C$_T$ covers the input space \emph{S}, written +/covers(C$_T$, S) when every value v$_S$$\in $S is a valid input to the +decision tree C$_T$. (TODO: rephrase) + +Theorem: Given an input space \emph{S} and a couple of decision trees, where +the target decision tree C$_T$ covers the input space \emph{S}, we say that +the two decision trees are equivalent when: + +\begin{center} +\begin{tabular}{l} +equiv(S, C$_S$, C$_T$, gs) = Yes $\wedge$ covers(C$_T$, S) $\to$ $\forall$v$_S$$\simeq$v$_T$ $\in $ S, C$_S$(v$_S$) $\simeq$gs C$_T$(v$_T$)\\ +\end{tabular} +\end{center} + +Similarly we say that a couple of decision trees in the presence of +an input space \emph{S} are \emph{not} equivalent when: + +\begin{center} +\begin{tabular}{l} +equiv(S, C$_S$, C$_T$, gs) = No(v$_S$,v$_T$) $\wedge$ covers(C$_T$, S) $\to$ v$_S$$\simeq$v$_T$ $\in $ S $\wedge$ C$_S$(v$_S$) $\ne$gs C$_T$(v$_T$)\\ +\end{tabular} +\end{center} + +Corollary: For a full input space \emph{S}, that is the universe of the +target program we say: + +\begin{center} +\begin{tabular}{l} +equiv(S, $\llbracket$t$_S$$\rrbracket$$_S$, $\llbracket$t$_T$$\rrbracket$$_T$, $\varnothing$) = Yes $\Leftrightarrow$ t$_S$ $\simeq$ t$_T$\\ +\end{tabular} +\end{center} + + +\begin{enumerate} +\item Proof of the correctness of the translation from source programs to source decision trees +\label{sec:orgfa2a152} + +We define a source term t$_S$ as a collection of patterns pointing to blackboxes +\begin{center} +\begin{tabular}{l} +t$_S$ ::= (p $\to$ bb)\(^{\text{i$\in $I}}\)\\ +\end{tabular} +\end{center} + +A pattern is defined as either a constructor pattern, an or pattern or +a constant pattern +\begin{center} +\begin{tabular}{lllll} +p ::= & K(p$_i$)$^i$, i $\in $ I & (p & q) & n $\in $ $\mathbb{N}$\\ +\end{tabular} +\end{center} + +A decision tree is defined as either a Leaf, a Failure terminal or +an intermediate node with different children sharing the same accessor \emph{a} +and an optional fallback. +Failure is emitted only when the patterns don't cover the whole set of +possible input values \emph{S}. The fallback is not needed when the user +doesn't use a wildcard pattern. +\%\%\% Give example of thing + +\begin{center} +\begin{tabular}{ll} +C$_S$ ::= Leaf bb & Node(a, (K$_i$ $\to$ C$_i$)\(^{\text{i$\in $S}}\) , C?)\\ +a ::= Here & n.a\\ +v$_S$ ::= K(v$_i$)\(^{\text{i$\in $I}}\) & n $\in $ $\mathbb{N}$\\ +\end{tabular} +\end{center} + +\begin{comment} +Are K and Here clear here? +\end{comment} + +We define the decomposition matrix \emph{m$_S$} as +\begin{center} +\begin{tabular}{l} +SMatrix m$_S$ := (a$_j$)\(^{\text{j$\in $J}}\), ((p\(_{\text{ij}}\))\(^{\text{j$\in $J}}\) $\to$ bb$_i$)\(^{\text{i$\in $I}}\)\\ +\end{tabular} +\end{center} +\begin{comment} +Correggi prendendo in considerazione l'accessor +\end{comment} + +We define the decision tree of source programs +$\llbracket$t$_S$$\rrbracket$ +in terms of the decision tree of pattern matrices +$\llbracket$m$_S$$\rrbracket$ +by the following: +$\llbracket$((p$_i$ $\to$ bb$_i$)\(^{\text{i$\in $I}}\)$\rrbracket$ := $\llbracket$(Root), (p$_i$ $\to$ bb$_i$)\(^{\text{i$\in $I}}\) $\rrbracket$ + +decision tree computed from pattern matrices respect the following invariant: +\begin{center} +\begin{tabular}{l} +$\forall$v (v$_i$)\(^{\text{i$\in $I}}\) = v(a$_i$)\(^{\text{i$\in $I}}\) $\to$ $\llbracket$m$\rrbracket$(v) = m(v$_i$)\(^{\text{i$\in $I}}\) for m = ((a$_i$)\(^{\text{i$\in $I}}\), (r$_i$)\(^{\text{i$\in $I}}\))\\ +\end{tabular} +\end{center} +where +\begin{center} +\begin{tabular}{l} +v(Here) = v\\ +K(v$_i$)$^i$(k.a) = v$_k$(a) if k $\in $ [0;n[\\ +\end{tabular} +\end{center} +\begin{comment} +TODO: EXPLAIN +\end{comment} + +We proceed to show the correctness of the invariant by a case +analysys. + +Base cases: +\begin{enumerate} +\item\relax [| $\varnothing$, ($\varnothing$ $\to$ bb$_i$)$^i$ |] := Leaf bb$_i$ where i := min(I), that is a +decision tree [|ms|] defined by an empty accessor and empty +patterns pointing to blackboxes \emph{bb$_i$}. 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 +\item\relax [| (a$_j$)$^j$, $\varnothing$ |] := Failure +\end{enumerate} + +Regarding non base cases: +Let's first define +\begin{center} +\begin{tabular}{l} +let Idx(k) := [0; arity(k)[\\ +let First($\varnothing$) := $\bot$\\ +let First((a$_j$)$^j$) := a\(_{\text{min(j$\in $J$\ne$$\varnothing$)}}\)\\ +\end{tabular} +\end{center} +\[ +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)^{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_j 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" m\(_{\text{wild}}\) +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_k for some k then + m(v_i)^i = m_k((v'_l)^l +++ (v_i)^{i\in I\backslash \{0\}}) + else + m(v_i)^i = m_{wild}(v_i)^{i\in I\backslash \{0\}} +\] + +\item Proof: +\label{sec:org8dad6fc} +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: +\begin{itemize} +\item either k is one of the k$_k$ for some k +\item or k is none of the (k$_k$)$^k$ +\end{itemize} + +Both m(v$_i$)$^i$ and m$_k$(v$_k$)$^k$ are defined as the first matching result of +a family over each row r$_j$ of a matrix + +We know, from the definition of +Groups(m), that m$_k$ is +\[ + ((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)^l +++ (p_{ij})^{i\in I\backslash \{0\}} \to e_j + if p_{0j} is _ then + (_)^l +++ (p_{ij})^{i\in I\backslash \{0\}} \to e_j + else \bot + )^j +\] + +By definition, m(v$_i$)$^i$ is +m(v$_i$)$^i$ = First(r$_j$(v$_i$)$^i$)$^j$ for m = ((a$_i$)$^i$, (r$_j$)$^j$) +(p$_i$)$^i$ (v$_i$)$^i$ = \{ + if p$_0$ = k(q$_l$)$^l$, v$_0$ = k'(v'$_k$)$^k$, k=Idx(k') and l=Idx(k) + if k $\ne$ k' then $\bot$ + if k = k' then ((q$_l$)$^l$ \sout{+} (p$_i$)\(^{\text{i$\in $I}\backslash\ \text{$\backslash${0$\backslash$}}}\)) ((v'$_k$)$^k$ \sout{+} (v$_i$)\(^{\text{i$\in $I}\backslash\ \text{$\backslash${0$\backslash$}}}\)) + if p$_0$ = (q$_1$|q$_2$) then + First( (q$_1$p$_i$\(^{\text{i$\in $I }\backslash\ \text{$\backslash${0$\backslash$}}}\)) v$_i$\(^{\text{i$\in $I }\backslash\ \text{$\backslash${0$\backslash$}}}\), (q$_2$p$_i$\(^{\text{i$\in $I }\backslash\ \text{$\backslash${0$\backslash$}}}\)) v$_i$\(^{\text{i$\in $I }\backslash\ \text{$\backslash${0$\backslash$}}}\) ) +\} + +For this reason, if we can prove that +\begin{center} +\begin{tabular}{l} +$\forall$j, r$_j$(v$_i$)$^i$ = r'$_j$((v'$_k$)$^k$ ++ (v$_i$)$^i$)\\ +\end{tabular} +\end{center} +it follows that +\begin{center} +\begin{tabular}{l} +m(v$_i$)$^i$ = m$_k$((v'$_k$)$^k$ ++ (v$_i$)$^i$)\\ +\end{tabular} +\end{center} +from the above definition. + +We can also show that a$_i$ = a\(_{\text{0.l}}\)$^l$ \sout{+} a\(_{\text{i$\in $I}\backslash\ \text{$\backslash${0$\backslash$}}}\) because v(a$_0$) = K(v(a)\{0.l\})$^l$) +\end{enumerate} + + + + +\subsection{Proof of equivalence checking} +\label{sec:orgffce3ea} +\begin{comment} +TODO: put ^i$\in $I where needed +\end{comment} +\subsubsection{The trimming lemma} +The trimming lemma allows to reduce the size of a decision tree given +an accessor $\to$ $\pi$ relation (TODO: expand) +\begin{center} +\begin{tabular}{l} +$\forall$v$_T$ $\in $ (a$\to$$\pi$), C$_T$(v$_T$) = C\(_{\text{t/a$\to$$\pi$(k$_i$)}}\)(v$_T$)\\ +\end{tabular} +\end{center} +We prove this by induction on C$_T$: + a. C$_T$ = Leaf\(_{\text{bb}}\): when the decision tree is a leaf terminal, we + know that +\begin{center} +\begin{tabular}{l} +Leaf\(_{\text{bb/a$\to$$\pi$}}\)(v) = Leaf\(_{\text{bb}}\)(v)\\ +\end{tabular} +\end{center} +That means that the result of trimming on a Leaf is the Leaf itself +b. The same applies to Failure terminal +\begin{center} +\begin{tabular}{l} +Failure\(_{\text{/a$\to$$\pi$}}\)(v) = Failure(v)\\ +\end{tabular} +\end{center} +c. When C$_T$ = Node(b, ($\pi$$\to$C$_i$)$^i$)\(_{\text{/a$\to$$\pi$}}\) then +we look at the accessor \emph{a} of the subtree C$_i$ and +we define $\pi$$_i$' = $\pi$$_i$ if a$\ne$b else $\pi$$_i$$\cap$$\pi$ +Trimming a switch node yields the following result: +\begin{center} +\begin{tabular}{l} +Node(b, ($\pi$$\to$C$_i$)$^i$)\(_{\text{/a$\to$$\pi$}}\) := Node(b, ($\pi$'$_i$$\to$C\(_{\text{i/a$\to$$\pi$}}\))$^i$)\\ +\end{tabular} +\end{center} + +\begin{comment} +Actually in the proof.org file I transcribed: + e. Unreachabe $\to$ $\bot$ +This is not correct because you don't have Unreachable nodes in target decision trees +\end{comment} + +For the trimming lemma we have to prove that running the value v$_T$ against +the decistion tree C$_T$ is the same as running v$_T$ against the tree +C\(_{\text{trim}}\) that is the result of the trimming operation on C$_T$ +\begin{center} +\begin{tabular}{l} +C$_T$(v$_T$) = C\(_{\text{trim}}\)(v$_T$) = Node(b, ($\pi$$_i$'$\to$C\(_{\text{i/a$\to$$\pi$}}\))$^i$)(v$_T$)\\ +\end{tabular} +\end{center} +We can reason by first noting that when v$_T$$\notin$(b$\to$$\pi$$_i$)$^i$ the node must be a Failure node. +In the case where $\exists$k| v$_T$$\in $(b$\to$$\pi$$_k$) then we can prove that +\begin{center} +\begin{tabular}{l} +C\(_{\text{k/a$\to$$\pi$}}\)(v$_T$) = Node(b, ($\pi$$_i$'$\to$C\(_{\text{i/a$\to$$\pi$}}\))$^i$)(v$_T$)\\ +\end{tabular} +\end{center} +because when a $\ne$ b then $\pi$$_k$'= $\pi$$_k$ and this means that v$_T$$\in $$\pi$$_k$' +while when a = b then $\pi$$_k$'=($\pi$$_k$$\cap$$\pi$) and vt$\in $$\pi$$_k$' because: +\begin{itemize} +\item by the hypothesis, v$_T$$\in $$\pi$ +\item we are in the case where v$_T$$\in $$\pi$$_k$ +\end{itemize} +So v$_T$ $\in $ $\pi$$_k$' and by induction +\begin{center} +\begin{tabular}{l} +C$_k$(v$_T$) = C\(_{\text{k/a$\to$$\pi$}}\)(v$_T$)\\ +\end{tabular} +\end{center} +We also know that $\forall$v$_T$$\in $(b$\to$$\pi$$_k$) $\to$ C$_T$(v$_T$) = C$_k$(v$_T$) +By putting together the last two steps, we have proven the trimming +lemma. + +\begin{comment} +TODO: what should I say about covering??? I swap $\pi$ and $\pi$' +Covering lemma: + $\forall$a,$\pi$ covers(C$_T$,S) $\to$ covers(C_{t/a$\to$$\pi$}, (S$\cap$a$\to$$\pi$)) + U$_i$$\pi$$^i$ $\approx$ U$_i$$\pi$'$\cap$(a$\to$$\pi$) $\approx$ (U$_i$$\pi$')$\cap$(a$\to$$\pi$) %% + + +%%%%%%% Also: Should I swap $\pi$ and $\pi$' ? +\end{comment} + +\subsubsection{Equivalence checking} +The equivalence checking algorithm takes as parameters an input space +\emph{S}, a source decision tree \emph{C$_S$} and a target decision tree \emph{C$_T$}: +\begin{center} +\begin{tabular}{ll} +equiv(S, C$_S$, C$_T$) $\to$ Yes & No(v$_S$, v$_T$)\\ +\end{tabular} +\end{center} + +When the algorithm returns Yes and the input space is covered by \emph{C$_S$} +we can say that the couple of decision trees are the same for +every couple of source value \emph{v$_S$} and target value \emph{v$_T$} that are equivalent. +\begin{comment} +Define "covered" +Is it correct to say the same? How to correctly distinguish in words $\simeq$ and = ? +\end{comment} +\begin{center} +\begin{tabular}{l} +equiv(S, C$_S$, C$_T$) = Yes and cover(C$_T$, S) $\to$ $\forall$ v$_S$ $\simeq$ v$_T$$\in $S $\wedge$ C$_S$(v$_S$) = C$_T$(v$_T$)\\ +\end{tabular} +\end{center} +In the case where the algorithm returns No we have at least a couple +of counter example values v$_S$ and v$_T$ for which the two decision trees +outputs a different result. +\begin{center} +\begin{tabular}{l} +equiv(S, C$_S$, C$_T$) = No(v$_S$,v$_T$) and cover(C$_T$, S) $\to$ $\forall$ v$_S$ $\simeq$ v$_T$$\in $S $\wedge$ C$_S$(v$_S$) $\ne$ C$_T$(v$_T$)\\ +\end{tabular} +\end{center} + +We define the following +\begin{center} +\begin{tabular}{l} +Forall(Yes) = Yes\\ +Forall(Yes::l) = Forall(l)\\ +Forall(No(v$_S$,v$_T$)::\_) = No(v$_S$,v$_T$)\\ +\end{tabular} +\end{center} +There exists and are injective: +\begin{center} +\begin{tabular}{l} +int(k) $\in $ $\mathbb{N}$ (arity(k) = 0)\\ +tag(k) $\in $ $\mathbb{N}$ (arity(k) > 0)\\ +$\pi$(k) = \{n\(\vert{}\) int(k) = n\} x \{n\(\vert{}\) tag(k) = n\}\\ +\end{tabular} +\end{center} +where k is a constructor. + +\begin{comment} +TODO: explain: +$\forall$v$\in $a$\to$$\pi$, C_{/a$\to$$\pi$}(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} +\begin{enumerate} +\item in case of unreachable: +\end{enumerate} +\begin{center} +\begin{tabular}{l} +C$_S$(v$_S$) = Absurd(Unreachable) $\ne$ C$_T$(v$_T$) $\forall$v$_S$,v$_T$\\ +\end{tabular} +\end{center} +\begin{enumerate} +\item In the case of an empty input space +\begin{center} +\begin{tabular}{l} +equiv($\varnothing$, C$_S$, C$_T$) := Yes\\ +\end{tabular} +\end{center} +and that is trivial to prove because there is no pair of values (v$_S$, v$_T$) that could be +tested against the decision trees. +In the other subcases S is always non-empty. +\item When there are \emph{Failure} nodes at both sides the result is \emph{Yes}: +\begin{center} +\begin{tabular}{l} +equiv(S, Failure, Failure) := Yes\\ +\end{tabular} +\end{center} +Given that $\forall$v, Failure(v) = Failure, the statement holds. +\item When we have a Leaf or a Failure at the left side: +\begin{center} +\begin{tabular}{l} +equiv(S, Failure as C$_S$, Node(a, ($\pi$$_i$ $\to$ C$_T$$_i$)$^i$)) := Forall(equiv( S$\cap$a$\to$$\pi$(k$_i$)), C$_S$, C$_T$$_i$)$^i$)\\ +equiv(S, Leaf bb$_S$ as C$_S$, Node(a, ($\pi$$_i$ $\to$ C$_T$$_i$)$^i$)) := Forall(equiv( S$\cap$a$\to$$\pi$(k$_i$)), C$_S$, C$_T$$_i$)$^i$)\\ +\end{tabular} +\end{center} +The algorithm either returns Yes for every sub-input space S$_i$ := S$\cap$(a$\to$$\pi$(k$_i$)) and +subtree C$_T$$_i$ +\begin{center} +\begin{tabular}{l} +equiv(S$_i$, C$_S$, C$_T$$_i$) = Yes $\forall$i\\ +\end{tabular} +\end{center} +or we have a counter example v$_S$, v$_T$ for which +\begin{center} +\begin{tabular}{l} +v$_S$$\simeq$v$_T$$\in $S$_k$ $\wedge$ c$_S$(v$_S$) $\ne$ C$_T$$_k$(v$_T$)\\ +\end{tabular} +\end{center} +then because +\begin{center} +\begin{tabular}{l} +v$_T$$\in $(a$\to$$\pi$$_k$) $\to$ C$_T$(v$_T$) = C$_T$$_k$(v$_T$) ,\\ +v$_S$$\simeq$v$_T$$\in $S $\wedge$ C$_S$(v$_S$)$\ne$C$_T$(v$_T$)\\ +\end{tabular} +\end{center} +we can say that +\begin{center} +\begin{tabular}{l} +equiv(S$_i$, C$_S$, C$_T$$_i$) = No(v$_S$, v$_T$) for some minimal k$\in $I\\ +\end{tabular} +\end{center} +\item When we have a Node on the right we define $\pi$$_n$ as the domain of +values not covered but the union of the constructors k$_i$ +\begin{center} +\begin{tabular}{l} +$\pi$$_n$ = ¬($\bigcup$$\pi$(k$_i$)$^i$)\\ +\end{tabular} +\end{center} +The algorithm proceeds by trimming +\begin{center} +\begin{tabular}{l} +equiv(S, Node(a, (k$_i$ $\to$ C$_S$$_i$)$^i$, C\(_{\text{sf}}\)), C$_T$) :=\\ +Forall(equiv( S$\cap$(a$\to$$\pi$(k$_i$)$^i$), C$_S$$_i$, C\(_{\text{t/a$\to$$\pi$(k$_i$)}}\))$^i$ \sout{+} equiv(S$\cap$(a$\to$$\pi$(k$_i$)), C$_S$, C\(_{\text{a$\to$$\pi$$_n$}}\)))\\ +\end{tabular} +\end{center} + The statement still holds and we show this by first analyzing the +\emph{Yes} case: +\begin{center} +\begin{tabular}{l} +Forall(equiv( S$\cap$(a$\to$$\pi$(k$_i$)$^i$), C$_S$$_i$, C\(_{\text{t/a$\to$$\pi$(k$_i$)}}\))$^i$ = Yes\\ +\end{tabular} +\end{center} +The constructor k is either included in the set of constructors k$_i$: +\begin{center} +\begin{tabular}{l} +k \(\vert{}\) k$\in $(k$_i$)$^i$ $\wedge$ C$_S$(v$_S$) = C$_S$$_i$(v$_S$)\\ +\end{tabular} +\end{center} +We also know that +\begin{center} +\begin{tabular}{l} +(1) C$_S$$_i$(v$_S$) = C\(_{\text{t/a$\to$$\pi$$_i$}}\)(v$_T$)\\ +(2) C\(_{\text{T/a$\to$$\pi$$_i$}}\)(v$_T$) = C$_T$(v$_T$)\\ +\end{tabular} +\end{center} +(1) is true by induction and (2) is a consequence of the trimming lemma. +Putting everything together: +\begin{center} +\begin{tabular}{l} +C$_S$(v$_S$) = C$_S$$_i$(v$_S$) = C\(_{\text{T/a$\to$$\pi$$_i$}}\)(v$_T$) = C$_T$(v$_T$)\\ +\end{tabular} +\end{center} + +When the k$\notin$(k$_i$)$^i$ [TODO] + +The auxiliary Forall function returns \emph{No(v$_S$, v$_T$)} when, for a minimum k, +\begin{center} +\begin{tabular}{l} +equiv(S$_k$, C$_S$$_k$, C\(_{\text{T/a$\to$$\pi$$_k$}}\) = No(v$_S$, v$_T$)\\ +\end{tabular} +\end{center} +Then we can say that +\begin{center} +\begin{tabular}{l} +C$_S$$_k$(v$_S$) $\ne$ C\(_{\text{t/a$\to$$\pi$$_k$}}\)(v$_T$)\\ +\end{tabular} +\end{center} +that is enough for proving that +\begin{center} +\begin{tabular}{l} +C$_S$$_k$(v$_S$) $\ne$ (C\(_{\text{t/a$\to$$\pi$$_k$}}\)(v$_T$) = C$_T$(v$_T$))\\ +\end{tabular} +\end{center} +\end{enumerate} +\end{document} diff --git a/tesi/tesi.pdf b/tesi/tesi.pdf index 6644301..51f413b 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 c4409c2..5ddbbbc 100644 --- a/tesi/tesi_unicode.org +++ b/tesi/tesi_unicode.org @@ -18,7 +18,6 @@ TODO: chiedi a Gabriel se T e S vanno bene, ma prima controlla che siano coerent - [ ] Formal Grammar - [ ] Symbolic execution of the Lambda target - [ ] Equivalence between source and target - - [ ] Statement of correctness - [ ] Proof of correctness - [ ] Practical results @@ -1362,9 +1361,9 @@ Correggi prendendo in considerazione l'accessor We define the decision tree of source programs 〚tₛ〛 in terms of the decision tree of pattern matrices - 〚mₛ〛 +〚mₛ〛 by the following: - 〚((pᵢ → bbᵢ)^{i∈I}〛 := 〚(Root), (pᵢ → bbᵢ)^{i∈I} 〛 +〚((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}) @@ -1467,13 +1466,13 @@ m(vᵢ)ⁱ = First(rⱼ(vᵢ)ⁱ)ʲ for m = ((aᵢ)ⁱ, (rⱼ)ʲ) 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 prova that +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ᵢ = a){0.l}ˡ +++ a_{i∈I\backslash \{0\}} because v(a₀) = K(v(a){0.l})ˡ) +We can also show that aᵢ = a_{0.l}ˡ +++ a_{i∈I\backslash \{0\}} because v(a₀) = K(v(a){0.l})ˡ) @@ -1484,36 +1483,52 @@ 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 (In other words???) +an accessor → π relation (TODO: expand) | ∀vₜ ∈ (a→π), Cₜ(vₜ) = C_{t/a→π(kᵢ)}(vₜ) - We prove this by induction on Cₜ: - a. Case where Cₜ = Leaf_{bb}: - Leaf_{bb/a→π}(v) = Leaf_{bb}(v) - That means that the result of trimming on a Leaf is - the Leaf itself - b. Same for failure terminal - e. Unreachabe → ⊥ - c. When Cₜ = Node(b, (π→Cᵢ)ⁱ)_{/a→π} then - we define πᵢ' = πᵢ if a≠b else πᵢ∩π ; - Node(b, (π→Cᵢ)ⁱ)_{/a→π} := Node(b, (π'ᵢ→C_{i/a→π})ⁱ) +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ₜ = 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, (π'ᵢ→C_{i/a→π})ⁱ) - Goal: prove that Cₜ(vₜ) = Node(b, (πᵢ'→C_{i/a→π})ⁱ)(vₜ) - Either vₜ∉(b→πᵢ)ⁱ and that means that the node is a Failure node - Or vₜ∈(b→πₖ) for some k, then - C_{k/a→π}(vₜ) = Node(b, (πᵢ'→C_{i/a→π})ⁱ)(vₜ) - because when a ≠ b then πₖ'= πₖ => vₜ∈πₖ' - while when a = b then πₖ'=(πₖ∩π) - - vₜ∈π because of hypothesis - - we already know that vₜ∈πₖ - So vₜ ∈ πₖ' and by induction Cₖ(vₜ) = C_{k/a→π}(vₜ) - and Cₜ(vₜ) = Cₖ(vₜ) when vₜ∈(b→πₖ) - This proves that Node(b, (πᵢ'→C_{i/a→π})ⁱ)(vₜ) = Cₜ(vₜ) - - Covering lemma: - ∀a,π covers(Cₜ,S) => covers(C_{t/a→π}, (S∩a→π)) - Uᵢπⁱ ≈ Uᵢπ'∩(a→π) ≈ (Uᵢπ')∩(a→π) %% \begin{comment} -Should I swap π and π' +Actually in the proof.org file I transcribed: + e. Unreachabe → ⊥ +This is not correct because you don't have Unreachable nodes in target decision trees +\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 +C_{trim} that is the result of the trimming operation on Cₜ +| Cₜ(vₜ) = C_{trim}(vₜ) = Node(b, (πᵢ'→C_{i/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 +| C_{k/a→π}(vₜ) = Node(b, (πᵢ'→C_{i/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ₜ) = C_{k/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} \subsubsection{Equivalence checking}