bparodi/UniTO
1
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

mail gabriel e coppo

Browse source
This commit is contained in:
Francesco Mecca 2020-04-11 00:31:10 +02:00
parent d5b2944465
commit 28a48f4755
4 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
tesi/.gitignore vendored
View file

@ -3,7 +3,6 @@ tesi.tex
tesi_unicode.tex tesi_unicode.tex
part4_unicode.tex part4_unicode.tex
part4.tex
## Core latex/pdflatex auxiliary files: ## Core latex/pdflatex auxiliary files:

1
tesi/gabriel/notations.sty Symbolic link
View file

@ -0,0 +1 @@
../notations.sty

BIN
tesi/gabriel/part4.pdf
View file

Binary file not shown.

12
tesi/gabriel/part4.tex
View file

@ -1,4 +1,4 @@
% Created 2020-04-11 Sat 00:26 % Created 2020-04-11 Sat 00:31
% Intended LaTeX compiler: pdflatex % Intended LaTeX compiler: pdflatex
\documentclass[11pt]{article} \documentclass[11pt]{article}
\usepackage[utf8]{inputenc} \usepackage[utf8]{inputenc}
@ -64,10 +64,10 @@ xleftmargin=1em,
\begin{document} \begin{document}
\section{Translation validation of the Pattern Matching Compiler} \section{Translation validation of the Pattern Matching Compiler}
\label{sec:org3d79c1b} \label{sec:org9d32dd4}
\subsection{Source program} \subsection{Source program}
\label{sec:orgc2c278d} \label{sec:org0032637}
The algorithm takes as its input a source program and translates it The algorithm takes as its input a source program and translates it
into an algebraic data structure which type we call \emph{decision\_tree}. into an algebraic data structure which type we call \emph{decision\_tree}.
@ -412,7 +412,7 @@ TODO: fix \{0}
\begin{enumerate} \begin{enumerate}
\item Proof: \item Proof:
\label{sec:org160a47b} \label{sec:orgb73fb4f}
Let \(m\) be a matrix with \[Group(m) = (k_r \to m_r)^k, m_{wild}\] 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. Let \((v_i)^i\) be an input matrix with \(v_0 = k(v'_l)^l\) for some k.
We proceed by case analysis: We proceed by case analysis:
@ -472,7 +472,7 @@ We can also show that a$_i$ = (a\(_{\text{0.l}}\))$^l$ \sout{+} a\(_{\text{i$\in
\subsection{Target translation} \subsection{Target translation}
\label{sec:orgd2ea1d0} \label{sec:org0337fa8}
The target program of the following general form is parsed using a parser 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. generated by Menhir, a LR(1) parser generator for the OCaml programming language.
@ -560,7 +560,7 @@ $\forall$v$_T$, t$_T$(v$_T$) = $\llbracket$t$_T$$\rrbracket$$_T$(v$_T$)\\
\subsection{Equivalence checking} \subsection{Equivalence checking}
\label{sec:org33b978b} \label{sec:org7268798}
The equivalence checking algorithm takes as input a domain of The equivalence checking algorithm takes as input a domain of
possible values \emph{S} and a pair of source and target decision trees and possible values \emph{S} and a pair of source and target decision trees and