more on the language section

language.tex

@@ -82,8 +82,8 @@ new syntactic category, called \textbf{type schemes}, that denotes a set of type
 Note that $\tsint \ts$ is closed under subsumption and intersection (straightforward induction).
 \end{definition}
 
-\begin{definition}[Representant]
-  We define a function $\tsrep {\_}$ that maps any non-empty type scheme to a type (a \textit{representant}).
+\begin{definition}[Representative]
+  We define a function $\tsrep {\_}$ that maps every non-empty type scheme into a type, \textit{representative} of the set of types denoted by the scheme.
 
   \begin{align*}
     \begin{array}{lcl}
@@ -94,9 +94,8 @@ Note that $\tsint \ts$ is closed under subsumption and intersection (straightfor
     \tsrep \tsempty && \textit{undefined}
     \end{array}
   \end{align*}
-
-Note that $\tsrep \ts \in \tsint \ts$.
 \end{definition}
+Note that $\tsrep \ts \in \tsint \ts$.
 
 \begin{lemma}
   Let $\ts$ be a type scheme and $t$ a type. We can compute a type scheme, written $t \tsand \ts$, such that:

language2.tex

@@ -87,7 +87,7 @@ values.
 
 
 
-\subsection{Dynamic semantics}
+\subsection{Dynamic semantics}\label{sec:opsem}
 
 The dynamic semantics is defined as a classic left-to-right cbv reduction for a $\lambda$-calculus with pairs enriched with a specific rule for type-cases. We have the following  notions of reduction:
 \[
@@ -437,17 +437,20 @@ illustrated in the introduction and it is sound. Now the problem is to
 decide whether an expression is well typed or not, that is, to find an
 algorithm that given a type environment $\Gamma$ and an expression $e$
 decides whether there exists a type $t$ such that $\Gamma\vdash e:t$
-is probable. For that we need to solve essentially three problems: $(i)$ how to handle the fact that it is possible to deduce several types for the same well-typed expression $(2)$ how to compute the auxiliary deduction system for paths.
-
-The origin of multiple types are of two distinct origins that will
-require two distinct technical solutions. The first origin is the rule
-\Rule{Abs-} by which it is possible to deduce for every well-typed
-lambda abstractions infinitely many types, that is the annotation of
-the function intersected with as many negations of arrow types as it
-is possible without making the type empty. To handle this multiplicity
-we use the technique of \emph{type schemes} defined
+is probable. For that we need to solve essentially three problems:
+$(i)$ how to handle the fact that it is possible to deduce several
+types for the same well-typed expression $(ii)$ how to compute the
+auxiliary deduction system for paths.
+
+Multiple types have two distinct origins each requiring a distinct
+technical solution.  The first origin is the rule \Rule{Abs-} by which
+it is possible to deduce for every well-typed lambda abstractions
+infinitely many types, that is the annotation of the function
+intersected with as many negations of arrow types as it is possible
+without making the type empty. To handle this multiplicity we use and
+extend the technique of \emph{type schemes} defined
 by~\citet{Frisch2004}. Type schemes are canonical representations of
-the infinite set of types of $\lambda$-abstraction and they are
+the infinite set of types of $\lambda$-abstractions and they are
 presented in Section~\ref{sec:type-schemes}. The second origin is due
 to the presence of structural rules\footnote{In logic, logical rules
   refer to a particular connective (here, a type constructor, that is,
@@ -467,22 +470,83 @@ judgments, we present in Section~\ref{sec:typenv} an algorithm that we
 prove sound \beppe{and complete?}. All these notions are used in the
 algorithmic typing system given in Section~\ref{sec:algorules}.
 
-\begin{enumerate}
-\item type of functions -> type schemes
-
-\item elimination rules (app, proj,if) ->operations on types and how to compute them
-  
-\item not syntax directed: rules Subs, Intersect, Env.
-  
-\item Compute the environments for occurrence typing. Algorithm to compute $\Gamma\vdash\Gamma$
+\beppe{\begin{enumerate}
+ \item type of functions -> type schemes
+  \item elimination rules (app, proj,if) ->operations on types and how to compute them
+  \item not syntax directed: rules Subs, Intersect, Env.
+  \item Compute the environments for occurrence typing. Algorithm to compute $\Gamma\vdash\Gamma$
 \end{enumerate}
+}
 
-Next we can give the algorithmic typing rules
 
 \subsubsection{Type schemes}\label{sec:type-schemes}
+We introduce the new syntactic category of \emph{types schemes} which are the terms $\ts$ produced by the following grammar.
+\[
+\begin{array}{lrcl}
+  \textbf{Type schemes} & \ts & ::= & t \alt \tsfun {\arrow t t ; \cdots ; \arrow t t} \alt \ts \tstimes \ts \alt \ts \tsor \ts \alt \tsempty
+\end{array}
+\]
+type schemes denote sets of type, as formally stated by the following definition:
+\begin{definition}[Interpretation of type schemes]
+  We define the function $\tsint {\_}$ that maps type schemes into sets of types.
+  \begin{align*}
+    \begin{array}{lcl}
+    \tsint t &=& \{s\alt t \leq s\}\\
+    \tsint {\tsfunone {t_i} {s_i}_{i=1..n}} &=& \{s\alt
+    \exists s_0 = \bigwedge_{i=1..n} \arrow {t_i} {s_i}
+    \land \bigwedge_{j=1..m} \neg (\arrow {t_j'} {s_j'}).\ 
+    \Empty \not\simeq s_0 \leq s \}\\
+    \tsint {\ts_1 \tstimes \ts_2} &=& \{s\alt \exists t_1 \in \tsint {\ts_1}\ 
+    \exists t_2 \in \tsint {\ts_2}.\ \pair {t_1} {t_2} \leq s\}\\
+    \tsint {\ts_1 \tsor \ts_2} &=& \{s\alt \exists t_1 \in \tsint {\ts_1}\ 
+    \exists t_2 \in \tsint {\ts_2}.\ {t_1} \vee {t_2} \leq s\}\\
+    \tsint \tsempty &=& \varnothing
+    \end{array}
+  \end{align*}
+\end{definition}
+Note that $\tsint \ts$ is closed under subsumption and intersection
+(straightforward induction) and that $\tsempty$, which denotes the
+empty set of types is different from $\empty$ whose interpretation is
+the set of all types.
+
+\begin{lemma}
+  Let $\ts$ be a type scheme and $t$ a type. It is possible to decide the assertion $t \in \tsint \ts$,
+  which we also write $\ts \leq t$.
+\end{lemma}
+
+We can now formally define the relation $v\in t$ used in
+Section~\ref{sec:opsem} to define the dynamic semantics of
+the language. First, we associate each (possibly, not well-typed)
+value to a type schema representing the best type information about
+the value. By induction on the definition of values: $\tyof c {} =
+\basic c$, $\tyof {\lambda^{\wedge_{i\in I}s_i\to t_i} x.e}{}=
+\tsfun{s_i\to t_i}_{i\in I}$, $\tyof {(v_1,v_2)}{} = \tyof
+      {v_1}{}\tstimes\tyof {v_1}{}$. Then we have $v\in t\iffdef \tyof
+      v{}\leq t$.
+
+\beppe{Do we need the next definition and lemma here or they can go in the appendix?
+
+\begin{definition}[Representative]
+  We define a function $\tsrep {\_}$ that maps every non-empty type scheme into a type, \textit{representative} of the set of types denoted by the scheme.
+
+  \begin{align*}
+    \begin{array}{lcl}
+    \tsrep t &=& t\\
+    \tsrep {\tsfunone {t_i} {s_i}_{i\in I}} &=& \bigwedge_{i\in I} \arrow {t_i} {s_i}\\
+    \tsrep {\ts_1 \tstimes \ts_2} &=& \pair {\tsrep {\ts_1}} {\tsrep {\ts_2}}\\
+    \tsrep {\ts_1 \tsor \ts_2} &=& \tsrep {\ts_1} \vee \tsrep {\ts_2}\\
+    \tsrep \tsempty && \textit{undefined}
+    \end{array}
+  \end{align*}
+\end{definition}
+Note that $\tsrep \ts \in \tsint \ts$.
+\begin{lemma}
+  Let $\ts$ be a type scheme and $t$ a type. We can compute a type scheme, written $t \tsand \ts$, such that:
+  \[\tsint {t \tsand \ts} = \{s \alt \exists t' \in \tsint \ts.\ t \land t' \leq s \}\]
+\end{lemma}
+}
 
 
-change the definition of typeof to take into account type-schemes for lambda abstractions
 
 \subsubsection{Operators on types}\label{sec:typeops}
 

setup.sty

@@ -93,6 +93,7 @@
 \newcommand {\Cast}[2]{\tt #2\(\langle\)#1\(\rangle\)}
 \newcommand {\ifty}[4]{\ensuremath{\texttt{(}#1\in#2\texttt{)?}#3\texttt{:}#4}}
 \newcommand {\code}[1]{\texttt{\color{darkblue}#1}}
+\newcommand {\iffdef}  {\hbox{\;\;$\iff$\hspace*{-5.94mm}\raise5pt\hbox{\rm\scriptsize def}\hspace*{4mm}}}
 \newcommand {\eqdef}  {\hbox{\;\;$=$\hspace*{-2.94mm}\raise5pt\hbox{\rm\scriptsize def}\hspace*{1mm}}}
 \newcommand {\eqdeftiny}  {\hbox{\;\;$=$\hspace*{-2.55mm}\raise5pt\hbox{\rm\tiny def}\hspace*{1.5mm}}}
 \newcommand {\bpi} {\boldsymbol{\pi}}