tesi altri punti

anno3/apprendimento_automatico/slides/todo.org

@@ -0,0 +1,5 @@
+* TODO [0/1]
+- [ ] 002:
+  - [ ] Laplace adjustment
+  - [ ] Output code decoding
+  - [ ] Itemeset bUh frequent: significato frequent

tesi/tesi_unicode.org

@@ -216,7 +216,7 @@ the scrutinee.
 \\
 Target decision trees have a similar shape but the tests on the
 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 blocks \texttt{x::xs} or tuples
 \texttt{(x,y)} are memory blocks with tag 0.
 \\
 The following parametrized grammar $D(\pi, e)$ describes the common structure of
@@ -526,12 +526,12 @@ For runtime values, OCaml uses a uniform memory representation in
 which every variable is stored as a value in a contiguous block of
 memory.
 Every value is a single word that is either a concrete integer or a
-pointer to another block of memory, that is called /cell/ or /box/.
+pointer to another block of memory, that is called /block/ or /box/.
 We can abstract the type of OCaml runtime values as the following:
 #+BEGIN_SRC 
-type t = Constant | Cell of int * t 
+type t = Constant | Block of int * t 
 #+END_SRC
-where a one bit tag is used to distinguish between Constant or Cell.
+where a one bit tag is used to distinguish between Constant or Block.
 In particular this bit of metadata is stored as the lowest bit of a
 memory block.
 \\
@@ -615,7 +615,7 @@ let test = function
 In the case of types with a smaller number of variants, the pattern
 matching compiler may avoid the overhead of computing a jump table.
 This example also highlights the fact that non constant constructor
