From 2e830c28729ea35e98e0475daf57d55f36266685 Mon Sep 17 00:00:00 2001 From: Francesco Mecca Date: Fri, 29 May 2020 16:49:45 +0200 Subject: [PATCH] latex on intro --- tesi/tesi_unicode.org | 120 +++++++++++++++++++++++------------------- 1 file changed, 67 insertions(+), 53 deletions(-) diff --git a/tesi/tesi_unicode.org b/tesi/tesi_unicode.org index f8e3633..8529d18 100644 --- a/tesi/tesi_unicode.org +++ b/tesi/tesi_unicode.org @@ -209,6 +209,72 @@ branches are related to the low level representation of values in Lambda code. For example, cons cells \texttt{x::xs} or tuples \texttt{(x,y)} are blocks with tag 0. +We can define this parametrized grammar for decision trees +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. + +The parametrized grammar $D(\pi, e)$ describes the common structure of +source and decision trees. We use $\pi$ for the \emph{conditions} on +each branch, and $a$ for our \emph{accessors}, which give a symbolic +description of a sub-value of the scrutinee. Source conditions $\pi_S$ +are just datatype constructors; target conditions $\pi_T$ are +arbitrary sets of low level OCaml values. +\begin{comment} + possible immediate-integer or block-tag values. +\end{comment} +% +\begin{mathpar} + +\begin{mathpar} + \begin{array}{l@{~}r@{~}r@{~}l} + \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 & \Guard {\cle(a)} {D_0} {D_1} \\ + & & \bnfor & Unreachable + \end{array} + \quad + \begin{array}{l@{~}r@{~}r@{~}l} + \text{\emph{environment}} & \sigma(v) + & \bnfeq & [x_1 \mapsto v_1, \dots, v_n \mapsto v_n] \\ + \text{\emph{closed term}} & \cle(v) + & \bnfeq & (\sigma(v), e) \\ + \text{\emph{accessors}} & a + & \bnfeq & \Root \;\bnfor\; a.n \quad (n \in \mathbb{N}) \\ + \end{array} + \quad + \begin{array}{l} + \pi_S : \text{datatype constructors} + \\ + \pi_T \subseteq \{ \Int n \mid n \in \mathbb{Z} \} + \uplus \{ \Tag n \mid n \in \mathbb{N} \} + \\[1em] + a(v_S), a(v_T), D_S(v_S), D_T(v_T) \quad (\text{\emph{omitted})} + \end{array} +\end{mathpar} +The tree $\Leaf \cle$ returns a leaf expression $e$ in a captured +environment $\sigma$ mapping variables to accessors. +% +$\Failure$ expresses match failure, when no clause matches the input +value. +% +$\Switch a {\Fam {i \in I} {\pi_i, D_i}} \Dfb$ has one subtree $D_i$ +for every head constructor that appears in the pattern matching +clauses, and a fallback case for the constructors. +% +$\Guard \cle {D_0} {D_1}$ represents a \texttt{when}-guard on a closed +expression $\cle$, expected to be of boolean type, with sub-trees +$D_0$ for the \texttt{true} case and $D_1$ for the \texttt{false} +case. + +We write $a(v)$ for the sub-value of the (source or target) value $v$ +that is reachable at the accessor $a$, and $D(v)$ for the result of +running a value $v$ against a decision tree $D$; this results in +a (source or target) matching run $R(v)$, just like running the value +against a program. + To check the equivalence of a source and a target decision tree, we proceed by case analysis. If we have two terminals, such as leaves in the previous example, @@ -710,7 +776,7 @@ Execution follows the rules of Hoare logic: - Conditional : \begin{mathpar} -\infer { \{P \wedge b \} c_1 \{Q\}, \{P\wedge\not b\}c_2\{Q\} } +\infer { \{P \wedge b \} c_1 \{Q\}, \{P\wedge\neg b\}c_2\{Q\} } { \{P\}\text{if b then $c_1$ else $c_2$}\{Q\} } \end{mathpar} @@ -1299,58 +1365,6 @@ captured by the relation $\progrel {t_S} {t_T}$. # TODO eq_muovi \subsection{Grammar of the decision trees} -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. - -The parametrized grammar $D(\pi, e)$ describes the common structure of -source and decision trees. We use $\pi$ for the \emph{conditions} on -each branch, and $a$ for our \emph{accessors}, which give a symbolic -description of a sub-value of the scrutinee. Source conditions $\pi_S$ -are just datatype constructors; target conditions $\pi_T$ are -arbitrary sets of possible immediate-integer or block-tag values. -% -\begin{mathpar} - \begin{array}{l@{~}r@{~}r@{~}l} - \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 & \Guard {\cle(a)} {D_0} {D_1} \\ - & & \bnfor & Unreachable \\ - \text{\emph{accessors}} & a - & \bnfeq & \Root \;\bnfor\; a.n \quad (n \in \mathbb{N}) \\ - \end{array} - \quad - \begin{array}{l} - \pi_S : \text{datatype constructors} - \\ - \pi_T \subseteq \{ \Int n \mid n \in \mathbb{Z} \} - \uplus \{ \Tag n \mid n \in \mathbb{N} \} - \\[1em] - a(v_S), a(v_T), D_S(v_S), D_T(v_T) \quad (\text{\emph{omitted})} - \end{array} -\end{mathpar} -The tree $\Leaf \cle$ returns a leaf expression $e$ in a captured -environment $\sigma$ mapping variables to accessors. -% -$\Failure$ expresses match failure, when no clause matches the input -value. -% -$\Switch a {\Fam {i \in I} {\pi_i, D_i}} \Dfb$ has one subtree $D_i$ -for every head constructor that appears in the pattern matching -clauses, and a fallback case for the constructors. -% -$\Guard \cle {D_0} {D_1}$ represents a \texttt{when}-guard on a closed -expression $\cle$, expected to be of boolean type, with sub-trees -$D_0$ for the \texttt{true} case and $D_1$ for the \texttt{false} -case. - -We write $a(v)$ for the sub-value of the (source or target) value $v$ -that is reachable at the accessor $a$, and $D(v)$ for the result of -running a value $v$ against a decision tree $D$; this results in -a (source or target) matching run $R(v)$, just like running the value -against a program. \subsection{From source programs to decision trees} Let's consider some trivial examples: