A lambda-free higher-order recursive path order

Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

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 languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings
EditorsJavier Esparza, Andrzej S. Murawski
PublisherSpringer/Verlag
Pages461-479
Number of pages19
ISBN (Print)9783662544570
DOIs
Publication statusPublished - 1 Jan 2017
Event20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017 - Uppsala, Sweden
Duration: 22 Apr 201729 Apr 2017

Publication series

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

Conference

Conference20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017
CountrySweden
City Uppsala
Period22/04/1729/04/17

Fingerprint Dive into the research topics of 'A lambda-free higher-order recursive path order'. Together they form a unique fingerprint.

  • 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 and Practice of Software, ETAPS 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