On the formalization of termination techniques based on multiset orderings

René Thiemann; Guillaume Allais; Julian Nagele

doi:10.4230/LIPIcs.RTA.2012.339

On the formalization of termination techniques based on multiset orderings

René Thiemann, Guillaume Allais, Julian Nagele

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

20 Citations (Scopus)

14 Downloads (Pure)

Abstract

Multiset orderings are a key ingredient in certain termination techniques like the recursive path ordering and a variant of size-change termination. In order to integrate these techniques in a certifier for termination proofs, we have added them to the Isabelle Formalization of Rewriting. To this end, it was required to extend the existing formalization on multiset orderings towards a generalized multiset ordering. Afterwards, the soundness proofs of both techniques have been established, although only after fixing some definitions.

Concerning efficiency, it is known that the search for suitable parameters for both techniques is NP-hard. We show that checking the correct application of the techniques--where all parameters are provided--is also NP-hard, since the problem of deciding the generalized multiset ordering is NP-hard.

Original language	English
Title of host publication	23rd International Conference on Rewriting Techniques and Applications (RTA'12)
Editors	Ashish Tiwari
Pages	339-354
Number of pages	16
Volume	15
DOIs	https://doi.org/10.4230/LIPIcs.RTA.2012.339
Publication status	Published - 29 May 2012
Event	International Conference on Rewriting Techniques and Applications - Noyori Conference Hall, Nagoya, Japan Duration: 28 May 2012 → 2 Jun 2012 Conference number: 23 https://rta2012.trs.cm.is.nagoya-u.ac.jp/

Publication series

Name	Leibniz International Proceedings in Informatics (LIPIcs)
Publisher	Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
Volume	15
ISSN (Print)	1868-8969

Conference

Conference	International Conference on Rewriting Techniques and Applications
Abbreviated title	RTA'12
Country/Territory	Japan
City	Nagoya
Period	28/05/12 → 2/06/12
Internet address	https://rta2012.trs.cm.is.nagoya-u.ac.jp/

Keywords

formalization
term rewriting
termination
orderings

Access to Document

10.4230/LIPIcs.RTA.2012.339Licence: CC BY-ND 4.0

Thiemann-etal-RTA2012-On-the-formalization-of-termination-techniquesFinal published version, 557 KBLicence: CC BY-ND 4.0

Cite this

@inproceedings{7cbf1b76818a47d08923ed672ded9f68,

title = "On the formalization of termination techniques based on multiset orderings",

abstract = "Multiset orderings are a key ingredient in certain termination techniques like the recursive path ordering and a variant of size-change termination. In order to integrate these techniques in a certifier for termination proofs, we have added them to the Isabelle Formalization of Rewriting. To this end, it was required to extend the existing formalization on multiset orderings towards a generalized multiset ordering. Afterwards, the soundness proofs of both techniques have been established, although only after fixing some definitions.Concerning efficiency, it is known that the search for suitable parameters for both techniques is NP-hard. We show that checking the correct application of the techniques--where all parameters are provided--is also NP-hard, since the problem of deciding the generalized multiset ordering is NP-hard. ",

keywords = "formalization, term rewriting, termination, orderings",

author = "Ren{\'e} Thiemann and Guillaume Allais and Julian Nagele",

year = "2012",

month = may,

day = "29",

doi = "10.4230/LIPIcs.RTA.2012.339",

language = "English",

isbn = "9783939897385",

volume = "15",

series = "Leibniz International Proceedings in Informatics (LIPIcs)",

publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik",

pages = "339--354",

editor = "Ashish Tiwari",

booktitle = "23rd International Conference on Rewriting Techniques and Applications (RTA'12)",

note = "International Conference on Rewriting Techniques and Applications , RTA'12 ; Conference date: 28-05-2012 Through 02-06-2012",

url = "https://rta2012.trs.cm.is.nagoya-u.ac.jp/",

}

Thiemann, R, Allais, G & Nagele, J 2012, On the formalization of termination techniques based on multiset orderings. in A Tiwari (ed.), 23rd International Conference on Rewriting Techniques and Applications (RTA'12). vol. 15, Leibniz International Proceedings in Informatics (LIPIcs), vol. 15, pp. 339-354, International Conference on Rewriting Techniques and Applications , Nagoya, Japan, 28/05/12. https://doi.org/10.4230/LIPIcs.RTA.2012.339

On the formalization of termination techniques based on multiset orderings. / Thiemann, René; Allais, Guillaume; Nagele, Julian.
23rd International Conference on Rewriting Techniques and Applications (RTA'12). ed. / Ashish Tiwari. Vol. 15 2012. p. 339-354 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 15).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

TY - GEN

T1 - On the formalization of termination techniques based on multiset orderings

AU - Thiemann, René

AU - Allais, Guillaume

AU - Nagele, Julian

N1 - Conference code: 23

PY - 2012/5/29

Y1 - 2012/5/29

N2 - Multiset orderings are a key ingredient in certain termination techniques like the recursive path ordering and a variant of size-change termination. In order to integrate these techniques in a certifier for termination proofs, we have added them to the Isabelle Formalization of Rewriting. To this end, it was required to extend the existing formalization on multiset orderings towards a generalized multiset ordering. Afterwards, the soundness proofs of both techniques have been established, although only after fixing some definitions.Concerning efficiency, it is known that the search for suitable parameters for both techniques is NP-hard. We show that checking the correct application of the techniques--where all parameters are provided--is also NP-hard, since the problem of deciding the generalized multiset ordering is NP-hard.

AB - Multiset orderings are a key ingredient in certain termination techniques like the recursive path ordering and a variant of size-change termination. In order to integrate these techniques in a certifier for termination proofs, we have added them to the Isabelle Formalization of Rewriting. To this end, it was required to extend the existing formalization on multiset orderings towards a generalized multiset ordering. Afterwards, the soundness proofs of both techniques have been established, although only after fixing some definitions.Concerning efficiency, it is known that the search for suitable parameters for both techniques is NP-hard. We show that checking the correct application of the techniques--where all parameters are provided--is also NP-hard, since the problem of deciding the generalized multiset ordering is NP-hard.

KW - formalization

KW - term rewriting

KW - termination

KW - orderings

U2 - 10.4230/LIPIcs.RTA.2012.339

DO - 10.4230/LIPIcs.RTA.2012.339

M3 - Conference contribution book

SN - 9783939897385

VL - 15

T3 - Leibniz International Proceedings in Informatics (LIPIcs)

SP - 339

EP - 354

BT - 23rd International Conference on Rewriting Techniques and Applications (RTA'12)

A2 - Tiwari, Ashish

T2 - International Conference on Rewriting Techniques and Applications

Y2 - 28 May 2012 through 2 June 2012

ER -

On the formalization of termination techniques based on multiset orderings

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this