Skip to main content
Conference Proceedings

A total AC-compatible reduction ordering on higher-order terms

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (1998) 1443 LNCS 530-542
DOI: 10.1007/bfb0055081
2Citations
Citations of this article
13Readers
Mendeley users who have this article in their library.
Get full text

Abstract

The higher-order rewriting in presence of associative and commutative (AC) symbols is considered. A higher-order reduction ordering which allows to state the termination of a given rewriting system is presented. This ordering is an AC-cxtensiou of λ-RPO and is defined on simply-typed λ-terms in β-normal η-long form. It is total on ground terms.

Cite

CITATION STYLE

APA

Walukiewiez, D. (1998). A total AC-compatible reduction ordering on higher-order terms. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1443 LNCS, pp. 530–542). https://doi.org/10.1007/bfb0055081

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free