Anzeige
Erschienen in:
2014 | OriginalPaper | Buchkapitel
Confluence by Critical Pair Analysis
verfasst von : Jiaxiang Liu, Nachum Dershowitz, Jean-Pierre Jouannaud
Erschienen in: Rewriting and Typed Lambda Calculi
Verlag: Springer International Publishing
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Knuth and Bendix showed that confluence of a terminating first-order rewrite system can be reduced to the joinability of its finitely many critical pairs. We show that this is still true of a rewrite system
${R_{\textit{T}}} \cup{R_{\textit{NT}}} $
such that
$R_{\textit{T}}$
is terminating and
$R_{\textit{NT}}$
is a left-linear, rank non-increasing, possibly non-terminating rewrite system. Confluence can then be reduced to the joinability of the critical pairs of
$R_{\textit{T}}$
and to the existence of decreasing diagrams for the critical pairs of
$R_{\textit{T}}$
inside
$R_{\textit{NT}}$
as well as for the rigid parallel critical pairs of
$R_{\textit{NT}}$
.