984 lines
No EOL
34 KiB
TeX
984 lines
No EOL
34 KiB
TeX
% Created 2020-04-11 Sat 00:26
|
|
% 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{\DZ}{\backslash\text{\{0\}}}
|
|
\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}
|
|
\date{\today}
|
|
\title{}
|
|
\hypersetup{
|
|
pdfauthor={},
|
|
pdftitle={},
|
|
pdfkeywords={},
|
|
pdfsubject={},
|
|
pdfcreator={Emacs 26.3 (Org mode 9.1.9)},
|
|
pdflang={English}}
|
|
\begin{document}
|
|
|
|
\section{Translation validation of the Pattern Matching Compiler}
|
|
\label{sec:org3d79c1b}
|
|
|
|
\subsection{Source program}
|
|
\label{sec:orgc2c278d}
|
|
The algorithm takes as its input a source program and translates it
|
|
into an algebraic data structure which type we call \emph{decision\_tree}.
|
|
|
|
\begin{verbatim}
|
|
type decision_tree =
|
|
| Unreachable
|
|
| Failure
|
|
| Leaf of source_expr
|
|
| Guard of source_blackbox * decision_tree * decision_tree
|
|
| Switch of accessor * (constructor * decision_tree) list * decision_tree
|
|
\end{verbatim}
|
|
|
|
Unreachable, Leaf of source\_expr and Failure are the terminals of the three.
|
|
We distinguish
|
|
\begin{itemize}
|
|
\item Unreachable: statically it is known that no value can go there
|
|
\item Failure: a value matching this part results in an error
|
|
\item Leaf: a value matching this part results into the evaluation of a
|
|
source black box of code
|
|
\end{itemize}
|
|
|
|
The algorithm doesn't support type-declaration-based analysis
|
|
to know the list of constructors at a given type.
|
|
Let's consider some trivial examples:
|
|
|
|
\begin{verbatim}
|
|
function true -> 1
|
|
\end{verbatim}
|
|
|
|
is translated to
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
Switch ([(true, Leaf 1)], Failure)\\
|
|
\end{tabular}
|
|
\end{center}
|
|
while
|
|
\begin{verbatim}
|
|
function
|
|
true -> 1
|
|
| false -> 2
|
|
\end{verbatim}
|
|
will be translated to
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
Switch ([(true, Leaf 1); (false, Leaf 2)])\\
|
|
\end{tabular}
|
|
\end{center}
|
|
|
|
It is possible to produce Unreachable examples by using
|
|
refutation clauses (a "dot" in the right-hand-side)
|
|
\begin{verbatim}
|
|
function
|
|
true -> 1
|
|
| false -> 2
|
|
| _ -> .
|
|
\end{verbatim}
|
|
that gets translated into
|
|
Switch ([(true, Leaf 1); (false, Leaf 2)], Unreachable)
|
|
|
|
We trust this annotation, which is reasonable as the type-checker
|
|
verifies that it indeed holds.
|
|
|
|
Guard nodes of the tree are emitted whenever a guard is found. Guards
|
|
node contains a blackbox of code that is never evaluated and two
|
|
branches, one that is taken in case the guard evaluates to true and
|
|
the other one that contains the path taken when the guard evaluates to
|
|
true.
|
|
|
|
\begin{comment}
|
|
[ ] Finisci con Switch
|
|
[ ] Spiega del fallback
|
|
[ ] rivedi compilazione per tenere in considerazione il tuo albero invece che le Lambda
|
|
\end{comment}
|
|
|
|
The source code of a pattern matching function has the
|
|
following form:
|
|
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
match variable with\\
|
|
\(\vert{}\) pattern$_1$ \(\to\) expr$_1$\\
|
|
\(\vert{}\) pattern$_2$ when guard \(\to\) expr$_2$\\
|
|
\(\vert{}\) pattern$_3$ as var \(\to\) expr$_3$\\
|
|
$\vdots$\\
|
|
\(\vert{}\) p$_n$ \(\to\) expr$_n$\\
|
|
\end{tabular}
|
|
\end{center}
|
|
|
|
Patterns could or could not be exhaustive.
|
|
|
|
Pattern matching code could also be written using the more compact form:
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
function\\
|
|
\(\vert{}\) pattern$_1$ \(\to\) expr$_1$\\
|
|
\(\vert{}\) pattern$_2$ when guard \(\to\) expr$_2$\\
|
|
\(\vert{}\) pattern$_3$ as var \(\to\) expr$_3$\\
|
|
$\vdots$\\
|
|
\(\vert{}\) p$_n$ \(\to\) expr$_n$\\
|
|
\end{tabular}
|
|
\end{center}
|
|
|
|
|
|
This BNF grammar describes formally the grammar of the source program:
|
|
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
start ::= "match" id "with" patterns \(\vert{}\) "function" patterns\\
|
|
patterns ::= (pattern0\(\vert{}\)pattern1) pattern1+\\
|
|
;; pattern0 and pattern1 are needed to distinguish the first case in which\\
|
|
;; we can avoid writing the optional vertical line\\
|
|
pattern0 ::= clause\\
|
|
pattern1 ::= "\(\vert{}\)" clause\\
|
|
clause ::= lexpr "->" rexpr\\
|
|
lexpr ::= rule ($\varepsilon$\(\vert{}\)condition)\\
|
|
rexpr ::= \_code ;; arbitrary code\\
|
|
rule ::= wildcard\(\vert{}\)variable\(\vert{}\)constructor\_pattern\(\vert{}\)\{\}or\_pattern ;;\\
|
|
;; rules\\
|
|
wildcard ::= "\_"\\
|
|
variable ::= identifier\\
|
|
constructor\_pattern ::= constructor (rule\(\vert{}\)$\varepsilon$) (assignment\(\vert{}\)$\varepsilon$)\\
|
|
constructor ::= int\(\vert{}\)float\(\vert{}\)char\(\vert{}\)string\(\vert{}\)bool \(\vert{}\)unit\(\vert{}\)record\(\vert{}\)exn\(\vert{}\)objects\(\vert{}\)ref \(\vert{}\)list\(\vert{}\)tuple\(\vert{}\)array\(\vert{}\)variant\(\vert{}\)parameterized\_variant ;; data types\\
|
|
or\_pattern ::= rule ("\(\vert{}\)" wildcard\(\vert{}\)variable\(\vert{}\)constructor\_pattern)+\\
|
|
condition ::= "when" bexpr\\
|
|
assignment ::= "as" id\\
|
|
bexpr ::= \_code ;; arbitrary code\\
|
|
\end{tabular}
|
|
\end{center}
|
|
|
|
A source program t$_S$ is a collection of pattern clauses pointing to
|
|
\emph{bb} terms. Running a program t$_S$ against an input value v$_S$ produces as
|
|
a result \emph{r}:
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
t$_S$ ::= (p $\to$ bb)\(^{\text{i$\in $I}}\)\\
|
|
p ::= \(\vert{}\) K(p$_i$)$^i$, i $\in $ I \(\vert{}\) (p\(\vert{}\)q) \(\vert{}\) n $\in $ $\mathbb{N}$\\
|
|
r ::= guard list * (Match bb \(\vert{}\) NoMatch \(\vert{}\) Absurd)\\
|
|
t$_S$(v$_S$) $\to$ r\\
|
|
\end{tabular}
|
|
\end{center}
|
|
|
|
TODO: argument on what it means to run a source program
|
|
|
|
\emph{guard} and \emph{bb} expressions are treated as blackboxes of OCaml code.
|
|
A sound approach for treating these blackboxes would be to inspect the
|
|
OCaml compiler during translation to Lambda code and extract the
|
|
blackboxes compiled in their Lambda representation.
|
|
This would allow to test for equality with the respective blackbox at
|
|
the target level.
|
|
Given that this level of introspection is currently not possibile, we
|
|
decided to restrict the structure of blackboxes to the following (valid) OCaml
|
|
code:
|
|
|
|
\begin{verbatim}
|
|
external guard : 'a -> 'b = "guard"
|
|
external observe : 'a -> 'b = "observe"
|
|
\end{verbatim}
|
|
|
|
We assume these two external functions \emph{guard} and \emph{observe} with a valid
|
|
type that lets the user pass any number of arguments to them.
|
|
All the guards are of the form \texttt{guard <arg> <arg> <arg>}, where the
|
|
<arg> are expressed using the OCaml pattern matching language.
|
|
Similarly, all the right-hand-side expressions are of the form
|
|
\texttt{observe <arg> <arg> ...} with the same constraints on arguments.
|
|
|
|
\begin{verbatim}
|
|
type t = K1 | K2 of t (* declaration of an algebraic and recursive datatype t *)
|
|
|
|
let _ = function
|
|
| K1 -> observe 0
|
|
| K2 K1 -> observe 1
|
|
| K2 x when guard x -> observe 2
|
|
| K2 (K2 x) as y when guard x y -> observe 3
|
|
| K2 _ -> observe 4
|
|
\end{verbatim}
|
|
|
|
|
|
|
|
In our prototype we make use of accessors to encode stored values.
|
|
\begin{minipage}{0.2\linewidth}
|
|
\begin{verbatim}
|
|
let value = 1 :: 2 :: 3 :: []
|
|
(* that can also be written *)
|
|
let value = []
|
|
|> List.cons 3
|
|
|> List.cons 2
|
|
|> List.cons 1
|
|
\end{verbatim}
|
|
\end{minipage}
|
|
\hfill
|
|
\begin{minipage}{0.5\linewidth}
|
|
\begin{verbatim}
|
|
|
|
|
|
(field 0 x) = 1
|
|
(field 0 (field 1 x)) = 2
|
|
(field 0 (field 1 (field 1 x)) = 3
|
|
(field 0 (field 1 (field 1 (field 1 x)) = []
|
|
\end{verbatim}
|
|
\end{minipage}
|
|
An \emph{accessor} \emph{a} represents the
|
|
access path to a value that can be reached by deconstructing the
|
|
scrutinee.
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
a ::= Here \(\vert{}\) n.a\\
|
|
\end{tabular}
|
|
\end{center}
|
|
The above example, in encoded form:
|
|
\begin{verbatim}
|
|
Here = 1
|
|
1.Here = 2
|
|
1.1.Here = 3
|
|
1.1.1.Here = []
|
|
\end{verbatim}
|
|
In our prototype the source matrix m$_S$ is defined as follows
|
|
\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}
|
|
|
|
Source matrices are used to build source decision trees C$_S$.
|
|
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}{l}
|
|
C$_S$ ::= Leaf bb \(\vert{}\) Switch(a, (K$_i$ $\to$ C$_i$)\(^{\text{i$\in $S}}\) , C?) \(\vert{}\) Failure \(\vert{}\) Unreachable\\
|
|
v$_S$ ::= K(v$_i$)\(^{\text{i$\in $I}}\) \(\vert{}\) n $\in $ $\mathbb{N}$\\
|
|
\end{tabular}
|
|
\end{center}
|
|
\begin{comment}
|
|
Are K and Here clear here?
|
|
\end{comment}
|
|
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}
|
|
|
|
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:
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
$\llbracket$((p$_i$ $\to$ bb$_i$)\(^{\text{i$\in $I}}\)$\rrbracket$ := $\llbracket$(Here), (p$_i$ $\to$ bb$_i$)\(^{\text{i$\in $I}}\) $\rrbracket$\\
|
|
\end{tabular}
|
|
\end{center}
|
|
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}}\))\\
|
|
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$ |] $\equiv$ 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 source matrix in the case of empty rows returns
|
|
the first expression and (Leaf bb)(v) := Match bb
|
|
\item\relax [| (a$_j$)$^j$, $\varnothing$ |] $\equiv$ 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\DZ}), \\
|
|
( if p_{0j} is k(q_l) then \\
|
|
(q_l)^{l \in Idx(k_k)} +++ (p_{ij})^{i \in I\DZ} \to e_j \\
|
|
if p_{0j} is \_ then \\
|
|
(\_)^{l \in Idx(k_k)} +++ (p_{ij})^{i \in I\DZ} \to e_j \\
|
|
else \bot )^j ), \\
|
|
((a_i)^{i \in I\DZ}, ((p_{ij})^{i \in I\DZ} \to e_j if p_{0j} is \_ else \bot)^{j \in J})
|
|
\end{equation}
|
|
|
|
Groups(m) is an auxiliary function that source 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 decomposition in 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:
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
if k = k$_k$ \text{ for some k then}\\
|
|
\quad m(v$_i$)$^i$ = m$_k$((v\(_{\text{l}}\)')$^l$ \sout{+} (v\(_{\text{i}}\))\(^{\text{i$\in $I}\DZ}\))\\
|
|
\text{else}\\
|
|
\quad m(v$_i$)$^i$ = m\(_{\text{wild}}\)(v$_i$)\(^{\text{i$\in $I}\DZ}\)\\
|
|
\end{tabular}
|
|
\end{center}
|
|
|
|
\begin{comment}
|
|
TODO: fix \{0}
|
|
\end{comment}
|
|
|
|
\begin{enumerate}
|
|
\item Proof:
|
|
\label{sec:org160a47b}
|
|
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
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
((a)\{0.l\})\(^{\text{l$\in $Idx(k$_k$)}}\) \sout{+} (a$_i$)\(^{\text{i$\in $I}\DZ}\)),\\
|
|
(\\
|
|
\quad if p\(_{\text{0j}}\) is k(q$_l$) then\\
|
|
\quad \quad (q$_l$)$^l$ \sout{+} (p\(_{\text{ij}}\))\(^{\text{i$\in $I}\DZ\ }\) $\to$ e$_j$\\
|
|
\quad if p\(_{\text{0j}}\) is \_ then\\
|
|
\quad \quad (\_)$^l$ \sout{+} (p\(_{\text{ij}}\))\(^{\text{i$\in $I}\DZ}\) $\to$ e$_j$\\
|
|
\quad else $\bot$\\
|
|
)\(^{\text{j$\in $J}}\)\\
|
|
\end{tabular}
|
|
\end{center}
|
|
|
|
By definition, m(v$_i$)$^i$ is
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
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$ = \{\\
|
|
\quad if p$_0$ = k(q$_l$)$^l$, v$_0$ = k'(v'$_k$)$^k$, k=Idx(k') and l=Idx(k)\\
|
|
\quad \quad if k $\ne$ k' then $\bot$\\
|
|
if k = k' then ((q$_l$)$^l$ \sout{+} (p$_i$)\(^{\text{i$\in $I}\DZ}\)) ((v'$_k$)$^k$ \sout{+} (v$_i$)\(^{\text{i$\in $I}\DZ}\) )\\
|
|
if p$_0$ = (q$_1$\(\vert{}\)q$_2$) then\\
|
|
First( (q$_1$p$_i$\(^{\text{i$\in $I}\DZ}\)) v$_i$\(^{\text{i$\in $I}\DZ}\), (q$_2$p$_i$\(^{\text{i$\in $I }\DZ}\)) v$_i$\(^{\text{i$\in $I}\DZ}\))\}\\
|
|
\end{tabular}
|
|
\end{center}
|
|
|
|
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}\DZ}\) because v(a$_0$) = K(v(a)\{0.l\})$^l$)
|
|
\end{enumerate}
|
|
|
|
|
|
|
|
\subsection{Target translation}
|
|
\label{sec:orgd2ea1d0}
|
|
|
|
The target program of the following general form is parsed using a parser
|
|
generated by Menhir, a LR(1) parser generator for the OCaml programming language.
|
|
Menhir compiles LR(1) a grammar specification, in this case a subset
|
|
of the Lambda intermediate language, down to OCaml code.
|
|
This is the grammar of the target language (TODO: check menhir grammar)
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
start ::= sexpr\\
|
|
sexpr ::= variable \(\vert{}\) string \(\vert{}\) "(" special\_form ")"\\
|
|
string ::= "$\backslash$"" identifier "$\backslash$"" ;; string between doublequotes\\
|
|
variable ::= identifier\\
|
|
special\_form ::= let\(\vert{}\)catch\(\vert{}\)if\(\vert{}\)switch\(\vert{}\)switch-star\(\vert{}\)field\(\vert{}\)apply\(\vert{}\)isout\\
|
|
let ::= "let" assignment sexpr ;; (assignment sexpr)+ outside of pattern match code\\
|
|
assignment ::= "function" variable variable+ ;; the first variable is the identifier of the function\\
|
|
field ::= "field" digit variable\\
|
|
apply ::= ocaml\_lambda\_code ;; arbitrary code\\
|
|
catch ::= "catch" sexpr with sexpr\\
|
|
with ::= "with" "(" label ")"\\
|
|
exit ::= "exit" label\\
|
|
switch-star ::= "switch*" variable case*\\
|
|
switch::= "switch" variable case* "default:" sexpr\\
|
|
case ::= "case" casevar ":" sexpr\\
|
|
casevar ::= ("tag"\(\vert{}\)"int") integer\\
|
|
if ::= "if" bexpr sexpr sexpr\\
|
|
bexpr ::= "(" ("!="\(\vert{}\)"\texttt{="\textbackslash{}vert\{\}">}"\(\vert{}\)"<="\(\vert{}\)">"\(\vert{}\)"<") sexpr digit \(\vert{}\) field ")"\\
|
|
label ::= integer\\
|
|
\end{tabular}
|
|
\end{center}
|
|
The prototype doesn't support strings.
|
|
|
|
The AST built by the parser is traversed and evaluated by the symbolic
|
|
execution engine.
|
|
Given that the target language supports jumps in the form of "catch - exit"
|
|
blocks the engine tries to evaluate the instructions inside the blocks
|
|
and stores the result of the partial evaluation into a record.
|
|
When a jump is encountered, the information at the point allows to
|
|
finalize the evaluation of the jump block.
|
|
In the environment the engine also stores bindings to values and
|
|
functions.
|
|
Integer additions and subtractions are simplified in a second pass.
|
|
The result of the symbolic evaluation is a target decision tree C$_T$
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
C$_T$ ::= Leaf bb \(\vert{}\) Switch(a, ($\pi$$_i$ $\to$ C$_i$)\(^{\text{i$\in $S}}\) , C?) \(\vert{}\) Failure\\
|
|
v$_T$ ::= Cell(tag $\in $ $\mathbb{N}$, (v$_i$)\(^{\text{i$\in $I}}\)) \(\vert{}\) n $\in $ $\mathbb{N}$\\
|
|
\end{tabular}
|
|
\end{center}
|
|
Every branch of the decision tree is "constrained" by a domain
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
Domain $\pi$ = \{ n\(\vert{}\)n$\in $$\mathbb{N}$ x n\(\vert{}\)n$\in $Tag$\subseteq$$\mathbb{N}$ \}\\
|
|
\end{tabular}
|
|
\end{center}
|
|
Intuitively, the $\pi$ condition at every branch tells us the set of
|
|
possible values that can "flow" through that path.
|
|
$\pi$ conditions are refined by the engine during the evaluation; at the
|
|
root of the decision tree the domain corresponds to the set of
|
|
possible values that the type of the function can hold.
|
|
C? is the fallback node of the tree that is taken whenever the value
|
|
at that point of the execution can't flow to any other subbranch.
|
|
Intuitively, the $\pi$\(_{\text{fallback}}\) condition of the C? fallback node is
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
$\pi$\(_{\text{fallback}}\) = ¬\bigcup\limits\(_{\text{i$\in $I}}\)$\pi$$_i$\\
|
|
\end{tabular}
|
|
\end{center}
|
|
The fallback node can be omitted in the case where the domain of the
|
|
children nodes correspond to set of possible values pointed by the
|
|
accessor at that point of the execution
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
domain(v$_S$(a)) = \bigcup\limits\(_{\text{i$\in $I}}\)$\pi$$_i$\\
|
|
\end{tabular}
|
|
\end{center}
|
|
We say that a translation of a target program to a decision tree
|
|
is correct when for every possible input, the target program and its
|
|
respective decision tree produces the same result
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
$\forall$v$_T$, t$_T$(v$_T$) = $\llbracket$t$_T$$\rrbracket$$_T$(v$_T$)\\
|
|
\end{tabular}
|
|
\end{center}
|
|
|
|
|
|
|
|
\subsection{Equivalence checking}
|
|
\label{sec:org33b978b}
|
|
|
|
The equivalence checking algorithm takes as input a domain of
|
|
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.
|
|
The algorithm respects the following correctness statement:
|
|
|
|
\begin{comment}
|
|
TODO: we have to define what \coversTEX mean for readers to understand the specifications
|
|
(or we use a simplifying lie by hiding \coversTEX in the statements).
|
|
\end{comment}
|
|
|
|
\begin{align*}
|
|
\EquivTEX S {C_S} {C_T} \emptyqueue = \YesTEX \;\land\; \coversTEX {C_T} S
|
|
& \implies
|
|
\forall v_S \approx v_T \in S,\; C_S(v_S) = C_T(v_T)
|
|
\\
|
|
\EquivTEX S {C_S} {C_T} \emptyqueue = \NoTEX {v_S} {v_T} \;\land\; \coversTEX {C_T} S
|
|
& \implies
|
|
v_S \approx v_T \in S \;\land\; C_S(v_S) \neq C_T(v_T)
|
|
\end{align*}
|
|
Our equivalence-checking algorithm \(\EquivTEX S {C_S} {C_T} G\) is
|
|
a exactly decision procedure for the provability of the judgment
|
|
\((\EquivTEX S {C_S} {C_T} G)\), defined below.
|
|
\begin{mathpar}
|
|
\begin{array}{l@{~}r@{~}l}
|
|
& & \text{\emph{constraint trees}} \\
|
|
C & \bnfeq & \Leaf t \\
|
|
& \bnfor & \Failure \\
|
|
& \bnfor & \Switch a {\Fam i {\pi_i, C_i}} \Cfb \\
|
|
& \bnfor & \Guard t {C_0} {C_1} \\
|
|
\end{array}
|
|
|
|
\begin{array}{l@{~}r@{~}l}
|
|
& & \text{\emph{boolean result}} \\
|
|
b & \in & \{ 0, 1 \} \\[0.5em]
|
|
& & \text{\emph{guard queues}} \\
|
|
G & \bnfeq & (t_1 = b_1), \dots, (t_n = b_n) \\
|
|
\end{array}
|
|
|
|
\begin{array}{l@{~}r@{~}l}
|
|
& & \text{\emph{input space}} \\
|
|
S & \subseteq & \{ (v_S, v_T) \mid \vrel {v_S} {v_T} \} \\
|
|
\end{array}
|
|
\\
|
|
\infer{ }
|
|
{\EquivTEX \emptyset {C_S} {C_T} G}
|
|
|
|
\infer{ }
|
|
{\EquivTEX S \Failure \Failure \emptyqueue}
|
|
|
|
\infer
|
|
{\trel {t_S} {t_T}}
|
|
{\EquivTEX S {\Leaf {t_S}} {\Leaf {t_T}} \emptyqueue}
|
|
|
|
\infer
|
|
{\forall i,\;
|
|
\EquivTEX
|
|
{(S \land a = K_i)}
|
|
{C_i} {\trim {C_T} {a = K_i}} G
|
|
\\
|
|
\EquivTEX
|
|
{(S \land a \notin \Fam i {K_i})}
|
|
\Cfb {\trim {C_T} {a \notin \Fam i {K_i}}} G
|
|
}
|
|
{\EquivTEX S
|
|
{\Switch a {\Fam i {K_i, C_i}} \Cfb} {C_T} G}
|
|
|
|
\begin{comment}
|
|
% TODO explain somewhere why the judgment is not symmetric:
|
|
% we avoid defining trimming on source trees, which would
|
|
% require more expressive conditions than just constructors
|
|
\end{comment}
|
|
\infer
|
|
{C_S \in {\Leaf t, \Failure}
|
|
\\
|
|
\forall i,\; \EquivTEX {(S \land a \in D_i)} {C_S} {C_i} G
|
|
\\
|
|
\EquivTEX {(S \land a \notin \Fam i {D_i})} {C_S} \Cfb G}
|
|
{\EquivTEX S
|
|
{C_S} {\Switch a {\Fam i {D_i} {C_i}} \Cfb} G}
|
|
|
|
\infer
|
|
{\EquivTEX S {C_0} {C_T} {G, (t_S = 0)}
|
|
\\
|
|
\EquivTEX S {C_1} {C_T} {G, (t_S = 1)}}
|
|
{\EquivTEX S
|
|
{\Guard {t_S} {C_0} {C_1}} {C_T} G}
|
|
|
|
\infer
|
|
{\trel {t_S} {t_T}
|
|
\\
|
|
\EquivTEX S {C_S} {C_b} G}
|
|
{\EquivTEX S
|
|
{C_S} {\Guard {t_T} {C_0} {C_1}} {(t_S = b), G}}
|
|
\end{mathpar}
|
|
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$) $\equiv$ 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$) $\equiv$ C$_T$(v$_T$) ) $\to$ r\\
|
|
t$_T$(v$_T$) $\to$ r\\
|
|
result r ::= guard list * (Match blackbox \(\vert{}\) NoMatch \(\vert{}\) Absurd)\\
|
|
guard ::= blackbox.\\
|
|
\end{tabular}
|
|
\end{center}
|
|
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$, 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 result of the proposed equivalence algorithm is \emph{Yes} or \emph{No(v$_S$,
|
|
v$_T$)}. In particular, in the negative case, v$_S$ and v$_T$ are a couple of
|
|
possible counter examples for which the decision trees produce a
|
|
different result.
|
|
|
|
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}
|
|
We say that C$_T$ covers the input space \emph{S}, written
|
|
\emph{covers(C$_T$, S)} when every value v$_S$$\in $S is a valid input to the
|
|
decision tree C$_T$. (TODO: rephrase)
|
|
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{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 \emph{a} $\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$}}\)(v$_T$)\\
|
|
\end{tabular}
|
|
\end{center}
|
|
We prove this by induction on C$_T$:
|
|
|
|
\begin{itemize}
|
|
\item C$_T$ = Leaf\(_{\text{bb}}\): when the decision tree is a leaf terminal, the result of trimming on a Leaf is the Leaf itself
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
Leaf\(_{\text{bb/a$\to$$\pi$}}\)(v) = Leaf\(_{\text{bb}}\)(v)\\
|
|
\end{tabular}
|
|
\end{center}
|
|
\item The same applies to Failure terminal
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
Failure\(_{\text{/a$\to$$\pi$}}\)(v) = Failure(v)\\
|
|
\end{tabular}
|
|
\end{center}
|
|
\item When C$_T$ = Switch(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}
|
|
Switch(b, ($\pi$$\to$C$_i$)\(^{\text{i$\in $I}}\))\(_{\text{/a$\to$$\pi$}}\) := Switch(b, ($\pi$'$_i$$\to$C\(_{\text{i/a$\to$$\pi$}}\))\(^{\text{i$\in $I}}\))\\
|
|
\end{tabular}
|
|
\end{center}
|
|
\end{itemize}
|
|
\begin{comment}
|
|
TODO: understand how to properly align lists
|
|
check that every list is aligned
|
|
\end{comment}
|
|
For the trimming lemma we have to prove that running the value v$_T$ against
|
|
the decision 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$) = Switch(b, ($\pi$$_i$'$\to$C\(_{\text{i/a$\to$$\pi$}}\))\(^{\text{i$\in $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 \(\vert{}\) 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$) = Switch(b, ($\pi$$_i$'$\to$C\(_{\text{i/a$\to$$\pi$}}\))\(^{\text{i$\in $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 v$_T$$\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}{l}
|
|
equiv(S, C$_S$, C$_T$) $\to$ Yes \(\vert{}\) 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$, Switch(a, ($\pi$$_i$ $\to$ C$_T$$_i$)\(^{\text{i$\in $I}}\))) := Forall(equiv( S$\cap$a$\to$$\pi$(k$_i$)), C$_S$, C$_T$$_i$)\(^{\text{i$\in $I}}\))\\
|
|
equiv(S, Leaf bb$_S$ as C$_S$, Switch(a, ($\pi$$_i$ $\to$ C$_T$$_i$)\(^{\text{i$\in $I}}\))) := Forall(equiv( S$\cap$a$\to$$\pi$(k$_i$)), C$_S$, C$_T$$_i$)\(^{\text{i$\in $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 Switch on the right we define $\pi$\(_{\text{fallback}}\) as the domain of
|
|
values not covered but the union of the constructors k$_i$
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
$\pi$\(_{\text{fallback}}\) = ¬\bigcup\limits\(_{\text{i$\in $I}}\)$\pi$(k$_i$)\\
|
|
\end{tabular}
|
|
\end{center}
|
|
The algorithm proceeds by trimming
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
equiv(S, Switch(a, (k$_i$ $\to$ C$_S$$_i$)\(^{\text{i$\in $I}}\), C\(_{\text{sf}}\)), C$_T$) :=\\
|
|
Forall(equiv( S$\cap$(a$\to$$\pi$(k$_i$)\(^{\text{i$\in $I}}\)), C$_S$$_i$, C\(_{\text{t/a$\to$$\pi$(k$_i$)}}\))\(^{\text{i$\in $I}}\) \sout{+} equiv(S$\cap$(a$\to$$\pi$$_n$), C$_S$, C\(_{\text{a$\to$$\pi$}_{\text{fallback}}}\)))\\
|
|
\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$)\(^{\text{i$\in $I}}\)), C$_S$$_i$, C\(_{\text{t/a$\to$$\pi$(k$_i$)}}\))\(^{\text{i$\in $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}
|
|
|