Source-linked AI summary
An Applicative Multiset Path Order (Extended Version)
Nao Hirokawa, Teppei Saito, Teppei Tanaka, Wataru Yachi
TL;DR
The paper addresses the difficulty of proving termination for untyped applicative rewriting, including a multiplication rule that the multiset path order cannot handle. It introduces arity assignment and reification to address partial and variable application, and reports a complete, terminating, and confluent rewrite system for the introductory equations. The order also proves termination of typical higher-order functions such as map and filter, while its decision status remains unclear for a fixed precedence and arity assignment.
Problem
The multiset path order cannot prove termination of the one-rule multiplication system, illustrating a difficulty in proving termination for applicative rewriting.
Source: §1 · p. 1Method
The variant combines arity assignment for constants with reification of function application to handle partial and variable application.
Source: §1 · p. 1Results
The order proves termination of typical higher-order functions such as map and filter and yields a complete, terminating, and confluent rewrite system for the introductory equations.
Source: §1 · pp. 1–2Takeaways & Limitations
The order provides a graceful correspondence with the original multiset path order and a minimum guarantee in termination proving.
Source: §1 · p. 2For a fixed precedence and arity assignment, it is unclear whether the relation is decidable, because its construction considers all grounding substitutions.
Source: §7 · p. 16
Abstract
from arXiv · showhide
We present a variant of the multiset path order for untyped applicative term rewriting. Compared to existing work, our variant incorporates two distinctive features, dubbed arity assignment and reification, to overcome difficulties in handling partial and variable application.
1 Introduction
The paper extends the multiset path order to untyped applicative rewriting, aiming to prove termination for lambda-free higher-order functions represented with first-order terms. Arity assignment and reification address partial and variable application, and the resulting order proves termination of functions such as map and filter while satisfying gracefulness.
1 Introduction
- The multiset path order cannot prove termination of the one-rule system mult (s x) y → add (mult x y) y, illustrating a difficulty in applicative termination proofs.The paper frames this as a limitation of reduction orders with the subterm property.Source: §1 · p. 1
- Knuth–Bendix completion with the order transforms the displayed append, map, and id equations into a complete rewrite system.The paper identifies the resulting system as terminating and confluent.Source: §1 · p. 1
- Arity assignment for constants simulates the original multiset path order, while reification, inspired by uncurrying, handles partial application and variable application.These are the variant’s two distinctive technical features.Source: §1 · p. 1
- The order is a reduction order that proves termination of typical higher-order functions such as map and filter, and satisfies gracefulness, a correspondence with the original multiset path order.The paper presents gracefulness as providing a minimum guarantee in termination proving.Source: §1 · p. 2
- The paper builds the order in three stages: a transitive, well-founded base order, a context-closed well-founded order, and then a reduction order.Section 6 evaluates the resulting order; Section 7 discusses related work.Source: §1 · p. 2
- This article is an extended version of the conference paper, with omitted proofs in the appendix.Source: §1 · p. 2
2 Preliminaries
This section recalls term rewriting and the multiset path order, then introduces applicative terms and the termination obstacle posed by multiplication. It also describes an arity-assignment-based order whose subterm property does not hold.
2 Preliminaries
- A reduction order is well-founded and closed under substitutions and contexts; a TRS is terminating exactly when some reduction order orients every rule.This equivalence is stated as Proposition 1.Source: §2 · p. 2
- The multiset path order compares terms using a precedence and multiset extension, and is a reduction order when its precedence is well-founded.Its comparison clauses include subterm, precedence, and multiset comparisons.Source: §2 · p. 3
- Applicative terms use a single binary application symbol, and currying represents function applications as nested applications to constants.The map TRS is given as an applicative TRS over {nil, cons, map, ◦}.Source: §2 · pp. 3–4
- The multiset path order proves termination for the addition and multiplication system, but the multiset path order’s subterm property prevents it from proving termination of the curried multiplication rule.The substitution y ↦ s x yields a descending cycle, contradicting the required order relation.Source: §2 · pp. 3–4
- The paper’s MPO derivation for addition relies on the subterm property and closure under contexts to justify decreases by chopping symbols.Source: §2 · pp. 3–4
3 Base Order
The base order extends the multiset path order to applicative terms using arity assignments and reification to handle non-full applications. It is transitive and well-founded when the precedence is well-founded, but is not itself closed under substitutions or contexts.
3 Base Order
- Arity assignments classify constant-headed terms as full or partial, while reification represents an application by introducing the fresh constant @.The relation retains the original MPO's first three cases and adds two cases to resolve non-fullness.Source: §3 · pp. 4–5
- For the example assignment, map f nil is full and map id is partial, while map f x y and f x are neither full nor partial.The latter terms illustrate that a term need not be either full or partial.Source: §3 · p. 4
- Two term measures support induction despite reification increasing term size, and the base relation is shown not to be closed under substitutions.The measures count symbols outside @-headed applications and argument counts; reification can increase term size while the measures decrease for induction.Source: §3 · pp. 5–6
- The base relation is transitive and well-founded when the precedence is well-founded.Transitivity and well-foundedness are established before the order is lifted further.Source: §3 · pp. 6, 8
4 Eta-Restriction
The base relation is not context-closed, so the paper defines an η-restriction that adds comparisons after fresh-variable application when the left term is partial. With @ maximal and a well-founded precedence, the restriction is a well-founded order closed under contexts.
4 Eta-Restriction
- The base relation is not closed under contexts, and two examples expose problematic comparisons involving partial applications.The paper addresses one example by requiring @ to be maximal and the other with a technique akin to η-saturation.Source: §4 · p. 8
- When the left term is partial, the η-restriction requires both the base comparison and a comparison after applying a fresh variable.The definition uses a fresh variable not occurring in the left term.Source: §4 · p. 9
- The base relation is preserved by substitutions that are head-preserving for both terms, unlike arbitrary substitutions.Head-preserving substitutions leave the variables occurring in head position unchanged.Source: §4 · p. 9
- The η-restriction is also preserved by head-preserving substitutions, and its definition ensures fresh-variable comparisons for partial terms.The added comparison is what allows the restricted relation to address partial applications while retaining that substitution property.Source: §4 · p. 9
- With @ maximal in the precedence and the precedence's strict part well-founded, the η-restriction is a well-founded order closed under contexts.The context-closure proof also establishes transitivity under the same maximality assumption.Source: §4 · p. 11
5 Reduction Order
The paper defines AMPO by requiring the η-restricted base comparison to hold after every grounding substitution. Under stated conditions it is a reduction order, and a head-variable-free source gives a sufficient way to establish AMPO comparisons.
5 Reduction Order
- AMPO is not closed under substitutions, so it is not itself a reduction order without the grounding-substitution construction.The paper's example shows an η-restricted comparison that fails after substitution.Source: §5 · p. 11
- AMPO requires the η-restricted comparison to hold after every grounding substitution for the two terms.The paper identifies this universally grounded relation as its applicative multiset path order.Source: §5 · p. 11
- AMPO is a reduction order when @ is maximum in the precedence and its strict part is well-founded.The proof uses the η-restriction's well-foundedness and closure under ground contexts.Source: §5 · p. 12
- If the source term is head-variable-free, an η-restricted comparison implies an AMPO comparison when @ is maximum.The paper presents this as a sufficient condition for checking AMPO comparisons.Source: §5 · pp. 12–13
- For functional terms, currying preserves MPO comparisons in AMPO when arities match the original function-symbol arities.The paper calls this the gracefulness property.Source: §5 · p. 13
6 Evaluation
The evaluation demonstrates termination proofs on higher-order function examples and tests the criterion on TPDB systems. It also identifies cases AMPO cannot orient.
6 Evaluation
- The append, map, and id ATRS is complete, and its termination is shown with the stated arity assignment and precedence.The example generalizes the map equation for cons x nil to a rule for cons x xs.Source: §6 · p. 13
- The filter ATRS terminates under α(@) = 2, α(if) = 3, α(cons) = α(filter) = 2, and α(nil) = α(true) = α(false) = 0.The stated precedence is @ ∼ filter ≻ if ≻ cons ≻ nil.Source: §6 · p. 14
- For zip, α(zip) = 0 permits the ordering, while changing it to 3 makes the second rule unorderable.The text attributes handling variable application f x to reification of the left-hand side.Source: §6 · p. 14
- AMPO cannot orient f (f x) → f (g (f x)) or a → f f, and adding mapid → map id prevents the stated termination proof.The first two limitations are attributed to the inductive definition of the base order; the added rule requires mapid ≻ @, contradicting @’s maximality.Source: §6 · p. 14
- 24 of 143 left head variable free ATRSs were shown terminating by AMPO, versus 2 by MPO; AProVE and NaTT proved 165 and 148 of the 202 ATRSs, respectively.Both AProVE and NaTT subsume AMPO’s results.Source: §6 · p. 14
7 Conclusion
The conclusion compares AMPO with related higher-order orders and discusses limitations in comparison choices and decidability. It anticipates a connection between AMPO, generalized uncurrying, and MPO.
7 Conclusion
- Unlike EPO, AMPO can show termination of higher-order recursive functions such as map and filter, while EPO is restricted to non-duplicating rules.EPO is described as the first reduction order in the MPO family; lambda-free RPO is not closed under contexts.Source: §7 · p. 15
- The authors anticipate AMPO can be simulated by generalized uncurrying combined with the original MPO.Their example relates the precedence for uncurried rules to the precedence in Example 37.Source: §7 · p. 15
- Left-to-right lexicographic comparison makes Lemma 18 fail; the authors expect right-to-left comparison to be viable.The paper notes that LPO compares arguments lexicographically.Source: §7 · pp. 15–16
- For a fixed precedence and arity assignment, whether s >ampo t is decidable remains unclear because Definition 30 considers all grounding substitutions.The authors say a decision procedure or generalization of Theorem 34 would enable more effective use of completion and rewriting induction.Source: §7 · p. 16
A Omitted Proofs
The appendix establishes properties used in the order’s proofs and shows that orientability of finite LATRSs with AMPO is decidable. Its search can bound arity assignments using applicative arity.
A Omitted Proofs
- The base order preserves variables: if s ▷ t, then Var(s) ⊇ Var(t).The proof uses induction on the derivation, including cases involving reification.Source: A Omitted Proofs · p. 19
- Under a head-preserving substitution σ, s ▷ t implies sσ ▷ tσ.The proof proceeds by induction on the derivation and uses head preservation for subterms.Source: A Omitted Proofs · p. 19
- When α is replaced by β(f) = min{α(f), aa_R(f) + 1}, fullness of terms in T_R is unchanged, so the orderings carry over.The appendix extends this preservation to ▷, ▷η, >ampo, and rule orientability.Source: A Omitted Proofs · p. 20
- For finite LATRS R, whether R ⊆ >ampo holds for some arity assignment and precedence is decidable.The search may assume α(f) ≤ aa_R(f) + 1 for every f, allowing enumeration of suitable assignments and precedences.Source: A Omitted Proofs · p. 20