-are mapped to cons cell that are accessed using the /tag/ directive.
+are mapped to cons blocks that are accessed using the /tag/ directive.
 #+BEGIN_SRC 
 (setglobal Prova!
   (let
@@ -907,12 +907,12 @@ Primitive OCaml datatypes include aggregate types in the form of
 functors. [CIT]
 Low level /Lambda/ untyped constructors of the form
 #+BEGIN_SRC 
-type t = Constant | Cell of int * t 
+type t = Constant | Block of int * t 
 #+END_SRC
 provides enough flexibility to encode source higher kinded types.
 This shouldn't surprise because the /Lambda/ language consists of
-s-expressions. The /field/ operation allows to address a /Cell/ value
+s-expressions. The /field/ operation allows to address a /Block/ value;
-and the expressions /(field 0 x)/ and /(field 1 x)/ are equivalent to
+the expressions /(field 0 x)/ and /(field 1 x)/ are equivalent to
 the Lisp primitives /(car x)/ and /(cdr x)/ respectively.
 \begin{comment}
 (* that can also be written *)
@@ -936,11 +936,11 @@ let value =  1 :: 2 :: 3 :: []
 \end{minipage} \\
 \\
 We can represent the concrete value of a higher kinded type as a flat
-list of cells.
+list of blocks.
 In the prototype we call this "view" into the value of a datatype the
 \emph{accessor} /a/.
 | a ::= Here \vert n.a
-Accessors have some resemblance with the low level /Cell/ values, such
+Accessors have some resemblance with the low level /Block/ values, such
 as the fact that both don't encode type informations; for example the
 accessor of a list of integers is structurally equivalent to the
 accessor of a tuple containing the same elements.
@@ -952,8 +952,8 @@ At the source level /accessors/ are constructed by inspecting the structure of
 the patterns at hand.
 At the target level /accessors/ are constructed by compressing the steps taken by
 the symbolic engine during the evaluation of a value.
-/Accessors/ don't store informations about the concrete value of the scrutinee or
+/Accessors/ don't store any kind of information about the concrete
-it's symbolic domain of values.
+value of the scrutinee.
 
 ** Source program
 The OCaml source code of a pattern matching function has the
@@ -1037,11 +1037,11 @@ following rules apply
 When a value /v/ matches pattern /p/ we say that /v/ is an /instance/ of /p/.
 
 
-During compilation by the translators, expressions at the
+During compilation by the translator, expressions at the
 right-hand-side are compiled into
 Lambda code and are referred as lambda code actions lᵢ.
 \\
-We define the /pattern matrix/ P as the matrix |m x n| where m bigger
+We define the /pattern matrix/ P as the matrix |m x n| where m is bigger
 or equal than the number of clauses in the source program and n is
 equal to the arity of the constructor with the gratest arity.
 \begin{equation*}
@@ -1053,14 +1053,18 @@ p_{2,1} & p_{2,2} & \cdots & p_{2,n}  \\
 p_{m,1} & p_{m,2} & \cdots & p_{m,n} )
 \end{pmatrix}
 \end{equation*}
-every row of /P/ is called a pattern vector
+Every row of /P/ is called a pattern vector
- $\vec{p_i}$ = (p₁, p₂, ..., pₙ); In every instance of P pattern
+ $\vec{p_i}$ = (p₁, p₂, ..., pₙ); in every instance of P pattern
 vectors appear normalized on the length of the longest pattern vector.
 Considering the pattern matrix P we say that the value vector
 $\vec{v}$ = (v₁, v₂, ..., vᵢ) matches the pattern vector pᵢ in P  if and only if the following two
 conditions are satisfied:
-- p_{i,1}, p_{i,2}, \cdots, p_{i,n}  ≼ (v₁, v₂, ..., vᵢ)
+- p_{i,1}, p_{i,2}, \cdots, p_{i,n}  ≼ (v₁, v₂, ..., vₙ)
-- ∀j < i p_{j,1}, p_{j,2}, \cdots, p_{j,n} ⋠ (v₁, v₂, ..., vᵢ) 
+- ∀j < i p_{j,1}, p_{j,2}, \cdots, p_{j,n} ⋠ (v₁, v₂, ..., vₙ) 
+In other words given the pattern vector of the i-th row pᵢ, we say
+that pᵢ matches $\vec{v}$ if every
+element vₖ of $\vec{v}$ is an instance of the corresponding sub-patten
+p_{i,k} and none of the pattern vectors of the previous rows matches.
 \\
 We can define the following three relations with respect to patterns:
 - Pattern p is less precise than pattern q, written p ≼ q, when all
@@ -1074,7 +1078,7 @@ Wit the support of two auxiliary functions
   | tail((xᵢ)^{i ∈ I}) := (xᵢ)^{i ≠ min(I)}
 - first non-⊥ element of an ordered family
   | First((xᵢ)ⁱ) := ⊥ \quad \quad \quad if ∀i, xᵢ = ⊥
-  | First((xᵢ)ⁱ) := x_min{i \vert{} xᵢ ≠ ⊥}  \quad  if ∃i, xᵢ ≠ ⊥
+  | First((xᵢ)ⁱ) := x_{min{i \vert{} xᵢ ≠ ⊥}}  \quad  if ∃i, xᵢ ≠ ⊥
 we now define what it means to run a pattern row against a value
 vector of the same length, that is (pᵢ)ⁱ(vᵢ)ⁱ
 | pᵢ                       | vᵢ                   | result_{pat}                                    |
@@ -1087,7 +1091,7 @@ vector of the same length, that is (pᵢ)ⁱ(vᵢ)ⁱ
 | (q₁\vert{}q₂, tail(pᵢ)ⁱ) | (vᵢ)ⁱ                | First((q₁,tail(pᵢ)ⁱ)(vᵢ)ⁱ, (q₂,tail(pᵢ)ⁱ)(vᵢ)ⁱ) |
 \\
 A source program tₛ is a collection of pattern clauses pointing to
-/bb/ terms. Running a program tₛ against an input value vₛ, written
+blackbox /bb/ terms. Running a program tₛ against an input value vₛ, written
 tₛ(vₛ) produces a result /r/ belonging to the following grammar:
 | tₛ ::= (p → bb)^{i∈I}
 | tₛ(vₛ) → r
@@ -1109,25 +1113,26 @@ TODO: understand how to explain guard
 \end{comment}
 We can define what it means to run an input value vₛ against a source
 program tₛ:
-| First((xᵢ)ⁱ) := x_min{i \vert{} xᵢ ≠ ⊥}  \quad  if ∃i, xᵢ ≠ ⊥ 
 | tₛ(vₛ) := NoMatch \quad if ∀i, pᵢ(vₛ) = ⊥
 | tₛ(vₛ) = { Absurd if bb_{i₀} = . (refutation clause)
 | \quad \quad \quad \quad \quad Match (σ, bb_{i₀}) otherwise
 | \quad \quad \quad \quad \quad where iₒ = min{i \vert{} pᵢ(vₛ) ≠ ⊥}
-/guard/ and /bb/ expressions are treated as blackboxes of OCaml code.
+Expressions of type /guard/ and /bb/ 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 structural equality with the counterpart
 Lambda blackboxes at the target level.
-Given that this level of introspection is currently not possibile, we
+Given that this level of introspection is currently not possibile
+because the OCaml compiler performs the translation of the pattern
+clauses in a single pass, we
 decided to restrict the structure of blackboxes to the following (valid) OCaml
 code:
 #+BEGIN_SRC 
 external guard : 'a -> 'b = "guard"
 external observe : 'a -> 'b = "observe"
 #+END_SRC 
-We assume these two external functions /guard/ and /observe/ with a valid
+We assume the existence of these two external functions /guard/ and /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.
@@ -1365,11 +1370,10 @@ let f x = match x with
   | 6 -> "6"
   | _ -> "_"
 #+END_SRC
-#+BEGIN_SRC
+\begin{verbatim}
-(setglobal Prova!
+(let
-  (let
   (f/80 =
-       (function x/81[int]
+     (function x/81
        (catch
          (let (switcher/83 =a (-3+ x/81))
            (if (isout 3 switcher/83) (exit 1)
@@ -1379,99 +1383,17 @@ let f x = match x with
               case int 2: "5"
               case int 3: "6")))
         with (1) "_")))
-    (makeblock 0 f/80)))
+  (makeblock 0 f/80))
-#+END_SRC
+\end{verbatim}
 The prototype takes into account such transformations and at the end
 of the symbolic evaluation it traverses the result in order to "undo"
 such optimization and have accessors of the variables match their
 intended value directly.
 
 ** Decision Trees
-For the source language we use Source matrices to build source
+We have already given the parametrized grammar for decision trees and
-decision trees Cₛ,
+we will now show how a decision tree is constructed from source and
-while in the case of the target language the decision tree Cₜ is the
+target programs.
-result of the symbolic execution on the lambda code.
-We give the following definitions.
-| Source and target programs: tₛ and tₜ 
-| Source and target expressions: eₛ and eₜ
-A source program $t_S$ is a list of pattern-matching
-clauses (with an optional \texttt{when}-guard) of the form
-\lstinline{| $p$ (when $e_S$)? -> $e_S$}, and a target program $t_T$
-is a series of control-flow conditionals (\texttt{if, switch,
-  Match\_failure, catch, exit}), value access (\texttt{field}),
-variable bindings (\texttt{let}) and comparison operators in Lambda
-code, with arbitrary Lambda-code expressions $e_T$ at the leaves.
-\\
-We assume given an equivalence relation $\erel {e_S} {e_T}$ on
-expressions (that are contained in the leaves of the decision trees).
-In our translation-validation setting, it suffices to
-relate each source expression to its compiled form -- the compiler
-computes this relation. We have to lift this relation on leaves
-into an equivalence procedure for (pattern-matching) programs.
-\\
-We already defined what it means to run a value vₛ against a program
-tₛ:
-| tₛ(vₛ) := NoMatch \quad if ∀i, pᵢ(vₛ) = ⊥
-| tₛ(vₛ) = { Absurd if bb_{i₀} = . (refutation clause)
-| \quad \quad \quad \quad \quad Match (σ, bb_{i₀}) otherwise
-| \quad \quad \quad \quad \quad where iₒ = min{i \vert{} pᵢ(vₛ) ≠ ⊥}
-and simmetrically, to run a value vₜ against a target program tₜ:
-# TODO t_t
-Starting from this we can define a 
-a relation $\vrel {v_S} {v_T}$ to relate a source to a target value
-in terms of equivalence between the two results:
-\begin{mathpar}
-  \erel {e_S} {e_T} \; (\text{\emph{assumed}})
-
-  t_S(v_S),\ t_T(v_T),\ \vrel {v_S} {v_T} \; (\text{\emph{omitted}})
-
-  \resrel {r_S} {r_T}, \runrel {R_S} {R_T} \; (\text{\emph{simple}})
-\\
-  \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) \\
-  \end{array}
-\quad
-  \begin{array}{l@{~}r@{~}r@{~}l}
-    \text{\emph{matching result}} & r(v)
-    & \bnfeq & \NoMatch \bnfor \Match {\cle(v)} \\
-    \text{\emph{matching run}} & R(v)
-    & \bnfeq & (\cle(v)_1, \dots, \cle(v)_n), r(v) \\
-  \end{array}
-\\
-  \infer
-  {\forall x,\ \vrel {\sigma_S(x)} {\sigma_T(x)}}
-  {\envrel {\sigma_S} {\sigma_T}}
-
-  \infer
-  {\envrel {\sigma_S} {\sigma_T} \\ \erel {e_S} {e_T}}
-  {\clerel {(\sigma_S, e_S)} {(\sigma_T, e_T)}}
-
-  \infer
-  {\forall {\vrel {v_S} {v_T}},\quad \runrel {t_S(v_S)} {t_T(v_T)}}
-  {\progrel t_S t_T}
-\end{mathpar}
-
-This relation captures our knowledge of the
-OCaml value representation, for example it relates the empty list
-constructor \texttt{[]} to $\Int 0$. We can then define \emph{closed}
-expressions $\cle$, pairing a (source or target) expression with the
-environment $\sigma$ captured by a program, and what it means to
-``run'' a value against a program or a decision, written $t(v)$ and
-$D(v)$, which returns a trace $(\cle_1, \dots, \cle_n)$ of the
-executed guards and a \emph{matching result} $r$.
-\\
-Once formulated in this way, our equivalence algorithm must check the
-natural notion of input-output equivalence for matching programs,
-captured by the relation $\progrel {t_S} {t_T}$.
-# TODO eq_muovi
-
-\subsection{Grammar of the decision trees}
-We have already given the parametrized grammar for decision trees that
-we will now explore in details.
-
 \begin{mathpar}
   \begin{array}{l@{~}r@{~}r@{~}l}
     \text{\emph{decision trees}} & D(\pi, e)
@@ -1496,9 +1418,9 @@ we will now explore in details.
 While the branches of a decision tree represents intuitively the
 possible paths that a program can take, branch conditions πₛ and πₜ
 represents the shape of possible values that can flow along that path.
-They refine 
+
-\\
+
-\subsection{From source programs to decision trees}
+\subsubsection{From source programs to decision trees}
 Let's consider some trivial examples:
 | function true -> 1
 is translated to
@@ -1705,10 +1627,10 @@ we have to prove that
 
 # TODO
 
-\subsection{From target programs to target decision trees}
+\subsubsection{From target programs to target decision trees}
 # TODO: replace C with D
 Symbolic Values during symbolic evaluation have the following form
-| vₜ ::= Cell(tag ∈ ℕ, (vᵢ)^{i∈I}) \vert n ∈ ℕ
+| vₜ ::= Block(tag ∈ ℕ, (vᵢ)^{i∈I}) \vert n ∈ ℕ
 The result of the symbolic evaluation is a target decision tree Cₜ
 | Cₜ ::= Leaf bb \vert Switch(a, (πᵢ → Cᵢ)^{i∈S} , C?) \vert Failure
 Every branch of the decision tree is "constrained" by a domain πₜ that
@@ -1735,6 +1657,109 @@ respective decision tree produces the same result
 
 
 ** Equivalence checking
+\subsubsection{Introductory remarks}
+We assume as given an equivalence relation $\erel {e_S} {e_T}$ on
+expressions (that are contained in the leaves of the decision trees).
+As highlighted before, in the prototype we use a simple structural
+equivalence between $observe$ expressions but ideally we could query
+the OCaml compiler and compare the blackboxes in Lambda form.
+We already defined what it means to run a value vₛ against a program
+tₛ:
+| tₛ(vₛ) := NoMatch \quad if ∀i, pᵢ(vₛ) = ⊥
+| tₛ(vₛ) = { Absurd if bb_{i₀} = . (refutation clause)
+| \quad \quad \quad \quad \quad Match (σ, bb_{i₀}) otherwise
+| \quad \quad \quad \quad \quad where iₒ = min{i \vert{} pᵢ(vₛ) ≠ ⊥}
+and simmetrically, to run a value vₜ against a target program tₜ:
+# TODO t_t todo.1 
+We denote as $\vrel {v_S} {v_T}$ the equivalence relation between a
+source value vₛ and a target value vₜ. The relationship is proven by
+structural induction.
+\begin{mathpar}
+  \infer[integers]
+  {\quad}
+  {\vrel {i} {(i)}}
+
+  \infer[boolean]
+  {\quad}
+  {\vrel {false} {(0)}}
+
+  \infer[boolean]
+  {\quad}
+  {\vrel {true} {(1)}}
+
+  \infer[unit value]
+  {\quad}
+  {\vrel {()} {(0)}}
+
+  \infer[Empty List]
+  {\quad}
+  {\vrel {[]} {(0)}}
+
+  \infer[List]
+  {\vrel {v_S} {v_T} \\ \vrel {v'_S} {v'_T}}
+  {\vrel {[v_S; v'_{S}]} {(block \enspace v_T \enspace v'_{T})}}
+
+  \infer[Tuple]
+  {\vrel {v_S} {v_T} \\ \vrel {v'_S} {v'_T}}
+  {\vrel {(v_S; v'_{S})} {(block \enspace v_T \enspace v'_{T})}}
+
+  \infer[Record]
+  {\vrel {v_S} {v_T} \\ \vrel {v'_S} {v'_T}}
+  {\vrel {\{v_S; v'_{S}\}} {(block \enspace v_T \enspace v'_{T})}}
+  
+  \infer[constant constructor]
+  {K_i \in Variant }
+  {\vrel {K_i} {(i)}}
+
+  \infer[Variant]
+  {K_i \in Variant \\ \vrel {v_S} {v_T}}
+  {\vrel {K_i v_S} {(block \enspace (tag \enspace i) \enspace v_T)}}
+\end{mathpar}
+The relation $\vrel {v_S} {v_T}$ captures our knowledge of the
+OCaml value representation, for example it relates the empty list
+constructor \texttt{[]} to $\Int 0$. We can then define \emph{closed}
+expressions $\cle$, pairing a (source or target) expression with the
+environment σ captured by a program, and what it means to
+``run'' a value against a program or a decision, written $t(v)$ and
+$D(v)$, which returns a trace $(\cle_1, \dots, \cle_n)$ of the
+executed guards and a \emph{matching result} $r$.
+\begin{mathpar}
+  \erel {e_S} {e_T} \; (\text{\emph{assumed}})
+
+  t_S(v_S),\ t_T(v_T),\ \vrel {v_S} {v_T} \; 
+
+  \resrel {r_S} {r_T}, \runrel {R_S} {R_T} \; (\text{\emph{simple}})
+\\
+  \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) \\
+  \end{array}
+\quad
+  \begin{array}{l@{~}r@{~}r@{~}l}
+    \text{\emph{matching result}} & r(v)
+    & \bnfeq & \NoMatch \bnfor \Match {\cle(v)} \\
+    \text{\emph{matching run}} & R(v)
+    & \bnfeq & (\cle(v)_1, \dots, \cle(v)_n), r(v) \\
+  \end{array}
+\\
+  \infer
+  {\forall x,\ \vrel {\sigma_S(x)} {\sigma_T(x)}}
+  {\envrel {\sigma_S} {\sigma_T}}
+
+  \infer
+  {\envrel {\sigma_S} {\sigma_T} \\ \erel {e_S} {e_T}}
+  {\clerel {(\sigma_S, e_S)} {(\sigma_T, e_T)}}
+
+  \infer
+  {\forall {\vrel {v_S} {v_T}},\quad \runrel {t_S(v_S)} {t_T(v_T)}}
+  {\progrel t_S    t_T}
+\end{mathpar}
+Once formulated in this way, our equivalence algorithm must check the
+natural notion of input-output equivalence for matching programs,
+captured by the relation $\progrel {t_S} {t_T}$.
+\subsubsection{The equivalence checking algorithm}
 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.

todo.org

@@ -1,41 +1,18 @@
-* Prog Mobile [10/11]
-- [X] Api all songs
-- [X] relazione
-- [X] slides
-- [X] teoria
-- [X] account prof
-- [X] Vnc sul fisso
-- [X] vedi differenza inizializzazione swift
-- [-] Elenco roba da ripetere [13/14]
-  - [ ] Presentazione   
-  - [X] Generiche di Kotlin
-  - [X] Application Framework
-  - [X] Activity
-  - [X] Broadcast receiver
-  - [X] Apk
-  - [X] Security model
-  - [X] Intents
-  - [X] data storage
-  - [X] gerarchia dei processi
-  - [X] inizializzazione classi swift
-  - [X] Arc GC
-  - [X] ios fs
-  - [X] coredata
-- [X] GCD Swift
-- [X] GC swift
-- [X] Android adapters
-** Roba da ripetere
-
-
 * Apprendimento Automatico [2/2]
 - [X] Scrivile per date di esame
 - [X] Richiedi date esame
 
 
-* Tesi [3/27]
+* Tesi [8/31]
 - [ ] Rivedere inference rules di Gabriel e aggiustarle con le mie
 - [ ] Definisci domain sempre allo stesso modo, con bigcup o |
-- [ ] Definizione di First(x_i): serve?
+- [X] Definizione di First(x_i): serve?
+- [ ] ~1444: run t_t against value (todo.1)
+- [X] ~1435: equivalence v_s v_t: formulala, correggi omitted
+- [ ] Definisci Run e =_run
+- [X] 3.4: DECISION TREE CHAPTER
+  + [X] sposta inferenze sotto decision tree in equivalenze?
+  + [X] Rivedi sezioni: magari le altre mettile come sottosezioni
 - [ ] Equivalenza R_s R_T (run)
 - [ ] TODO t_t
 - [ ] Introduzione: Explain covers alla fine (o vedi che si fa nel paper)
@@ -46,6 +23,8 @@
   + [ ] Esempio full signature match: allinea
   + [ ] 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] segreteria: tesi inglese
 - [X] Gatti: inglese
 - [X] Gatti: Coppo mio relatore
@@ -71,8 +50,8 @@
 - [ ] Spiega perche` trimming non simmetrico
 - [ ] Spiega meglio le guards on equivalence checking
 - [ ] t_T e t_S o t_t e t_s???
-- [ ] TODO eq_muovi : si parla di eq checking, forse non li`
+- [X] TODO eq_muovi : si parla di eq checking, forse non li`
-- [ ] Gabriel: quello che penso sulle equivalenze omesse e` giusto?
+- [X] Gabriel: quello che penso sulle equivalenze omesse e` giusto?
 - [ ] Cambia le C di constraint tree in D
 - [ ] TODO on the org file
 HALP