latex on intro
This commit is contained in:
parent
286cda4043
commit
2e830c2872
1 changed files with 67 additions and 53 deletions
|
@ -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
|
Lambda code. For example, cons cells \texttt{x::xs} or tuples
|
||||||
\texttt{(x,y)} are blocks with tag 0.
|
\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,
|
To check the equivalence of a source and a target decision tree,
|
||||||
we proceed by case analysis.
|
we proceed by case analysis.
|
||||||
If we have two terminals, such as leaves in the previous example,
|
If we have two terminals, such as leaves in the previous example,
|
||||||
|
@ -710,7 +776,7 @@ Execution follows the rules of Hoare logic:
|
||||||
|
|
||||||
- Conditional :
|
- Conditional :
|
||||||
\begin{mathpar}
|
\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\} }
|
{ \{P\}\text{if b then $c_1$ else $c_2$}\{Q\} }
|
||||||
\end{mathpar}
|
\end{mathpar}
|
||||||
|
|
||||||
|
@ -1299,58 +1365,6 @@ captured by the relation $\progrel {t_S} {t_T}$.
|
||||||
# TODO eq_muovi
|
# TODO eq_muovi
|
||||||
|
|
||||||
\subsection{Grammar of the decision trees}
|
\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}
|
\subsection{From source programs to decision trees}
|
||||||
Let's consider some trivial examples:
|
Let's consider some trivial examples:
|
||||||
|
|
Loading…
Reference in a new issue