Commit 1de33dd9 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Slides premier jet

parent d09a0f41
*~
#*
*.backup
*.aux
*.bbl
*.blg
*.log
*.out
*.idx
*.nav
*.nlo
*.snm
*.toc
*.vtc
*.synctex.gz
*.cut
*.vrb
*.pdf
\documentclass{beamer}
\usetheme{Warsaw}
\setbeamertemplate{navigation symbols}{%
%\insertslidenavigationsymbol
%\insertframenavigationsymbol
%\insertsubsectionnavigationsymbol
%\insertsectionnavigationsymbol
%\insertdocnavigationsymbol
%\insertbackfindforwardnavigationsymbol
}
\usepackage[T1]{fontenc} %Permet d'imprimer les caractères spéciaux
\usepackage[utf8]{inputenc} %Permet de taper directement les caractères spéciaux dans le fichier Tex
\usepackage{amsthm} %Permet de définir les différents types de théorèmes, remarques...
\usepackage{amssymb} %Ajoute \mathbb
\usepackage{mathrsfs} %Ajoute la commande \mathscr
\usepackage{amsmath} %Environnement align*, commande \text et définitions des mathOperator
\usepackage{stmaryrd} %Ajoute \llbracket
\usepackage{xcolor} %Pour mettre de la couleur
\usepackage[normalem]{ulem} %Pour souligner, hachurer...
\usepackage{hyperref}%Création d'une table des matières avec des hyperliens
\hypersetup{% parametrage des hyperliens
colorlinks=true,% colorise les liens
breaklinks=true,% permet les retours à la ligne pour les liens trop longs
urlcolor= black,% couleur des hyperliens
linkcolor= black,% couleur des liens internes aux documents (index, figures, tableaux, equations,...)
citecolor= black% couleur des liens vers les references bibliographiques
}
\usepackage[toc,page]{appendix} % Pour gérer les annexes
\bibliographystyle{apalike} % Type de bibliographie
\usepackage{multirow}
\usepackage{listings}
\usepackage{bussproofs}
\usepackage{color}
\usepackage{tikz}
\setbeamertemplate{headline}{}
\setbeamertemplate{footline}{
\leavevmode%
\hbox{\hspace*{-0.1cm}
\begin{beamercolorbox}[wd=.5\paperwidth,ht=2.25ex,dp=1ex,right]{title in head/foot}%
\usebeamerfont{title in head/foot} \insertshorttitle\hspace{1mm}
\end{beamercolorbox}%
\hspace*{-0.1cm}
\begin{beamercolorbox}[wd=.31\paperwidth,ht=2.25ex,dp=1ex,left]{author in head/foot}%
\usebeamerfont{author in head/foot}\hspace{1mm}\insertshortauthor%~~(\insertshortinstitute)
\end{beamercolorbox}%
\hspace*{-0.1cm}
\begin{beamercolorbox}[wd=.21\paperwidth,ht=2.25ex,dp=1ex,right]{author in head/foot}%
\usebeamerfont{author in head/foot}
\insertframenumber{} / \inserttotalframenumber\hspace{0.5cm}
\end{beamercolorbox}}%
\vskip0pt%
}
\lstset{basicstyle={\ttfamily\small},keywordstyle={\color{blue}}}
\lstdefinelanguage{Dedukti}
{
alsoletter={=->:\#},
keywords={Type,def,-->,->,=>,:=,:,.,\#SNF,\#NAME,\#PRINT},
delim=[s][\color{brown}]{\[}{\]},
comment=[n]{(;}{;)},
string=[b]{"},
stringstyle=\color{orange},
commentstyle=\color{red},
showstringspaces=false,
}
\lstset{language=Dedukti}
\title[Dependency Pairs in Dependent Type Theory]{Dependency Pairs in Dependent Type Theory with Rewriting}
\titlegraphic{
\includegraphics[width=1.3cm]{../../Bureau/Utiles/Logos/LSV.png}\hspace{1cm}
\includegraphics[width=1.8cm]{../../Bureau/Utiles/Logos/ENSPS.png}\hspace{1cm}
\includegraphics[width=2cm]{../../Bureau/Utiles/Logos/Inria.png}\hspace{0.9cm}
\includegraphics[width=1.7cm]{../../Bureau/Utiles/Logos/Mines.png}
}
\author[Guillaume Genestier]{Guillaume Genestier\\\color{gray}{Joint work with Fr\'ed\'eric Blanqui and Olivier Hermant}}
\date{Thursday, June 27, 2019}
\usepackage{marvosym}
\usepackage{mathdots}
\usepackage{array}
\usepackage{tikz}
\usetikzlibrary{arrows,shapes,decorations.pathmorphing,backgrounds,positioning,fit,calc}
\definecolor{noir}{RGB}{0,0,0}
\definecolor{gris}{RGB}{150,150,150}
\definecolor{grispale}{RGB}{240,240,240}
\definecolor{vertfonce}{RGB}{0,130,0}
\definecolor{bleufonce}{RGB}{0,0,130}
\definecolor{blue-violet}{rgb}{0.54, 0.17, 0.89}
\newcommand{\bto}{{\color{blue}{\to}}}
\newcommand{\interp}[1]{\left\llbracket#1\right\rrbracket}
\newcommand{\tool}[1]{\sc{#1}}
\newcommand{\Dedukti}{\tool{Dedukti}}
\newcommand{\SCT}{\tool{SizeChangeTool}}
\lstset{escapeinside={@}{@}}
\AtBeginSection[]{
\begin{frame}
\frametitle{Contents}
\tableofcontents[currentsection,hideothersubsections]
\end{frame}
}
\begin{document}
\frame{\titlepage}
\begin{frame}\frametitle{Contents}
\tableofcontents[hidesubsections]
\end{frame}
\section{Context: \Dedukti{}}
\begin{frame}[fragile]\frametitle{\emph{Dedukti}}
\emph{Dedukti} is a type-checker for the $\lambda\Pi$-calculus modulo rewriting.
\begin{block}{Example of dependent type}
\begin{lstlisting}
def F : Nat -> TYPE
[] F 0 --> Nat
[n] F (s n) --> Nat -> F n
\end{lstlisting}
{\tt F n} = {\tt Nat $\to$ Nat $\to \dots\to$ Nat} with {\tt n} arrows.
\end{block}
\begin{block}{Example of rewriting rules}
\begin{lstlisting}[mathescape=true]
def sum : (n: Nat) -> F n
[] sum 0 --> 0
[] sum (s 0) --> $\lambda$x, x
[n] sum (s (s n)) --> $\lambda$x y, sum (s n) (plus x y)
\end{lstlisting}
\emph{Example} : {\texttt sum 5 1 2 3 4 5 $\longrightarrow^*$ 1+2+3+4+5 $\longrightarrow^*$ 15}
\end{block}
\end{frame}
\begin{frame}
\frametitle{\emph{Dedukti} is well-suited for interoperability}
\begin{center}
\begin{tikzpicture}
[node distance=3cm,
on grid,
checker/.style = {shape=ellipse, draw=blue-violet!100, fill=blue-violet!25, align=center,
minimum height=1.2cm, minimum width=2cm},
dedukti node/.style = {shape=ellipse, draw=blue-violet!90, fill=blue-violet!50, label={south:Dedukti}},
post/.style={->, >=stealth', semithick}]
\node [checker, fill=blue-violet!75, label={north:D[HOL]}] (DHOL) {};
\node [checker, left=of DHOL, fill=blue-violet!75, label={north:D[Matita]}] (DMatita) {};
\begin{scope}[on background layer]
\node [dedukti node, inner sep=7pt, fit={(DMatita) (DHOL)}] (Dedukti) {};
\end{scope}
\node [draw=none] (Coq) [above=of Dedukti] {};
\node [checker, label={north:HOL}] (HOL) [right=of Coq, yshift=-1cm] {};
\node [checker, label={north:Matita}] (Matita) [left=of Coq, yshift=-1cm] {};
\draw[circle,fill=violet!50] (Matita.center) circle (0.25) {};
\draw[post, very thick, ->, orange] ([yshift=-0.25cm]Matita.center)
.. controls ([yshift=-0cm,xshift=-3cm]Dedukti)
.. (DMatita);
\draw[post, very thick, <-, orange] (HOL)
.. controls ([yshift=-0cm,xshift=3cm]Dedukti)
.. (DHOL);
\draw[very thick, orange, dashed, ->] (DMatita) .. controls ([xshift=-0.5cm,yshift=0.5cm]Dedukti) and ([xshift=0.5cm,yshift=0.5cm]Dedukti) .. (DHOL);
\end{tikzpicture}
\end{center}
\end{frame}
\begin{frame}{Non-restrictive Rewriting}
\begin{itemize}\itemsep=3mm
\item LHS can overlap:\hfill$x+0\bto x$, $0+x\bto x$
\item LHS can be non-linear:\hfill$x-x\bto 0$
\item LHS can contain defined symbols:\hfill$(x+y)+z\bto x+(y+z)$
\item LHS can contain abstractions:\hfill$lam\,(\lambda x.app\,F\,x)\bto F$
\item matching modulo $\beta$:\hfill
$\partial\,(\lambda x. ln\,(F\,x))\bto\lambda x.( \partial\,F\,x ) / (F\,x )$
\item rules can be both at the object and type levels
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Expected properties of rewriting}
\begin{itemize}
\item Termination: There is no infinite sequence of reduction starting from a well-typed term;
\hfill
\begin{tikzpicture}
\node (one) at (0,0) {};
\node (two) at (1.2,0) {};
\node (three) at (1.8,-0.6) {};
\node (four) at (1.2,-1.2) {};
\node (five) at (0,-1.2) {};
\node (six) at (-0.6,-0.6) {};
\draw[->] (one) to (two);
\draw[->] (two) to (three);
\draw[->] (three) to (four);
\draw[->] (four) to (five);
\draw[->] (five) to (six);
\draw[->] (six) to (one);
\draw[color=red] (-0.8,0.2) to (2,-1.4);
\draw[color=red] (-0.8,-1.4) to (2,0.2);
\end{tikzpicture}
\item Typing preservation (\emph{Subject reduction}) : If a term is well-typed, its reducts have the same type;
\item Confluence: Two reducts of a term have a comon reduct.
\hfill
\begin{tikzpicture}
\node (tl) at (0,0) {};
\node (bl) at (0,-1.5) {};
\node (tr) at (1.5,0) {};
\node (br) at (1.5,-1.5) {};
\draw[->>] (tl) to (tr);
\draw[->>] (tl) to (bl);
\draw[dotted,->>] (tr) to (br);
\draw[dotted,->>] (bl) to (br);
\end{tikzpicture}
\end{itemize}
\end{frame}
\begin{frame}{Termination: difficulties}
\begin{itemize}\itemsep=5mm
\item the set of terms $\lambda\Pi/\mathcal{R}$ depends on rewriting rules $\mathcal{R}$,
\item higher-order rules cannot be dealt with
independently of $\beta$-reduction,
\item type-level rewriting forbids the use of erasing tricks
reducing termination to simply-typed $\lambda$-calculus,
\item type-level rewriting allows to encode any functional pure type
system (e.g. system F or the calculus of constructions).
\end{itemize}
\end{frame}
\newcommand{\bType}{\textcolor{blue}{\mathrm{Type}}}
\newcommand{\bKind}{\textcolor{blue}{\mathrm{Kind}}}
\newcommand{\bs}{\textcolor{blue}{s}}
\newcommand{\rA}{\textcolor{red}{A}}
\newcommand{\rB}{\textcolor{red}{B}}
\newcommand{\subst}[3]{#1\crochet{\sur{#3}{#2}}}
\newcommand{\sur}[2]{\raisebox{0.4ex}{$#1$} / \raisebox{-0.7ex}{$#2$}}
\newcommand{\paren}[1]{\left(#1\right)}
\newcommand{\crochet}[1]{\left[#1\right]}
\begin{frame}\frametitle{Typing rules}
Abstraction:
\begin{prooftree}
\AxiomC{$\Gamma\vdash \rA:\bType$}
\AxiomC{$\Gamma,x:\rA\vdash \rB:\bs$}
\AxiomC{$\Gamma,x:\rA\vdash t:\rB$}
\TrinaryInfC{$\Gamma\vdash\lambda(x:A).t:\textcolor{red}{\Pi(x:A).B}$}
\end{prooftree}
Application:
\begin{prooftree}
\AxiomC{$\Gamma\vdash t:\textcolor{red}{\Pi(x:A).B}$}
\AxiomC{$\Gamma\vdash u:\rA$}
\BinaryInfC{$\Gamma\vdash t\,u:\textcolor{red}{\subst{B}{x}{u}}$}
\end{prooftree}
Conversion:
\begin{prooftree}
\AxiomC{$\Gamma\vdash t:\rA$}
\AxiomC{$\Gamma\vdash \rB:\bs$}
\AxiomC{$\rA\leftrightarrow_{\beta\mathcal{R}} \rB$}
\TrinaryInfC{$\Gamma\vdash t:\rB$}
\end{prooftree}
\end{frame}
\newcommand{\ens}[1]{\left\{#1\right\}}
\newcommand{\enscond}[2]{\ens{\left.\vphantom{#2}#1\right|#2}}
\section{Termination criterion}
\begin{frame}\frametitle{Main Goal}
\onslide<2>{\Large Find a {\color{red} criterion} such that:}
\LARGE If $\Gamma\vdash t:T$, then $t\in\mathrm{SN}(\to_{\beta\mathcal{R}})$.
\end{frame}
\subsection{Logical relation}
\begin{frame}\frametitle{Logical relation}
\begin{block}{Goal}
Define $\interp{T}$ such :
\begin{itemize}
\item $\Gamma\vdash t:T$ implies $t\in\interp{T}$,
\item $t\in\interp{T}$ implies $t\in\mathrm{SN}(\to_{\beta\mathcal{R}})$.
\end{itemize}
\end{block}
\begin{block}{Reducibility conditions}
\begin{itemize}
\item $\interp{T}\subseteq\mathrm{SN}$,
\item If $t\in\interp{T}$ and $t\to_{\beta\mathcal{R}}u$, then $u\in\interp{T}$,
\item If $t$ is neutral and $\enscond{u}{t\to_{\beta\mathcal{R}}u}\subseteq\interp{T}$, then $t\in\interp{T}$.
\end{itemize}
\end{block}
\begin{block}{}
\begin{itemize}
\item For $\beta$-reduction, we set $\interp{\Pi(x:A).B}=\enscond{t}{\forall a\in\interp{A}, t\,a\in\interp{\subst{B}{x}{a}}}$
\item For conversion rule, if $T\leftrightarrow_{\beta\mathcal{R}}U$, then $\interp{T}=\interp{U}$.
\end{itemize}
\end{block}
\end{frame}
\begin{frame}\frametitle{Our interpretation}
We define $\interp{.}$ as the fixpoint of a monotonic function.
\begin{lemma}[Adequacy]
if for all $f$, $f\in\interp{\Theta_f}$
and $\Gamma\vdash t:T$, then $t\in\interp{T}$.
\end{lemma}
\begin{block}{Goal}
Define $\interp{T}$ such that:
\begin{itemize}
\item $\Gamma\vdash t:T$ implies $t\in\interp{T}$,\hfill{ \color[RGB]{230,100,0}$\sim$}
\item $t\in\interp{T}$ implies $t\in\mathrm{SN}(\to_{\beta\mathcal{R}})$.\hfill{\color[RGB]{0,200,30}\checkmark}
\end{itemize}
\end{block}
\end{frame}
\begin{frame}\frametitle{Bonne structuration}
\begin{block}{Objectif}
Pour tout $f$, $f\in\interp{\Theta_f}$.
\end{block}
\onslide<2>{
\begin{block}{}
$\succeq$ pré-ordre sur la signature compatible avec la réécriture et le typage.
\end{block}
\begin{definition}[Système bien structuré]\label{def-well-struct}
$\mathcal{R}$ est \emph{bien structuré} si pour toute règle $(\Delta,f\,\bar l\to r)$,
avec $\Theta_f=\Pi(\bar x:\bar T).U$,
on a $\Delta\vdash_{\preceq f} r:U[\bar x\to \bar l]$.
\end{definition}
}
\end{frame}
\begin{frame}\frametitle{Les paires de dépendance reviennent}
\begin{definition}[Plain Function Passing]
$f\,\bar l\to r$ est \emph{PFP} si toutes les variables apparaissant dans $r$ qui sont de type fonctionnel sont égales à l'un des $l_i$.
\end{definition}
\begin{lemma}
Tout $f$ est dans l'interprétation de $\Theta_f$ si:
\begin{itemize}
\item $\mathcal{R}$ est \emph{bien structuré},
\item $\mathcal{R}$ est \emph{PFP},
\item $(>\to_{arg}^*)$ est bien fondée.
\end{itemize}
\end{lemma}
\end{frame}
\subsection{Utilisation de SCT}
\begin{frame}\frametitle{Théorème principal}
\begin{theorem}
$\to_{\beta\mathcal{R}}$ termine sur tous les termes typables dans $\lambda\Pi/\mathcal{R}$ si :
\begin{itemize}
\item $\to_{\beta\mathcal{R}}$ est localement confluente et préserve le typage,
\item $\mathcal{R}$ est bien structuré et \emph{Plain Function Passing},
\item $\mathcal{R}$ est \emph{Size-Change Terminating}.
\end{itemize}
\end{theorem}
\end{frame}
\section{\SCT{}}
\end{document}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment