A lambda-free higher-order recursive path order

Jasmin Christian Blanchette; Uwe Waldmann; Daniel Wand

doi:10.1007/978-3-662-54458-7_27

A lambda-free higher-order recursive path order

Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

5 Downloads (Pure)

Abstract

We generalize the recursive path order (RPO) to higher-order terms without λ-abstraction. This new order fully coincides with the standard RPO on first-order terms also in the presence of currying, distinguishing it from previous work. It has many useful properties, including well-foundedness, transitivity, stability under substitution, and the subterm property. It appears promising as the basis of a higher-order superposition calculus.

Original language	English
Title of host publication	Foundations of Software Science and Computation Structures
Subtitle of host publication	20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory anPractice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings
Editors	Javier Esparza, Andrzej S. Murawski
Publisher	Springer/Verlag
Pages	461-479
Number of pages	19
ISBN (Electronic)	9783662544587
ISBN (Print)	9783662544570
DOIs	https://doi.org/10.1007/978-3-662-54458-7_27
Publication status	Published - 2017
Event	20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017 - Uppsala, Sweden Duration: 22 Apr 2017 → 29 Apr 2017

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10203 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017
Country/Territory	Sweden
City	Uppsala
Period	22/04/17 → 29/04/17

Funding

We are grateful to Stephan Merz, Tobias Nipkow, and Christoph Weidenbach for making this research possible; to Heiko Becker and Dmitriy Traytel for proving some theorems on the lexicographic and multiset extensions in Isabelle/HOL; to Carsten Fuhs for his invaluable feedback and his experiments; to Alexander Steen for pointing us to related work; and to Simon Cruanes, Mark Summerfield, Dmitriy Traytel, and the anonymous reviewers for suggesting textual improvements. Blanchette has received funding from the European Research Council (ERC) under the European Union?s Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Wand is supported by the Deutsche Forschungsgemeinschaft (DFG) grant Hardening the Hammer (NI 491/14-1).

Funders	Funder number
Horizon 2020 Framework Programme	713999
European Research Council
Deutsche Forschungsgemeinschaft	NI 491/14-1

Access to Document

10.1007/978-3-662-54458-7_27

A Lambda-Free Higher-Order Recursive Path OrderFinal published version, 295 KBLicence: Article 25fa Dutch Copyright Act

Persistent URL (handle)

Persistent link

Cite this

Blanchette, J. C., Waldmann, U., & Wand, D. (2017). A lambda-free higher-order recursive path order. In J. Esparza, & A. S. Murawski (Eds.), Foundations of Software Science and Computation Structures: 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory anPractice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings (pp. 461-479). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10203 LNCS). Springer/Verlag. https://doi.org/10.1007/978-3-662-54458-7_27

Blanchette, Jasmin Christian ; Waldmann, Uwe ; Wand, Daniel. / A lambda-free higher-order recursive path order. Foundations of Software Science and Computation Structures: 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory anPractice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. editor / Javier Esparza ; Andrzej S. Murawski. Springer/Verlag, 2017. pp. 461-479 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{5c9ff1ff0e31407ba1d91c353998e75a,

title = "A lambda-free higher-order recursive path order",

abstract = "We generalize the recursive path order (RPO) to higher-order terms without λ-abstraction. This new order fully coincides with the standard RPO on first-order terms also in the presence of currying, distinguishing it from previous work. It has many useful properties, including well-foundedness, transitivity, stability under substitution, and the subterm property. It appears promising as the basis of a higher-order superposition calculus.",

author = "Blanchette, {Jasmin Christian} and Uwe Waldmann and Daniel Wand",

year = "2017",

doi = "10.1007/978-3-662-54458-7_27",

language = "English",

isbn = "9783662544570",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer/Verlag",

pages = "461--479",

editor = "Javier Esparza and Murawski, {Andrzej S.}",

booktitle = "Foundations of Software Science and Computation Structures",

note = "20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017 ; Conference date: 22-04-2017 Through 29-04-2017",

}

Blanchette, JC, Waldmann, U & Wand, D 2017, A lambda-free higher-order recursive path order. in J Esparza & AS Murawski (eds), Foundations of Software Science and Computation Structures: 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory anPractice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10203 LNCS, Springer/Verlag, pp. 461-479, 20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017, Uppsala, Sweden, 22/04/17. https://doi.org/10.1007/978-3-662-54458-7_27

A lambda-free higher-order recursive path order. / Blanchette, Jasmin Christian; Waldmann, Uwe; Wand, Daniel.
Foundations of Software Science and Computation Structures: 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory anPractice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. ed. / Javier Esparza; Andrzej S. Murawski. Springer/Verlag, 2017. p. 461-479 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10203 LNCS).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A lambda-free higher-order recursive path order

AU - Blanchette, Jasmin Christian

AU - Waldmann, Uwe

AU - Wand, Daniel

PY - 2017

Y1 - 2017

N2 - We generalize the recursive path order (RPO) to higher-order terms without λ-abstraction. This new order fully coincides with the standard RPO on first-order terms also in the presence of currying, distinguishing it from previous work. It has many useful properties, including well-foundedness, transitivity, stability under substitution, and the subterm property. It appears promising as the basis of a higher-order superposition calculus.

AB - We generalize the recursive path order (RPO) to higher-order terms without λ-abstraction. This new order fully coincides with the standard RPO on first-order terms also in the presence of currying, distinguishing it from previous work. It has many useful properties, including well-foundedness, transitivity, stability under substitution, and the subterm property. It appears promising as the basis of a higher-order superposition calculus.

UR - http://www.scopus.com/inward/record.url?scp=85015825488&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85015825488&partnerID=8YFLogxK

U2 - 10.1007/978-3-662-54458-7_27

DO - 10.1007/978-3-662-54458-7_27

M3 - Conference contribution

AN - SCOPUS:85015825488

SN - 9783662544570

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 461

EP - 479

BT - Foundations of Software Science and Computation Structures

A2 - Esparza, Javier

A2 - Murawski, Andrzej S.

PB - Springer/Verlag

T2 - 20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017

Y2 - 22 April 2017 through 29 April 2017

ER -

Blanchette JC, Waldmann U, Wand D. A lambda-free higher-order recursive path order. In Esparza J, Murawski AS, editors, Foundations of Software Science and Computation Structures: 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory anPractice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. Springer/Verlag. 2017. p. 461-479. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Epub 2017 Mar 16. doi: 10.1007/978-3-662-54458-7_27

A lambda-free higher-order recursive path order

Abstract

Publication series

Conference

Funding

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this