... @@ -294,7 +294,7 @@ def sum : (n: Nat) -> F n ... @@ -294,7 +294,7 @@ def sum : (n: Nat) -> F n \newcommand{\ens}[1]{\left\{#1\right\}} \newcommand{\ens}[1]{\left\{#1\right\}} \newcommand{\enscond}[2]{\ens{\left.\vphantom{#2}#1\right|#2}} \newcommand{\enscond}[2]{\ens{\left.\vphantom{#2}#1\right|#2}} \section{Termination criterion} \section{Termination Criterion} \begin{frame}\frametitle{Main Goal} \begin{frame}\frametitle{Main Goal} ... @@ -303,7 +303,7 @@ def sum : (n: Nat) -> F n ... @@ -303,7 +303,7 @@ def sum : (n: Nat) -> F n \LARGE If $\Gamma\vdash t:T$, then $t\in\mathrm{SN}(\to_{\beta\mathcal{R}})$. \LARGE If $\Gamma\vdash t:T$, then $t\in\mathrm{SN}(\to_{\beta\mathcal{R}})$. \end{frame} \end{frame} \subsection{Logical relation} \subsection{Logical Relations} \begin{frame}\frametitle{Logical Relations} \begin{frame}\frametitle{Logical Relations} \begin{block}{Goal} \begin{block}{Goal} ... @@ -394,7 +394,7 @@ $\color{red}{(3)}$ append _ (cons x p l) q m $\color{red}{>}$ p + q ... @@ -394,7 +394,7 @@ $\color{red}{(3)}$ append _ (cons x p l) q m $\color{red}{>}$ p + q \end{frame} \end{frame} \begin{frame}[fragile]\frametitle{Call-graph: Example} \begin{frame}[fragile]\frametitle{Call-Graph: Example} \begin{lstlisting}[mathescape=true] \begin{lstlisting}[mathescape=true] def plus : Nat -> Nat -> Nat. def plus : Nat -> Nat -> Nat. set infix "+" := plus. set infix "+" := plus. ... @@ -423,15 +423,15 @@ def append: (p: Nat) -> List p -> ... @@ -423,15 +423,15 @@ def append: (p: Nat) -> List p -> \end{center} \end{center} \end{frame} \end{frame} \subsection{Well-structuring} \subsection{Well-Structuring} \begin{frame}\frametitle{Well-structuring} \begin{frame}\frametitle{Well-Structuring} \begin{block}{} \begin{block}{} $\succeq$ quasi-order on the signature compatible with rewriting and typing. $\succeq$ quasi-order on the signature compatible with rewriting and typing. \end{block} \end{block} \begin{definition}[Well-structured system]\label{def-well-struct} \begin{definition}[Well-Structured System]\label{def-well-struct} $\mathcal{R}$ is \emph{well-structured} if for all rule $(\Delta,f\,\bar l\to r)$, $\mathcal{R}$ is \emph{well-structured} if for all rule $(\Delta,f\,\bar l\to r)$, with $\Theta_f=\Pi(\bar x:\bar T).U$, with $\Theta_f=\Pi(\bar x:\bar T).U$, we have $\Delta\vdash_{\!\!\preceq f} r:U[\bar x\to \bar l]$. we have $\Delta\vdash_{\!\!\preceq f} r:U[\bar x\to \bar l]$. ... @@ -475,7 +475,7 @@ def append: (p: Nat) -> List p -> ... @@ -475,7 +475,7 @@ def append: (p: Nat) -> List p -> \subsection{Size-Change Termination} \subsection{Size-Change Termination} \begin{frame}[fragile]\frametitle{Call-graph: Example} \begin{frame}[fragile]\frametitle{Call-Graph: Example} \begin{lstlisting}[mathescape=true] \begin{lstlisting}[mathescape=true] def plus : Nat -> Nat -> Nat. def plus : Nat -> Nat -> Nat. set infix "+" := plus. set infix "+" := plus. ... ...