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

2 Downloads (Pure)


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
Subtitle of host publication20th 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
EditorsJavier Esparza, Andrzej S. Murawski
Number of pages19
ISBN (Electronic)9783662544587
ISBN (Print)9783662544570
Publication statusPublished - 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


Conference20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017
City Uppsala


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).

FundersFunder number
Horizon 2020 Framework Programme713999
European Research Council
Deutsche ForschungsgemeinschaftNI 491/14-1


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

    Cite this