Commit d09a0f41 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Final version

parent 9ad9a7bf
......@@ -76,11 +76,11 @@
\section{Introduction}
\SCT{} \cite{sizechangetool} is a fully automated termination checker for the $\lm\Pi$-calculus modulo rewriting.
Its development was essential, when various libraries were encoded in an implementation of this logic:
Its development became essential as various libraries were encoded in an implementation of this logic:
the logical framework \Dedukti{} \cite{dowekAl19Dk}.
A logical framework allows the user to define the logic he wants to reason with and then use it to actually write proofs.
In \Dedukti{}, to define a logic the user provides a set of rewriting rules.
A logical framework allows the user to define the logic they want to reason with and then use it to actually write proofs.
To define a logic in \Dedukti{}, the user provides a set of rewriting rules.
Those rules do not only define functions, but can also define types.
However, to ensure that the defined type system has good properties, like logical consistency or decidability, the rules must satisfy some properties:
termination, confluence and type preservation.
......@@ -107,14 +107,14 @@ It is a system of dependent types where types are identified not only modulo the
but also by user-given rewriting rules.
\begin{defi}
$\lm\Pi/\mcal{R}$ is the Pure Type System \cite{barendregt92chapter} $\lm P$, enriched by a finite signature $\mbb{F}$ and a set of rules $(\D,f\,\bar l\to r)$ such that $f\in\mbb{F}$, $\FV(r)\subseteq\FV(\bar l)$ and $\D$ is a context associating a type to every variable of $\bar l$.
$\lm\Pi/\mcal{R}$ extends the Pure Type System $\lm P$ \cite{barendregt92chapter} with a finite signature $\mbb{F}$ and a set of rules $\mcal{R}=(\D,f\,\bar l\to r)$ such that $f\in\mbb{F}$, $\FV(r)\subseteq\FV(\bar l)$ and $\D$ is a context associating a type to every variable of $\bar l$.
$\to_\mcal{R}$ is the closure by substitution and context of $\mcal{R}$.
The conversion rule is enriched to take into account rewriting rules:
\begin{prooftree}
\AxiomC{$\Gamma\vdash t:A$}
\AxiomC{$\Gamma\vdash B:s$}
\AxiomC{$A\leftrightarrow_{\beta\mcal{R}}B$}
\AxiomC{$A\leftrightarrow^*_{\beta\mcal{R}}B$}
\RightLabel{(conv)}
\TrinaryInfC{$\Gamma\vdash t:B$}
\end{prooftree}
......@@ -127,7 +127,7 @@ Let us give two examples, highlighting the possibilities offered by the system.
A more comprehensive example can be found in \cite{blanqui19fscd}.
\begin{expl}[Summation of variable arity]
Type level rewrite rules allows us for instance to define {\tt F n} as the type {\tt Nat $\impli$ Nat $\impli$\dots$\impli$ Nat} with $n$ arrows.
Rewriting rules at type level allow us for instance to define {\tt F n} as the type {\tt Nat $\impli$ Nat $\impli$\dots$\impli$ Nat} with $n$ arrows.
With it, we can type the function {\tt sum} which is such that {\tt sum n $l_1$\dots $l_n$ = $l_1$ +\dots+ $l_n$}\footnote{\& is used in \Dedukti{} to identify pattern variables in rewriting rules.}.
\begin{lstlisting}[mathescape=true]
symbol Nat : TYPE
......@@ -195,7 +195,7 @@ It consists in following the arguments through sequences of recursive calls and
all idempotent matrices labeling a loop have some $-1$ on their diagonal.
\end{defi}
In \cite{blanqui19fscd}, we presented an adaptation of dependency pairs to $\lm\Pi/\mcal{R}$ and prove that (under some conditions) the absence of infinite chains implies the termination of $\to_{\beta\mcal{R}}$.
In \cite{blanqui19fscd}, we present an adaptation of dependency pairs to $\lm\Pi/\mcal{R}$ and prove that (under some conditions) the absence of infinite chains implies the termination of $\to_{\beta\mcal{R}}$.
After Wahlstedt \cite{wahlstedt07phd}, we used an adaptation of SCT to check the absence of infinite chains of dependency pairs.
\begin{defi}[Well-Structured System]\label{def-well-struct}
......@@ -225,7 +225,7 @@ we replace the plain-function passing hypothesis by a condition analogous to str
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Implementation and interaction with the type-checker}\label{sect-implem}
\SCT{} takes as input \Dedukti{} files or \tool{XTC} files, the format of the termination competition.
\SCT{} takes as input \Dedukti{} files or \tool{XTC} files, the format of the termination competition \cite{termComp}.
However, \tool{XTC} does not include dependent types now,
hence we proposed a backward compatible extension of the format.
In fact, the tool accepts this format extension.
......@@ -241,7 +241,7 @@ to use the extension \ref{extension-sn} of \indthm{thm-sn}.
This algorithm can be found in \cite{dowekAl19Dk}.
\item
\emph{well-structuring} requires to construct the pre-order described in \inddef{def-well-struct}.
Once this pre-order is computed, \Dedukti{} is reused to type-check the right-hand side of every rule in the pruned signature.
Once this pre-order is computed, \Dedukti{} is reused to check if it is possible to type the right-hand side of every rule using the pruned signature where symbols greater than the one defined are removed.
\item
\emph{size-change termination} requires to analyze every rule in order to extract the dependency pairs.
Then the call-graph is constructed.
......@@ -262,37 +262,37 @@ to use the extension \ref{extension-sn} of \indthm{thm-sn}.
\node[draw] (ast) at (0,0) {AST representation};
\node[draw] (xtc) at (-2.5,1) {XTC File};
\node[draw] (dk) at (-2.5,-1) {\tool{Dedukti} File};
\node[draw] (call_gr) at (4,-1) {Call graph};
\node (sct) at (8.6,-1) {\emph{Size-change termination}};
\node[draw] (symb_ord) at (2.3,-2) {Symbols order};
\node[draw] (dk_pruned) at (5.8,-2) {Pruned signature};
\node (pos) at (9.3,-2) {\emph{Strict positivity}};
\node[draw] (dk_sign) at (4,2) {\tool{Dedukti} signature};
\node (sr) at (9.1,2) {\emph{Type preservation}};
\node[draw] (type_gr) at (4.2,1) {Type ordering graph};
\node[draw] (type_cstr) at (4.2,0) {Type ordering constraints};
\node (well-struct) at (9.2,0.5) {\emph{Well-structuring}};
\node[draw] (symb_ord) at (2.3,1) {Symbols order};
\node[draw] (dk_pruned) at (5.8,1) {Pruned signature};
\node (well-struct) at (9.2,1) {\emph{Well-structuring}};
\node[draw] (call_gr) at (4,0) {Call graph};
\node (sct) at (8.6,0) {\emph{Size-change termination}};
\node[draw] (type_gr) at (4.2,-1) {Type ordering graph};
\node[draw] (type_cstr) at (4.2,-2) {Type ordering constraints};
\node (pos) at (9.3,-1.5) {\emph{Strict positivity}};
\draw[>=latex,->,color=blue] (xtc) to (ast);
\draw[>=latex,->,color=blue] (dk) to (ast);
\draw[>=latex,->,color=darkgreen] (ast) to[bend right=10] (call_gr);
\draw[>=latex,->,color=darkgreen] (ast) to (symb_ord);
\draw[>=latex,->,color=darkgreen] (ast) to[bend left=10] (type_gr);
\draw[>=latex,->,color=darkgreen] (ast) to (type_cstr);
\draw[>=latex,->,color=red] (ast) to[bend left] (dk_sign);
\draw[>=latex,->,color=red] (symb_ord) to (dk_pruned);
\draw[>=latex,->,double] (dk_sign) to (sr);
\draw[>=latex,->,double] (dk_pruned) to (pos);
\draw[>=latex,->,color=darkgreen] (ast) to[bend left=20] (symb_ord);
\draw[>=latex,->,color=red] (symb_ord) to (dk_pruned);
\draw[>=latex,->,double] (dk_pruned) to (well-struct);
\draw[>=latex,->,color=darkgreen] (ast) to (call_gr);
\draw[>=latex,->,double] (call_gr) to (sct);
\draw[double] (type_gr) to[out=0] (7,0.5);
\draw[double] (type_cstr) to[out=0,in=-140] (7,0.5);
\draw[>=latex,->,double] (7,0.5) to (well-struct);
\draw[>=latex,->,color=darkgreen] (ast) to[bend right=10] (type_gr);
\draw[>=latex,->,color=darkgreen] (ast) to[bend right] (type_cstr);
\draw[double] (type_gr) to[out=0] (7,-1.5);
\draw[double] (type_cstr) to[out=0,in=-140] (7,-1.5);
\draw[>=latex,->,double] (7,-1.5) to (pos);
\node[draw] (leg) at (-2,-2.2) {\begin{tabular}{ll}
{\color{blue}$\to$}&Parser\\
{\color{red}$\to$}&Translation to \tool{Dedukti}\\
{\color{darkgreen}$\to$}&Rule analyzer\\
\end{tabular}};
\end{tikzpicture}
\caption{Behaviour of \tool{SizeChangeTool}\label{fig-sct-schema}}
\caption{\tool{SizeChangeTool} Workflow\label{fig-sct-schema}}
\end{figure}
\end{center}
......@@ -329,7 +329,7 @@ The very low time consumption of the presented criterion suggests that \tool{Wan
If we restrict ourselves to orthogonal systems,
it is then possible to compare our technique to the ones implemented in \tool{Coq} and \tool{Agda}.
\tool{Coq} essentially implements a higher-order version of primitive recursion \cite{gimenez94types},
whereas \tool{Agda} uses size-change termination \cite{abel98foetus}.
whereas \tool{Agda} uses subterm criterion (a criterion very similar to size-change termination) \cite{abel98foetus}.
Hence, \tool{Coq} cannot handle function definitions with permuted arguments in function calls, which is not a problem for \tool{Agda} and \SCT{}.
Agda recently added the possibility of declaring rewriting rules
but this feature is highly experimental and no check is performed on the rules.
......
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