From 0ba93f90461f959487330c0b1c2f940b1d866bd9 Mon Sep 17 00:00:00 2001 From: Francesco Mecca Date: Tue, 30 Jun 2020 21:39:38 +0200 Subject: [PATCH] c to D --- tesi/tesi_unicode.org | 23 +++++++++++------------ todo.org | 24 ++++++++++++------------ 2 files changed, 23 insertions(+), 24 deletions(-) diff --git a/tesi/tesi_unicode.org b/tesi/tesi_unicode.org index 1e8ca0d..8e4fd59 100644 --- a/tesi/tesi_unicode.org +++ b/tesi/tesi_unicode.org @@ -271,7 +271,7 @@ environment $\sigma$ mapping variables to accessors.\\ $\Failure$ expresses a match failure that occurs when no clause matches the input value. \\ -$\Switch a {\Fam {i \in I} {\pi_i, D_i}} \Dfb$ has one subtree $D_i$ +$\Switch a {\Fam {i \in I} {\pi_i, D_i}} D_{fallback}$ has one subtree $D_i$ for every head constructor that appears in the pattern matching clauses, and a fallback case that is used when at least one variant of the constructor doesn't appear in the clauses. The presence of the @@ -362,9 +362,9 @@ If we have two terminals, such as leaves in the first example, we check that the two right-hand-sides are equivalent. If we have a node $N$ and another tree $T$ we check equivalence for each child of $N$, which is a pair of a branch condition $\pi_i$ and a -subtree $C_i$. For every child $(\pi_i, C_i)$ we reduce $T$ by killing all +subtree $D_i$. For every child $(\pi_i, D_i)$ we reduce $T$ by killing all the branches that are incompatible with $\pi_i$ and check that the -reduced tree is equivalent to $C_i$. +reduced tree is equivalent to $D_i$. \\ \subsection{From source programs to decision trees} Our source language supports integers, lists, tuples and all algebraic @@ -436,13 +436,13 @@ possible values \emph{S} and a pair of source and target decision trees and in case the two trees are not equivalent it returns a counter example. Our algorithm respects the following correctness statement: \begin{align*} - \EquivTEX S {C_S} {C_T} = \YesTEX \;\land\; \coversTEX {C_T} S + \EquivTEX S {D_S} {D_T} = \YesTEX \;\land\; \coversTEX {D_T} S & \implies - \forall v_S \approx v_T \in S,\; C_S(v_S) = C_T(v_T) + \forall v_S \approx v_T \in S,\; D_S(v_S) = D_T(v_T) \\ - \EquivTEX S {C_S} {C_T} = \NoTEX {v_S} {v_T} \;\land\; \coversTEX {C_T} S + \EquivTEX S {D_S} {D_T} = \NoTEX {v_S} {v_T} \;\land\; \coversTEX {D_T} S & \implies - v_S \approx v_T \in S \;\land\; C_S(v_S) \neq C_T(v_T) + v_S \approx v_T \in S \;\land\; D_S(v_S) \neq D_T(v_T) \end{align*} * Background ** OCaml @@ -1439,7 +1439,7 @@ target programs. \text{\emph{decision trees}} & D(\pi, e) & \bnfeq & \Leaf {\cle(a)} \\ & & \bnfor & \Failure \\ - & & \bnfor & \Switch a {\Fam {i \in I} {\pi_i, D_i}} \Dfb \\ + & & \bnfor & \Switch a {\Fam {i \in I} {\pi_i, D_i}} D_{fallback} \\ & & \bnfor & \Guard {\cle(a)} {D_0} {D_1} \\ & & \bnfor & Unreachable \\ \text{\emph{accessors}} & a @@ -1854,7 +1854,7 @@ counter-example.) \begin{array}{l@{~}r@{~}l} & & \text{\emph{boolean result}} \\ - b & \in & \{ 0, 1 \} \\ + b & \in & \{ No, Yes \} \\ \end{array} \begin{array}{l@{~}r@{~}l} @@ -1908,7 +1908,7 @@ hand side. \\ \forall i,\; \Equivrel {(S \cap a \in \pi_i)} {D_S} {D_i} G \\ - \Equivrel {(S \cap a \notin \Fam i {\pi_i})} {D_S} \Dfb G} + \Equivrel {(S \cap a \notin \Fam i {\pi_i})} {D_S} {D_{fallback}} G} {\Equivrel S {D_S} {\Switch a {\Fam i {\pi_i} {D_i}} \Dfb} G} \end{mathpar} @@ -2005,7 +2005,6 @@ Corollary: For a full input space /S/, that is the universe of the target program: | $equiv(S, \llbracket t_S \rrbracket{_S}, \llbracket t_T \rrbracket{_T}, \emptyset) = Yes \Leftrightarrow \progrel {t_S} {t_T}$ - \begin{comment} TODO: put ^i∈I where needed \end{comment} @@ -2047,7 +2046,7 @@ 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→π)) + ∀a,π covers(Dₜ,S) → covers(D_{t/a→π}, (S∩a→π)) Uᵢπⁱ ≈ Uᵢπ'∩(a→π) ≈ (Uᵢπ')∩(a→π) %% diff --git a/todo.org b/todo.org index c6a6ba1..10293b4 100644 --- a/todo.org +++ b/todo.org @@ -27,7 +27,7 @@ - [ ] chiedi a Galla`, Marco e Naz quali sono tutti gli es - [ ] linear models.zip? -* Tesi [9/33] +* Tesi [18/33] - [X] Rivedere inference rules di Gabriel e aggiustarle con le mie - [ ] Definisci domain sempre allo stesso modo, con bigcup o | - [ ] Scegli se usare [[t_s]\] o D(ts) @@ -42,7 +42,7 @@ - [ ] Equivalenza R_s R_T (run) - [ ] TODO t_t - [ ] Introduzione: Explain covers alla fine (o vedi che si fa nel paper) -- [ ] Paginazione: +- [-] Paginazione: + [ ] figura (function scrutinee) fuori pagina + [ ] figura primo decision tree: migliorala + [ ] Line breaks @@ -50,7 +50,7 @@ + [ ] correct. stat. di eq. checking: fuori margine + [ ] Minipages: spazio o divisore dalle linee prima e dopo + [ ] Minipages: allinea - + [ ] {\progrel t_S t_T}: t_S finisce fuori + + [X] {\progrel t_S t_T}: t_S finisce fuori - [X] segreteria: tesi inglese - [X] Gatti: inglese - [X] Gatti: Coppo mio relatore @@ -64,21 +64,21 @@ - [X] snellendo un po' la presentazione formale. - [ ] spiegando meglio il ruolo della symbolic interpretation - [X] Perche' ci si concentra sulla traduzione dei pattern? -- [ ] riferimenti bibliografici -- [ ] paper pattern matching C++ -- [ ] Gabriel: finisci -- [ ] SimpleEquiv Latex -- [ ] Boolean result o Yes|No? (Inference rules) +- [X] riferimenti bibliografici +- [X] paper pattern matching C++ +- [X] Gabriel: finisci +- [X] SimpleEquiv Latex +- [X] Boolean result o Yes|No? (Inference rules) - [ ] Mostra altri casi per la empty rule -- [ ] Adatta i cambiamenti al paper +- [X] Adatta i cambiamenti al paper - [ ] Esempio trimming - [ ] Trimming e resto: mi sa che usi left e right male - [ ] Spiega perche` trimming non simmetrico -- [ ] Spiega meglio le guards on equivalence checking -- [ ] t_T e t_S o t_t e t_s??? +- [X] Spiega meglio le guards on equivalence checking +- [X] t_T e t_S o t_t e t_s??? - [X] TODO eq_muovi : si parla di eq checking, forse non li` - [X] Gabriel: quello che penso sulle equivalenze omesse e` giusto? -- [ ] Cambia le C di constraint tree in D +- [X] Cambia le C di constraint tree in D - [ ] TODO on the org file HALP HALP!