Seminar

seminar/document.tex

@@ -10,9 +10,8 @@
 %% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - %%
 
 \usepackage[utf8]{inputenc} %% use UTF-8, maybe not needed since 2018
-\usepackage[italian,main=english]{babel} %% language
+\usepackage[main=english]{babel} %% language
 
-\usepackage{csquotes} %% correct language also for citations
 
 \usepackage[
   backend=biber,
@@ -37,15 +36,20 @@
 \usepackage{algpseudocode} %% loads algorithmicx
 \usepackage{amsthm}
 \usepackage{thmtools} %% theorems
+\usepackage{cmll}
+\usepackage{leftindex}
+\usepackage{semantic} %% semantics
+\usepackage{formal-grammar} %% BNF
+
+\usepackage{csquotes} %% correct language also for citations
 
 %% plot packages
 \usepackage{pgfplots} %% plots used with \begin{tikzpicture}
 \usepackage{tikz} %% for pictures
-\usetikzlibrary{trees}
+\usetikzlibrary{trees,chains,shadows.blur,fit,arrows.meta,positioning}
 \pgfplotsset{width=10cm,compat=newest}
 
 %% design packages
-\usepackage{enumitem} %% for lists and enumerating
 \usepackage{color}
 \usepackage{xcolor,colortbl} % xcolor for defining colors, colortbl for table colors
 \usepackage{makecell} %% for multiple lines in cell of table
@@ -74,10 +78,10 @@
 \DeclareMathOperator*{\argmax}{argmax}
 \DeclareMathOperator*{\argmin}{argmin}
 
-%% itemize use less vertical space (use olditemize for default behaviour)
+% %% itemize use less vertical space (use olditemize for default behaviour)
-\let\olditemize=\itemize%% old itemize
+% \let\olditemize=\itemize%% old itemize
-\let\endolditemize=\enditemize%% old end itemize
+% \let\endolditemize=\enditemize%% old end itemize
-\renewenvironment{itemize}{\olditemize\itemsep-0.2em}{\endolditemize}
+% \renewenvironment{itemize}{\olditemize\itemsep+0.1em}{\endolditemize}
 
 %% items in itemize emph+box
 %% usage: \ieb{Class:} for simple item
@@ -118,15 +122,17 @@
 
 %% PACKAGE tabularray
 \UseTblrLibrary{amsmath}
-
+\UseTblrLibrary{booktabs}
 
 %% PACKAGE color
 \definecolor{red}{rgb}{1, 0.1, 0.1}
 \definecolor{lightgreen}{rgb}{0.55, 0.87, 0.47}
-\definecolor{gray}{rgb}{0.3, 0.3, 0.3}
+\definecolor{gray}{rgb}{0.4, 0.4, 0.4}
+\definecolor{blue}{rgb}{0.2, 0.2, 0.675}
 \newcommand{\lgt}{\cellcolor{lightgreen}} %% light green in tables
-\newcommand{\gry}{\textcolor{gray}} %% gray text
+\newcommand{\graytext}{\textcolor{gray}} %% gray text
 \newcommand{\rd}{\textcolor{red}} %% red text
+\newcommand{\bluetext}{\textcolor{blue}} %% red text
 
 %% PACKAGE minipage
 \newcommand{\thend}[1]{\begin{center}
@@ -170,9 +176,12 @@
 
 %% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - %%
 
-\title{SEMINARIO}
+\title{SEMINAR:\\
+ A Unified View of Modalities in Types Systems}
 \author{Elvis Rossi}
 \institute[DEPARTMENT OF COMPUTER SCIENCE]{Department of Computer Science\\
+  \medskip
+  University of Pisa\\
   \medskip
   Master Degree in Computer Science
 }
@@ -193,7 +202,7 @@
   \tableofcontents
 \end{frame}
 
-\include{write_here.tex}
+\include{seminar.tex}
 
 \end{document}
 

seminar/seminar.tex

@@ -0,0 +1,631 @@
+\AtBeginSection[ ]
+{
+\begin{frame}{Outline}
+    \tableofcontents[currentsection]
+\end{frame}
+}
+
+\begin{section}{Modalities}
+  \begin{frame}{In Philosophy}
+    A modality in philosophy and formally in formal logic/type theory expresses a certain mode (or ``moment'' as in Hegel) of being.
+
+    According to Kant the four “categories” are:
+    \begin{itemize}
+    \item Quantity
+    \item Quality
+    \item Relation
+    \item Modality
+    \end{itemize}
+    and the modalities contain the three pairs of opposites:
+
+    \begin{itemize}
+    \item possibility --- impossibility
+    \item being --- nothing
+    \item necessity --- Zufälligkeit
+    \end{itemize}
+  \end{frame}
+
+  \begin{frame}{In formal logic and type theory}
+    In formal logic and type theory modalities are formalized by modal operators or closure operators
+    \#, that send propositions/types \(X\) to new propositions/types \#\(X\), satisfying some properties.
+    \hspace{1em}\\
+
+    Adding such modalities to propositional logic or similar produces what is called modal logic. Here the most famous modal operators are those meant to formalize necessity (denoted \(\Box\)) and possibility (denoted \(\lozenge\)), which together form S4 modal logic.
+    Similarly, adding modalities more generally to type theory and homotopy type theory yields modal type theory and modal homotopy type theory
+
+    %% modalities are thus qualifiers that apply to types or propositions.
+    %% the paper seeks to provide a generic framework for modalities powerful enough to be instanciated to useful specific application
+    %% and contrained enough to come with a rich meta-theory.
+  \end{frame}
+\end{section}
+
+\AtBeginSection[ ]
+{
+\begin{frame}{Outline}
+    \tableofcontents[currentsection]
+\end{frame}
+}
+
+\begin{section}{Introduction}
+  \begin{frame}{Ringoid of Modalities}
+    %% we begin by presenting the modality structure: a ring-like wich parameterises the calculus \Lambda^p
+    %% three operations are needed: addition, multiplication and meet. and two elements for the ring structure.
+    The modality structure is a ring-like structure, which parameterises the calculus \(\Lambda^p\).
+
+    It is a 6-tuple consisting of a set M, addition (+), multiplication (\(\cdot\)), meet (\(\wedge\)), element 0 and element 1.
+  \end{frame}
+
+  \begin{frame}
+    \begin{itemize}
+    \item<1-> (M, +, 0) forms a commutative monoid (associative and commutative), with 0 as identity
+    \item<2-> (M, \(\cdot\), 1) forms a monoid (associative), with 1 as identity
+    \item<3-> 0 is an absorbing element for multiplication: \( p \cdot 0 = 0 \cdot p = 0 \)
+    \item<4-> (M, \(\wedge\)) forms a semilattice: meet is associative, commutative and idempotent.
+    \item<5-> multiplication distributes over addition: \(p (q + r) = pq + pr\) and \((p+q) r = pr + qr\)
+    \item<5-> multiplication distributes over meet: \(p (q \wedge r) = pq \wedge pr\) and \((p\wedge q) r = pr \wedge qr\)
+    \item<5-> addition distributes over meet: \((p \wedge q) + r = (p + r) \wedge (q + r)\)
+    \end{itemize}
+
+    %% addition is used to combine modalities of two components of a term which are both run,
+    %% for example the function and the argument of an application.
+    %% 0 corresponds to no usage
+
+    %% multiplication arises from function composition and is the principal means
+    %% to combine modalities (qualifying a single type with several modalities);
+    %% its unit (1) corresponds to the identity function, or, more generally,
+    %% a single (non-qualified) use, like a plain variable occurrence.
+
+    %% meet can be used to match modalities between the branches of a conditional, via weakening
+  \end{frame}
+
+  \begin{frame}
+    \begin{definition}[Order]
+      \[(p \leq q) \triangleq (p = p \wedge q)\]
+    \end{definition}
+    %% This is the standard partial order arising from semi-lattices.
+
+    %% Note that addition and multiplication are monotone with respect to (⩽), as a consequence of the
+    %% corresponding distributivity.
+  \end{frame}
+
+  \begin{frame}
+    %% also a context is needed, in order to map variables to the modality expression associated
+    \begin{definition}[Modality context]
+      A modality context (or usage map) is defined as a map from variable names to modality expressions.
+      %% expressions are formed from variables, constants, sums products and meets.
+      %% all variables not specified are mapped to 0
+      %% referred by the symbols \gamma, \delta and \zeta (lowercase greek letters)
+    \end{definition}
+
+    \begin{itemize}
+    \item Every variable in the judgement \(\gamma \Gamma \vdash t : A\) is qualified by a modality.\\
+    \item \(t\) has type \(A\) with unit qualification, in context \(\gamma\Gamma\)\\
+    \item notation: \(\gamma\Gamma, x : \leftindex^{p}A \triangleq (\gamma, x \mapsto p) (\Gamma,x : A)\)
+    \end{itemize}
+  \end{frame}
+
+  \begin{frame}
+    Some properties:
+    %% addition, meet and scaling by q (multipling by q) are lifted to act pointwise on modality contexts:
+    \begin{center}
+      \begin{align*}
+        (\gamma + \delta) (x) &= \gamma(x) + \delta(x),\\
+        (\gamma \wedge \delta) (x) &= \gamma (x) \wedge \delta (x),\\
+        (q \cdot \gamma) (x) &= q \cdot \gamma (x)\\
+      \end{align*}
+    \end{center}
+
+    %% in particular modality contexts form a left module to ringoid M.
+    %% Modules are just generalisations of vector spaces where the scalar q comes from a ring rather than a field.
+  \end{frame}
+
+  \begin{frame}{Predicative Polymorphic Lambda Calculus with Modalities}
+    \(\Lambda^p\) is a functional programming language with:
+    \begin{itemize}
+    \item predicative polymorphism \(\forall \alpha. B\),
+    \item modal function types \(\leftindex^{p}A \to B\),
+    \item modal boxing \(p \langle A \rangle\),
+    \item and modality polymorphism \(\forall m.B\).
+    \end{itemize}
+
+    %% the important construct is the modal boxing operator, that forms a new type: A qualified by modality p
+
+    %% the language lacks recursion on type and term level, but Church encoding can be used represent some inductive data types.
+    %% But we have that it is total and strongly normalising, meaning that it can be used as a consistent logic.
+  \end{frame}
+
+  \begin{frame}{Types}
+    \begin{definition}
+      Types \(A, B, C \in \texttt{Ty}\) are given by the following grammar:
+      \begin{center}
+        \begin{grammar}
+          \firstcase{\text{A,B,C}}{K \gralt{} 1 \gralt{} \alpha}{}
+          \otherform{\forall{} \alpha.A \gralt{} \forall{} m.A}{}
+          \otherform{\vphantom{a}^{p}A \to{} B \gralt{} A + B}{}
+          \otherform{A \times{} B \gralt{} p \langle{} A \rangle{}}{}
+        \end{grammar}
+      \end{center}
+    \end{definition}
+    %% K ranges over a set TyConst of uninterpreted base types, to add to 1, +, \times, \to and p\langle_\rangle
+    %% Boolean type can, for example be encoded as Bool = 1 + 1
+
+    Let Ty\(_0\) denote the set of monomorphic types (monotypes).\\
+    %% types free of polymorphism (dont contain sub-expressions of the form \forall \alpha.B)
+    If \(\alpha\) is restricted to only monotypes, \(\Lambda^p\) becomes predicative.\\
+    %% in particular B[A/\alpha] < \forall \alpha.B is well-founded (where A is a monotype)
+    Let Ty\(_0^0\) denote the set of closed monotypes.
+    %% types that neither contain type quantification nor type variables.
+  \end{frame}
+
+  \begin{frame}
+    %% the key idea is to that modalities operate multiplicatly with respect to the context, and additively over each other.
+    \begin{itemize}
+    \item If \(\gamma \Gamma \vdash A\) then \(p \gamma \Gamma\) is needed to produce \(p \langle A \rangle\).
+    \item If \(\gamma \Gamma \vdash A\) and \(\delta \Gamma \vdash B\), then \((\gamma + \delta)\Gamma\) is needed to produce both \(A\) and \(B\).
+    \end{itemize}
+  \end{frame}
+
+  \begin{frame}
+    %% lets see how functions are encoded:
+    \[\leftindex^{p}A \to B\]
+    %% is the domain of function types quantified with an arbitrary modality expression p.
+    %% ommitted modality implicitly stands for 1
+    \pause\[\leftindex^{1}A \to B\quad = \quad A \to B\quad = \quad A \multimap B\]
+
+    %% we can also apply a modality directly to a type
+    \pause\[\leftindex^{p}A \to B\quad = \quad p\langle A\rangle \to B\]
+    %% both are typing rules for pedagogical purpuses
+  \end{frame}
+
+  \begin{frame}
+    In a language with generalised algebraic data types, \(p\langle A \rangle \)
+    would be defined instead as a data type with constructor of type \[\leftindex^{p}A \to p \langle A \rangle \]
+  \end{frame}
+
+  \begin{frame}\frametitle{Typing rules for \(\Lambda^p\)}
+    %% lets see now how we evaluate the types of the language:
+
+    %% from simply typed lambda calculus rules
+    %% note that in the variable since A is used only once, it is decorated with modality one
+    %% and the rest of the context is not used.
+
+    %% the abstraction rule simply carries the information of the modality
+    \fboxsep=0pt
+    \noindent
+    \begin{minipage}[t]{0.40\linewidth}
+      \begin{center}
+        \bluetext{System F}\\
+        \bluetext{({\it from lambda calculus\/})}
+      \end{center}
+      \footnotesize{
+        \inference[VAR]
+        {}
+        {\Gamma, \graytext{x:}\ A |- \graytext{x:}\ A} % chktex 1
+        \vspace{2em}
+        \inference[ABS]
+        {\Gamma, \graytext{x:}\ A |- \graytext{t:}\ B} % chktex 1
+        {\Gamma |- \lambda x.t: A -> B} % chktex 1
+        \vspace{2em}
+        \inference[APP]
+        {\Gamma |- \graytext{t:}\ A -> B \quad \Gamma |- \graytext{u:}\ A} % chktex 1
+        {\Gamma |- \graytext{t\ u:}\ B} % chktex 1
+      }
+    \end{minipage}
+    \hfill
+    \begin{minipage}[t]{0.55\linewidth}
+      \begin{center}
+        \bluetext{\(\Lambda^p\)}\\
+        \phantom{\bluetext{({\it from lambda calculus\/})}}
+      \end{center}
+      \footnotesize{
+        \inference[VAR]
+        {}
+        {\rd{0}\Gamma, \graytext{x:} \leftindex^{\rd{1}}A |- \graytext{x:}\ A} % chktex 1
+        \vspace{1.9em}
+        \inference[ABS]
+        {\rd{\gamma}\Gamma, \graytext{x:}\leftindex^{\rd{q}} A |- \graytext{t:}\ B} % chktex 1
+        {\rd{\gamma}\Gamma |- \graytext{\lambda \leftindex^{\rd{q}}x.t:} \leftindex^{\rd{q}}A -> B} % chktex 1
+        \vspace{1.5em}
+        \inference[APP]
+        {\rd{\gamma}\Gamma |- \graytext{t:} \leftindex^{\rd{q}} A -> B \quad \rd{\delta} \Gamma |- \graytext{u:}\ A} % chktex 1
+        {\rd{(\gamma + q \delta)}\Gamma |- \graytext{t \leftindex^{\rd{q}} u:}\ B} % chktex 1
+      }
+    \end{minipage}
+  \end{frame}
+
+  \begin{frame}
+    %% here the rules that differentiate System F from simply typed lambda calculus: abstraction and application.
+    %% again the modality is simply carried over.
+    \fboxsep=0pt
+    \noindent
+    \begin{minipage}[t]{0.40\linewidth}
+      \begin{center}
+        \bluetext{System F}
+      \end{center}
+      \small{
+        \inference[T-ABS]
+        {(\Gamma, \alpha) |- \graytext{t:}\ B} % chktex 1
+        {\Gamma |- \graytext{\Lambda \alpha.t:}\ \forall \alpha.B} % chktex 1
+        \vspace{2em}
+        \inference[T-APP]
+        {\Gamma |- \graytext{t:}\ \forall \alpha. B \quad \Gamma |- A} % chktex 1
+        {\Gamma |- \graytext{t \cdot A:}\ B[A/\alpha]} % chktex 1
+      }
+    \end{minipage}
+    \hfill
+    \begin{minipage}[t]{0.55\linewidth}
+      \begin{center}
+        \bluetext{\(\Lambda^p\)}
+      \end{center}
+      \small{
+        \inference[T-ABS]
+        {\rd{\gamma} (\Gamma, \alpha) |- \graytext{t:}\ B} % chktex 1
+        {\rd{\gamma}\Gamma |- \graytext{\Lambda \alpha.t:}\ \forall \alpha. B} % chktex 1
+        \vspace{2em}
+        \inference[T-APP]
+        {\rd{\gamma}\Gamma |- \graytext{t:}\ \forall \alpha. B \quad \Gamma |- A} % chktex 1
+        {\rd{\gamma}\Gamma |- \graytext{t\cdot A:}\ B[A/\alpha]} % chktex 1
+      }
+    \end{minipage}
+  \end{frame}
+
+  \begin{frame}
+    %% the introduction rule simply works by multiplying p
+    %% the elimination rule is more involved: first gamma produces p A, but to use A to produce C, we might need more than p, so we allow for an additional arbitrary multiplication by q
+    %% to give more flexibility to the grammar
+
+    \begin{center}
+      \bluetext{\(\Lambda^p\)}
+    \end{center}
+    \inference[p\(\langle\cdot\rangle\)-INTRO]
+    {\gamma \Gamma |- \graytext{t:} A} % chktex 1
+    {p\gamma\Gamma |- \graytext{[\leftindex^{p}t]:} p \langle A \rangle} % chktex 1
+
+    \vspace{2em}
+    \inference[p\(\langle\cdot\rangle\)-ELIM]
+    {\gamma\Gamma |- \graytext{u:} p\langle A \rangle \quad \delta \Gamma\graytext{, x:} \leftindex^{qp}A |- \graytext{t:} C} % chktex 1
+    {(q\gamma + \delta)\Gamma |-\graytext{\texttt{let} [\leftindex^{p}x] = \leftindex^{q} u \texttt{ in } t:} C} % chktex 1
+  \end{frame}
+
+  \begin{frame}
+    %% we note that every variable occurrence corresponds to usage 1. This ensures stability of usage under variable substitution. Other rules make modalities match.
+    %% for example abstraction introduces a variable with modality q and application multiplies the usage of the argument by q
+    \begin{center}
+      \hspace{-1em}\inference[WK]
+      {\delta \Gamma |- \graytext{t:} A \quad \gamma \leq \delta} % chktex 1
+      {\gamma\Gamma |- \graytext{t:} A} % chktex 1
+    \end{center}
+
+    \begin{theorem}[Convertibility]
+      If \(p \leq q\), then there is a term of type \(\leftindex^{p}A \to q \langle A \rangle \) for any \(A\).
+    \end{theorem}
+
+    %% it is allowed to use weakening: one can always use a variable in a more specific modality.
+    %% there is always convertibility in this direction
+
+    %% finally the existence of meet ensures compositionality for case branches.
+    %% that is if there are different branches, one can always find a single modality context such that it is smaller or equal than all the branches.
+  \end{frame}
+\end{section}
+
+\AtBeginSection[ ]
+{
+\begin{frame}{Outline}
+    \tableofcontents[currentsection]
+\end{frame}
+}
+
+\begin{section}{Applications}
+  \begin{frame}
+    %% While the origin of the discovery of this new logic comes from a semantical analysis of the models of System F (or polymorphic λ-calculus),
+    %% one can see the whole system of linear logic as a bold attempt to reconcile the beauty and symmetry of classical logic afforded by De Morgan's dualities
+    %% with the quest for constructive proofs that had led to intuitionistic logic.
+
+    Consider the three basic structural properties satisfied by simply-typed lambda calculus:
+
+    \begin{definition}[Exchange]
+      Exchange indicates that the order in which we write down variables in the context is irrelevant:
+
+      \begin{center}
+        \begin{tikzpicture}[node/.style = {draw,rounded corners,blur shadow, fill=white,align=center}]
+          \node[node] at (0.2,0) (if) {If\quad \(\Gamma_1, x_1 : T_1, x_2: T_2, \Gamma_2 \vdash t : T\)};
+          \node[node] at (0,-1.5) (then) {then\quad \(\Gamma_1, x_2 : T_2, x_1: T_1, \Gamma_2 \vdash t : T\)};
+
+          \draw[-{Stealth[length=2mm]}] (-0.78,-0.3) -- (0.54,-1.2);
+          \draw[-{Stealth[length=2mm]}] (0.54,-0.3) -- (-0.78,-1.2);
+        \end{tikzpicture}
+      \end{center}
+    \end{definition}
+
+  \end{frame}
+
+  \begin{frame}
+    \begin{definition}[Weakening]
+      Weakening indicates that adding extra unneeded assumptions to the context does not prevent a term from type checking:
+
+      \begin{center}
+        \begin{tikzpicture}[node/.style = {draw,rounded corners,blur shadow, fill=white,align=center}]
+          \node[node] at (-0.1,0) (if) {If\hspace{2.5em} \(\Gamma_1, \Gamma_2 \vdash t : T\)};
+          \node[node] at (0,-0.85) (then) {then\hspace{1em} \(\Gamma_1, x_1 : T_1, \Gamma_2 \vdash t : T\)};
+        \end{tikzpicture}
+      \end{center}
+    \end{definition}
+  \end{frame}
+
+  \begin{frame}
+    \begin{definition}[Contraction]
+      Contraction states that if we can type check a term using two identical assumptions (\(x_2:T_1\) and \(x_3:T_1\)) then we can check the same term using a single assumption:
+
+      \begin{center}
+        \begin{tikzpicture}[node/.style = {draw,rounded corners,blur shadow, fill=white,align=center}]
+          \node[node] at (-0.1,0) (if) {If\hspace{2.5em} \(\Gamma_1, x_2 : T_1, x_3 : T_1,\Gamma_2 \vdash t : T_2\)};
+          \node[node] at (0,-0.85) (then) {then\hspace{1em} \(\Gamma_1, x_1:T_1, \Gamma_2 \vdash [x_2 \mapsto x_1][x_3 \mapsto x_1] t : T_2\)};
+        \end{tikzpicture}
+      \end{center}
+    \end{definition}
+  \end{frame}
+
+  \begin{frame}
+    We thus have different types systems if we allow different rules to be applied:
+
+    \begin{itemize}
+    \item \bluetext{{\it Linear\/} type systems ensure that every variable is used exactly once (E)}.
+
+    \item {\it Affine\/} type systems ensure that every variable is used at most once (E, W).
+
+    \item {\it Relevant\/} type systems ensure that every variable is used at least once (E, C).
+
+    \item {\it Ordered\/} type systems ensure that every variable is used exactly once and in the order which it is introduced (none).
+    \end{itemize}
+  \end{frame}
+
+  \begin{frame}
+    %% omega, or also called \mathbb{N}, is the extremum of the meet-lattice.
+    %% variables associated with this modality can be used in unrestricted fashion.
+    \begin{center}
+      \begin{tikzpicture}[
+        node/.style = {draw,rounded corners,blur shadow,fill=white,align=center},
+        nodeh/.style = {},
+        nodegroup/.style = {draw,rounded corners,align=center}
+        ]
+        \onslide<1->{
+          \node[node] at (0,1.5) (linear) {linear (E)};
+          \node[node] at (-2,3) (affine) {affine (E, W)};
+          \node[node] at (2,3) (relevant) {relevant (E, C)};
+        }
+        \onslide<1>{
+          \node[node] at (0,0) (ordered) {ordered (none)};
+          \node[node] at (0,4.5) (unrestricted) {unrestricted (E, W, C)};
+        }
+
+        \onslide<1>{
+          \draw[-] (ordered) -- (linear);
+          \draw[-] (relevant) -- (unrestricted);
+          \draw[-] (affine) -- (unrestricted);
+        }
+
+        \onslide<1->{
+          \draw[-] (linear) -- (affine);
+          \draw[-] (linear) -- (relevant);
+        }
+
+        \onslide<2->{
+          \begin{scope}[node distance=0.3cm]
+            \node[nodeh] at (0,-0.2) (linearw) {\(\omega\)};
+            \node[nodeh] (linear0) [above left=of linearw] {0};
+            \node[nodeh] (linear1) [above right=of linearw] {1};
+            \draw[-] (linearw) -- (linear0);
+            \draw[-] (linearw) -- (linear1);
+          \end{scope}
+          \node[nodegroup,fit=(linearw)(linear0)(linear1)] (grouplinear) {};
+          \draw[-] (linear) -- (grouplinear);
+
+          \begin{scope}[node distance=0.3cm]
+            \node[nodeh] at (4,4) (linearw) {\(\omega\)};
+            \node[nodeh] (linear0) [above left=of linearw] {0};
+            \node[nodeh] (linear1p) [above right=of linearw] {\(1^{+}\)};
+            \draw[-] (linearw) -- (linear0);
+            \draw[-] (linearw) -- (linear1p);
+          \end{scope}
+          \node[nodegroup,fit=(linearw)(linear0)(linear1p)] (grouprelevant) {};
+          \draw[-] (relevant) -- (grouprelevant);
+
+          \begin{scope}[node distance=0.3cm]
+            \node[nodeh] at (-4,4) (linearw) {\(\omega\)};
+            \node[nodeh] (linearat) [above=of linearw] {@};
+            \node[nodeh] (linear0) [above=of linearat] {0};
+            \node[nodeh] (linear1) [right=of linearat] {\hspace{-0.9em}\(= 1\)};
+
+            \draw[-] (linearw) -- (linearat);
+            \draw[-] (linearat) -- (linear0);
+          \end{scope}
+          \node[nodegroup,fit=(linearw)(linearat)(linear0)(linear1)] (groupaffine) {};
+          \draw[-] (affine) -- (groupaffine);
+        }
+
+        \onslide<3->{
+          \begin{scope}[node distance=0.3cm]
+            \node[nodeh] at (-3,0) (linearw) {\(\omega\)};
+            \node[nodeh] (linearat) [above=of linearw] {@};
+            \node[nodeh] (linear1p) [right=of linearat] {\(1^{+}\)};
+            \node[nodeh] (linear1) [above=of linear1p] {1};
+            \node[nodeh] (linear0) [above left=of linearat] {0};
+            \draw[-] (linearw) -- (linear1p);
+            \draw[-] (linearw) -- (linearat);
+            \draw[-] (linearat) -- (linear0);
+            \draw[-] (linearat) -- (linear1);
+            \draw[-] (linear1p) -- (linear1);
+          \end{scope}
+          \node[
+          label={[label distance=0cm]-90:{\it combined}},
+          nodegroup,fit=(linearw)(linearat)(linear1p)(linear1)(linear0)] (groupcombined) {};
+        }
+      \end{tikzpicture}
+    \end{center}
+
+    %% It might be possible to define type systems containing other combinations
+    %% of structural properties, such as contraction only or weakening only,
+    %% but so far researchers have not found applications for such combinations.
+    %% Consequently, we have excluded them from the diagram.
+  \end{frame}
+
+  \begin{frame}\frametitle{Linear Types}
+    \vspace{1.5em}
+
+    Indeed the unit modality precisely corresponds to linear usages.
+
+    A 0-qualified function is necessarily constant ({\it irrelevance\/}).
+
+    \(\omega\) represents non-linear usage, equivalent to the more traditional exclamation mark (!).
+
+    \begin{tikzpicture}[
+      remember picture,overlay,
+      node/.style = {draw,rounded corners,blur shadow,fill=white,align=center},
+      nodeh/.style = {},
+      nodegroup/.style = {draw,rounded corners,align=center}
+      ]
+      \begin{scope}[node distance=0.3cm]
+        \node[nodeh,xshift=-3cm,yshift=-3.5cm] at (current page.north east) (linearw) {\(\omega\)};
+        \node[nodeh] (linear0) [above left=of linearw] {0};
+        \node[nodeh] (linear1) [above right=of linearw] {1};
+        \draw[-] (linearw) -- (linear0);
+        \draw[-] (linearw) -- (linear1);
+      \end{scope}
+      \node[nodegroup,fit=(linearw)(linear0)(linear1)] (grouplinear) {};
+    \end{tikzpicture}
+  \end{frame}
+
+
+  \begin{frame}\frametitle{Linear Type System}
+    \begin{center}
+      \begin{grammar}
+        \firstcase{A}{p \gralt{} p^{\bot}}{}
+        \otherform{A \otimes{} A \gralt{} A \oplus{} A}{}
+        \otherform{A \& A \gralt{} A \parr{} A}{}
+        \otherform{1 \gralt{} 0 \gralt{} \top{} \gralt{} \bot{}}{}
+        \otherform{!A \gralt{}?A}{}
+      \end{grammar}
+    \end{center}
+    %% where p are logical atoms
+
+    %% in particular we are intereseted in the exponentials: ! and ?, which limit access to weakening and contraction.
+    %% while in intuitionistic and constructive logic, the formula A \impl B can be interpreted as "if you give me an A, i will give you a B", in linear logic it means "give me as many A's as I might need and I will give you one B".
+    %% Encoding the notion of copy into the logic.
+
+    %% This duplication of the connectives actually leads to a much clearer understanding of the conflict between classical and intuitionistic logic.
+    %% For example, the law of excluded middle (A or not-A) is considered valid in the classical world and absurd in the intuitionistic one.
+    %% But in linear logic, this law has two readings: the additive version (A \oplus ¬A) is not provable and corresponds to the intuitionistic reading of disjunction;
+    %% the multiplicative version (A \parr \neg A) is trivially provable and simply corresponds to the tautology (A \implies A)
+    %% that is perfectly acceptable in intuitionistic logic too.
+  \end{frame}
+
+  \begin{frame}
+    %% the exponential ! (of course) permits contraction and weakening on the left sequent context, while the exponential ? (why not) permits contraction and weakening on the right hand sequent context.
+    The intuitionistic implication \(B \implies C \) can be defined as \( ! B \multimap C \)
+
+    Where \[ B \multimap A \triangleq B^\bot \parr C \]
+  \end{frame}
+
+  \begin{frame}
+    %% we must not forget the other two operations: addition and multiplication, but they follow an easily computable rules:
+
+    Finally the rules for \(\cdot\) and +:
+
+    \begin{center}
+      \begin{tblr}{c|ccccc}
+        (+) & 0 & \(\omega\) & @ & 1 & \(1^{+}\)\\
+        \midrule
+        0 & 0 & \(\omega\) & @ & 1 & \(1^{+}\) \\
+        \(\omega\) & \(\omega\) & \(\omega\) & \(\omega\) & \(1^{+}\) & \(1^{+}\) \\
+        @ & @ & \(\omega\) & \(\omega\) & \(1^{+}\) & \(1^{+}\) \\
+        1 & 1 & \(1^{+}\) & \(1^{+}\) & \(1^{+}\) & \(1^{+}\) \\
+        \(1^{+}\) & \(1^{+}\) & \(1^{+}\) & \(1^{+}\) & \(1^{+}\) & \(1^{+}\) \\
+      \end{tblr}\hspace{0.1em}
+      \begin{tblr}{c|ccccc}
+        \((\cdot)\) & 0 & \(\omega\) & @ & 1 & \(1^{+}\)\\
+        \midrule
+        0 & 0 & 0 & 0 & 0 & 0 \\
+        \(\omega\) & 0 & \(\omega\) & \(\omega\) & \(\omega\) & \(\omega\) \\
+        @ & 0 & \(\omega\) & @ & @ & \(\omega\) \\
+        1 & 0 & \(\omega\) & @ & 1 & \(1^{+}\) \\
+        \(1^{+}\) & 0 & \(\omega\) & \(\omega\) & \(1^{+}\) & \(1^{+}\) \\
+      \end{tblr}
+    \end{center}
+  \end{frame}
+
+  \begin{frame}\frametitle{Quantitative Typing}
+    A generalisation of all the above systems in what can be called quantitative typing, with one modality for each set of accepted usage.
+
+    %% modalities are interpreted as a sets of natural numbers.
+    %% An element in such a set is an admissible number of times that a variable can be used.
+
+    Where the set of all modalities Mod \(= 2^{\mathbb{N}}\), with \(0 = \{0\}, 1 = \{1\}\) and:
+    \begin{align*}
+      p+q &= \{x+y | x \in p, y \in q\}\\
+      p\cdot q &= \{x \cdot y | x \in p, y \in q\}\\
+      p \land q &= p \cup q
+    \end{align*} %% Minkovski operations
+
+    Every acceptable set of usage is tracked.
+    %% unfortunately even in their simplest form modality expressions for this structure can be too large.
+  \end{frame}
+
+  \begin{frame}\frametitle{Sensitivity Analysis for Differential Privacy}
+    In differential privacy one is interested in publishing statistically anonymised data without revealing individual secrets.
+
+    The role of the type system is to ensure that if a certain amount of noise is introduced in the inputs of a program, then at least the same amount is present in the outputs.
+  \end{frame}
+
+  \begin{frame}
+    In the literature every type \(A\) is equipped with a metric \(d_A : A \times A \to \mathbb{R}^{\infty}_{\geq 0}\).
+
+    \(f:A \to B\) is \(c\)-sensitive if it does not increase distances by a factor greater than \(c\):
+
+    \[d_B (f(x),f(y)) \leq_{\mathbb{R}} c \cdot d_A (x, y) \]
+    %% 0 means equality on all types \implies 0-sensitive functions are necessarily constant.
+    %% \infty-sensitive functions impose no restrictions on the argument.
+  \end{frame}
+
+  \begin{frame}
+    To translate the model into the proposed framework, let the modality carrier set be \(\mathbb{R}_{\geq 0}^{\infty}\); let \(\land\) be the max operator.\vspace{2em}
+
+    \bluetext{Note:} the order on the lattice is opposite to the order on \(\mathbb{R}\): \((\leq) = (\geq_{\mathbb{R}})\).
+  \end{frame}
+
+  \begin{frame}
+    In the literature there is a need to prove that evaluation preserve sensitivity, in this framework no special preservation proof is needed: any system is type-preserving for any modality ringoid, thus any assignment of types to metrics will do.
+  \end{frame}
+
+  \begin{frame}\frametitle{Information-Flow Security}
+    %% finally an application where it does not matter how many times variables are used, but rather in which context.
+    One application of type systems is to ensure that certain parts of a program do not have access to private (high security) information.\vspace{1em}
+
+    The principal property of such systems is that the output of a program does not depend on secret inputs.\vspace{1em}
+
+    This property holds for \(\Lambda^p\), if we consider that any modality \(p\) above 1 in the lattice is secret.
+    %% The simplest security lattice has a single secret level H (high) which can be represented by 0 and a single public level L (low) represented by 1
+  \end{frame}
+
+  \begin{frame}
+    \bluetext{Note:} The addition is relegated to play the same role as the meet: \((+) = (\land)\).
+
+    If we need a variable in two parts of a term, we mus assume the worst and require the most public level given by the meet.\vspace{1em}
+
+    \bluetext{Note:} The multiplication acts as the join (\(\lor\)) of the lattice (dual to the meet).
+
+    \begin{center}
+      \phantom{}
+      \inference[]
+      {|- t: \leftindex^{p}A -> B & x:  \leftindex^{q}X |- u: A}
+      {x: \leftindex^{p\lor{} q} X |- t \leftindex^{p} u: B}
+    \end{center}
+
+    %% Supporting security features via generic abstraction features of type systems have been proposed
+    %% before, but so far this has been done via quantification over types
+  \end{frame}
+\end{section}
+
+%%% Local Variables:
+%%% TeX-command-extra-options: "-shell-escape"
+%%% TeX-master: "document.tex"
+%%% End:

seminar/write_here.tex

@@ -1,13 +0,0 @@
-\begin{section}{First Section}
-  \begin{frame}\frametitle{Title}
-    \begin{itemize}
-    \item first item
-    \item second item
-    \end{itemize}
-  \end{frame}
-\end{section}
-
-%%% Local Variables:
-%%% TeX-command-extra-options: "-shell-escape"
-%%% TeX-master: "document.tex"
-%%% End: