Commit 470dd74b authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

version 1, envoyée FB et OH

parent a11aee16
......@@ -80,10 +80,17 @@
\Dedukti{} \cite{dowekAl19Dk} is a logical framework,
meaning that the user can define the logic he wants to reason with and then use it to actually make proofs.
To define its logic, the user provide a set of rewriting rules.
However, to ensure that the defined type system has good properties, like logical consistency or decidability, the rules must satisfy some properties,
like termination, confluence or type preservation.
Those rules does not only define functions, but also 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.
Many criteria have been created to check termination of first-order rewriting.
For instance, dependency pairs \cite{arts00tcs}, which evolved in a complete framework \cite{thiemann07phd} or size-change termination \cite{lee01popl}, just to mention those appearing in this abstract.
The dynamism of this research area is illustrated by the numerous tools participating in the various first-order categories of the termiantion competition \cite{termComp}.
For higher-order rewriting too, criteria have been crafted (many of them in \cite{kop12phd} and a category exists in the competition.
However, one can deplore the small number of participants in this category\footnote{Only 2 in 2019, including \SCT{}}.
On the other hand, criteria have been developed for higher-order rewriting rules with dependent types \cite{blanqui05mscs,jouannaud15tlca},
This lack of implementations is even more visible for higher-order rewriting with dependent types, for which criteria have been developed \cite{blanqui05mscs,jouannaud15tlca},
but as far as the author knows, none of them have been implemented.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -92,7 +99,6 @@ but as far as the author knows, none of them have been implemented.
The $\lm\Pi$-calculus modulo rewriting ($\lm\Pi/\mcal{R}$ for short) is an extension of the logical framework LF \cite{harper93jacm}.
It is a system of dependent types where types are identified not only modulo the $\beta$-conversion of $\lm$-calculus,
but also by user-given rewriting rules.
Those rules does not only define functions, but also types.
\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$.
......@@ -152,7 +158,7 @@ We are interested in the strong normalization of $\to_{\beta\mcal{R}}=(\to_\beta
Dependency pairs are at the core of all the state-of-the-art automated termination provers for first-order term rewriting systems.
Arts and Giesl \cite{arts00tcs} proved that a first-order rewriting relation is terminating if and only if there is no infinite chains, that are sequences of dependency pairs interleaved with reductions in the arguments.
This notion of dependency pairs has been extended to the higher-order \cite{blanqui06wst,kop12phd,fuhs19esop},
This notion of dependency pairs has been extended to the higher-order \cite{blanqui06wst,fuhs19esop},
however those extensions do not include dependent types, which is a compulsory feature when we are developping a logical framework.
\begin{defi}[Dependency pairs]
......@@ -172,13 +178,13 @@ It consists in following the arguments through sequences of recursive and checki
Let $\rhd$ be a well-founded order on terms.
The call graph $\mcal{G}(\mcal{R},\rhd)$ associated to $\mcal{R}$ is the directed labeled graph on the defined symbols of $\mbb{F}$ such that there is an edge between $f$ and $g$ iff there is a dependency pair $f\,l_1\dots l_p>g\,m_1\dots m_q$.
This edge is labeled with the matrix $(a_{i,j})_{i\leq ar(f),j\leq ar(g)}$ where:
\begin{tabular}{ll}
$\bullet$ if $l_i\rhd m_j$, then $a_{i,j}=-1$; &
$\bullet$ if $l_i=m_j$, then $a_{i,j}=0$;\\
$\bullet$ otherwise $a_{i,j}=\infty$ (in particular if $i>p$ or $j>q$).&\\
\end{tabular}
$\mcal{R}$ is size-change terminating (SCT) if, in the transitive closure of $\mcal{G}(\mcal{R})$ (using the min-plus semi-ring to multiply the matrices labeling the edges),
all idempotent matrices labeling a loop have some $-1$ on the diagonal.
\end{defi}
......@@ -228,12 +234,12 @@ to use the extension \ref{extension-sn} of \indthm{thm-sn}.
Then the call-graph is constructed.
To perform size-change termination checking, one must compute the transitive closure of the call graph and verify the presence of a $-1$ on the diagonal of every idempotent matrices labeling a loop.
This check has been implemented by Lepigre and Raffalli for the language PML${}_2$ \cite{lepigre17PML}.
\SCT{} reuses their work to analyze the call-graph.
\SCT{} reuses their work to analyze the call-graph.
\item
\emph{the strict positivity condition} requires to have a pre-order on type constructors.
The user is not asked to provide this order.
While analyzing the rules, \SCT{} constructs a graph whose vertices are type constructors and arrows means ``is smaller or equal to'' as well as a list of constraints of the form ``Type constructor A is strictly greater than type constructor B.''
To check that this relation is indeed a pre-order, one checks that for every constraint ``A is strictly smaller than B.'' there is no arrow between A and B in the transitive closure of the graph.
\end{enumerate}
......@@ -319,9 +325,34 @@ In particular, \tool{Agda} termination checker does not handle rewriting rules.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Conclusion and future work}
For now on, \SCT{} takes as input \Dedukti files or \tool{XTC} files, the format of the termination competition.
However, \tool{XTC} does not include dependent types now,
hence we suggested a backward compatible extension of the format.
In fact, it is this extension which is accepted by the tool.
One could imagine extending it to other input format,
for instance to deal with the rewriting rules offered in \tool{Agda}.
Following the approach adopted by \tool{Wanda},
one could also just study truly higher-order rules,
use a state-of-the-art first-order prover for the remaining rules
and then rely on a modularity theorem to conclude.
This strategy would improve the performance of \SCT{} in the competition, since, according to C. Kop:
``about half the benchmarks now do little more than test the strength of the first-order back-end that some higher-order tools use.'' \cite{kop19mail}.
One could also think of various enhancement of the criterion,
for instance to handle rules with a local increase of the size of the arguments like in:
\begin{lstlisting}[mathescape=true]
rule f &x $\alp$ g (s &x) rule g (s (s &x)) $\alp$ f &x
\end{lstlisting}
Hyvernat proposed such an extension of SCT for constructor based first-order languages \cite{hyvernat14lmcs}.
Adapting other so-called ``dependency pairs processors'' \cite{fuhs19esop} to the $\lm\Pi/\mcal{R}$ is of course another active subject of study and would improve the tool.
Now that a higher-order rewriting with dependent types termination prover has been developed,
one can hope such development will be emulated by other researchers.
The adoption of an extension of \tool{XTC} and the creation of a category for $\lm\Pi/\mcal{R}$ in the competition,
would probably support the creation of such new implementations.
We hope the development of this tool will be emulated by other researchers.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{thebibliography}{10}
......@@ -388,6 +419,12 @@ R.~Harper, F.~Honsell, G.~Plotkin.
logics}.
\newblock {\em JACM} 40(1):143--184, 1993.
\bibitem{hyvernat14lmcs}
P.~Hyvernat.
\newblock \href{http://doi.org/10.2168/LMCS-10(1:11)2014}{The size-change
termination principle for constructor based languages}.
\newblock {\em LMCS} 10(1):1--30, 2014.
\bibitem{jouannaud15tlca}
J.-P. Jouannaud, J.~Li.
\newblock \href{http://doi.org/10.4230/LIPIcs.TLCA.2015.257}{Termination of
......@@ -400,6 +437,11 @@ C.~Kop.
termination}}.
\newblock PhD thesis, VU University Amsterdam, 2012.
\bibitem{kop19mail}
C.~Kop.
\newblock \href{http://lists.lri.fr/pipermail/termtools/2019-March/001226.html}{Mail to the termtools list.}
\newblock {higher-order union beta category in the TPDB. 19/03/2019.}
\bibitem{Wanda}
C.~Kop.
\newblock {Wanda}.
......@@ -427,7 +469,7 @@ R.~Thiemann.
\newblock PhD thesis, RWTH Aachen University, 2007.
\newblock Technical Report AIB-2007-17.
\bibitem{wahlstedt07phd}
D.~Wahlstedt.
\newblock {\em
......
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