Chapter 5: Term Ordering

Mix.install([
  {:shot_tx, "0.1.0"},
  {:shot_to, "0.2.0"},
  {:kino, "~> 0.19.0"}
])

Overview

Demodulation was introduced in Chapter 3 as a branch-local simplification: an oriented equation $\ell \to r$ rewrites occurrences of $\ell$ to $r$, shrinking the branch's formula set without touching soundness or completeness. That "oriented" carries an unstated obligation. Rewriting only terminates if the orientation is grounded in a well-founded order (otherwise $\ell \to r$ and $r \to \ell$ could alternate forever), and the rewrite is only sound if the order is stable under the substitutions a branch may still receive. This chapter supplies that order.

The order is NCPO-LNF, the $\beta\eta$-long normal computability path order of Niederhauser and Middeldorp [NM25b], which adapts their NCPO [NM25a] from $\beta\eta$-normal to $\beta\eta$-long normal form and thereby to Nipkow's higher-order rewrite systems. It is a higher-order generalisation of the recursive path orders [Der82] familiar from first-order superposition [BG94], acting directly on typed $\lambda$-terms in $\beta\eta$-long normal form. Numbered definitions, lemmas and theorems cited below are those of [NM25b]. Two design decisions specific to this thesis frame the whole chapter:

• Where the reference implementation leaves the order's parameters (precedences, statuses, accessibility) as unknowns for an SMT solver to discharge while proving a rewrite system terminating, we fix them as inputs and obtain a decidable boolean predicate on a single pair of terms. That is what a tableau prover needs: a yes/no orientation for one equation at a time, in place of a termination certificate for a whole system.
• The prover uses the order at two strengths. The paper's order proper is sound but partial: it may refuse to orient a pair in either direction. That partiality is what gating a rewrite requires, and what choosing a canonical form cannot accept. The prover therefore layers a total heuristic extension over the sound core and keeps the two separate at every call site. The final section states that distinction and how it is enforced, and it is what makes Chapter 3's demodulation sound.

Requirements for an Orientation Order

Recall the two properties a rewrite order carries. Well-foundedness rules out infinite descent, so rewriting to normal form terminates. Stability (closure under substitution) ensures that if $s \succ t$ then $s\theta \succ t\theta$ for every admissible $\theta$, so an orientation decided now survives the substitutions a branch's free variables may still receive under Chapter 6's global reconciliation. In the first-order setting a recursive path order built from a precedence on function symbols delivers both [Der82, BN98]. The higher-order setting breaks the naive lifting in two places: terms carry $\lambda$-binders, so the order must descend under abstraction and handle bound variables; and terms carry types, so the order must respect a companion order on types to stay stable.

NCPO-LNF addresses both. It assumes its inputs are in $\beta\eta$-long normal form, with every subterm fully $\eta$-expanded to its type's arity, which shot_ds already maintains, so the "LNF" precondition holds by construction and no normalisation step is needed before a comparison. Its recursion interleaves a term comparison with a companion type comparison, and it opens $\lambda$-abstractions against fresh variables as it descends.

ShotTo decides the single predicate $s >^1_\tau t$ of Definition 8 of the paper: given two term IDs in the $\beta\eta$-long-normal representation and a %ShotTo.Parameters{} struct, ShotTo.gt?/3 returns a boolean. It is a decision procedure rather than an SMT-constraint generator, which is the contrast the paper's Haskell reference implementation hrsterm draws, and the one this chapter turns on. Because each $\lambda$-opening allocates a fresh shot_ds free variable, the implementation wraps every top-level comparison in a term-factory scratchpad so those variables die when the comparison returns rather than accumulating in the global pool.

The Type Order

The term order is stable only if it defers, at the leaves, to a well-founded order on types. NCPO-LNF uses the admissible type order of the paper's Lemma 4 (itself Lemma 2.3 of the CPO paper [BJR15]).

Definition (Admissible Type Order). Given a well-founded strict precedence $\succ_{\mathcal{S}}$ on base sorts, the admissible type order $\succ_{\mathcal{T}}$ is the smallest strict order on types containing $\succ_{\mathcal{S}}$ and the right-argument relation $(\tau, \bar{\upsilon}) {\to} \varsigma ;\mathrel{\triangleright_r}; \bar{\upsilon} {\to} \varsigma$, and closed under right-congruence: $\bar\upsilon {\to} \varsigma ;\succ_{\mathcal{T}}; \bar{\upsilon}' {\to} \varsigma'$ implies $(\tau, \bar\upsilon) {\to} \varsigma ;\succ_{\mathcal{T}}; (\tau, \bar{\upsilon}') {\to} \varsigma'$ for every $\tau \in \mathcal{T}$.

Intuitively: a function type dominates its own result type, and among two function types with the same argument prefix the one with the greater result type is greater. On base sorts the order is just the user's sort precedence.

ShotTo.TypeOrder implements this directly on the uncurried %Type{goal: a, args: [t1, ..., tn]} representation. type_gt?/3 decides $\succ_{\mathcal{T}}$ and type_geq?/3 its reflexive closure; the base-vs-base case consults Parameters.sort_prec/2, the function case peels the shared leading argument and recurses on the result type. Inside NCPO the comparison enters through type_geq?/3, where the type_check? flag on the internal ncpo/6 predicate toggles whether $\tau(s) \succeq_{\mathcal{T}} \tau(t)$ must hold at a given node, corresponding to the paper's choice between $>^{b,X}$ and $>^{b,X}_\tau$. A term comparison that would otherwise succeed is vetoed when the types disagree the wrong way.

import ShotDs.Hol.Definitions
alias ShotDs.Data.Type
alias ShotTo.{Parameters, TypeOrder}
alias ShotDs.Util.LatexFormatter, as: LF

# iota precedes o at the base level.
params = Parameters.new sort_precedence: %{i: 0, o: 1}

# o > iota at the base sorts (by precedence), and (iota -> o) > (iota -> iota)
# by right-congruence, both in the type order.
"""
| Query                               | Result                              |
| ----------------------------------- | ----------------------------------- |
| $#{LF.format! type_o()} \\succ_\\mathcal{T} #{LF.format! type_i()}$       |\
#{TypeOrder.type_gt? type_o(), type_i(), params}                            |
| $(#{LF.format! type_io()}) \\succ_\\mathcal{T} (#{LF.format! type_ii()})$ |\
#{TypeOrder.type_gt? type_io(), type_ii(), params}                          |
| $#{LF.format! type_i()} \\succ_\\mathcal{T} #{LF.format! type_o()}$       |\
#{TypeOrder.type_gt? type_i(), type_o(), params}                            |
"""
|> Kino.Markdown.new

The third entry is false because $\iota \prec o$: the type order is strict, and $\iota \succ{\mathcal{T}} o$ does not hold._

The Ordering Parameters

A concrete instance of NCPO-LNF is fixed by five pieces of data. Together they are the entire tunable surface of the order, and, as Chapter 8 will exploit, the entire surface the ablation study varies when it studies the order's effect.

Definition (Ordering Parameters). An NCPO-LNF instance is given by:

• a well-founded strict order $\succ_{\mathcal{S}}$ on base sorts;
• a precedence $\succsim_{\mathcal{F}}$ on constants, with strict part $\succ_{\mathcal{F}}$ and equivalence $\simeq_{\mathcal{F}}$;
• a status $\mathrm{stat}(f) \in {\mathsf{lex}, \mathsf{mul}}$ per constant, selecting lexicographic or multiset comparison of argument lists under equal heads;
• a basicness predicate $\mathrm{basic}(a)$ on base sorts;
• an accessibility predicate $\mathrm{Acc}(f, i)$ on argument positions.

The first three are the familiar RPO parameters lifted to the typed higher-order setting. Basicness and accessibility are the higher-order additions: they control the computability machinery, meaning which subterms may be descended into while preserving stability, and their soundness depends on compatibility conditions (the paper's Definitions 5 & 6) relating them to the type precedence.

Status is the parameter whose usable settings the LNF restriction changes, and the paper's own examples show it. The symbolic differentiation rules of [NM25a], carried over as Example 6 of [NM25b], are oriented there with every symbol given multiset status. That assignment stops working once heads are saturated. With $\operatorname{ar}(\mathrm{diff}) = 2$ the partial application $\mathrm{diff}(F)$ is stored as $\lambda r., \mathrm{diff}(F, 1)$, so after $\langle\lambda{=}\rangle$ peels the outer binder the recursive goal compares two argument pairs whose second components are unrelated fresh variables, and no multiset comparison relates those. Lexicographic status walks the arguments left to right and decides at the first position, leaving a goal $\langle\mathcal{FX}\rangle$ discharges. Only $\mathrm{diff}$'s status matters, which is what the third row below shows.

import ShotDs.Hol.Sigils
alias ShotTo.Parameters

diff_rules =
  with_context ~e[F: r>r, G: r>r, sin: r>r, cos: r>r,
                  diff: (r>r)>r>r, times: (r>r)>(r>r)>r>r,
                  plus: (r>r)>(r>r)>r>r], fn ->
    [
      {~g{ diff @ (^[X: r]: (sin @ (F @ X))) },
       ~g{ times @ (^[X: r]: (cos @ (F @ X))) @ (diff @ F) }},
      {~g{ diff @ (times @ F @ G) },
       ~g{ plus @ (times @ (diff @ F) @ G) @ (times @ F @ (diff @ G)) }}
    ]
  end

prec_diff = %{"diff" => 1, "sin" => 0, "cos" => 0, "plus" => 0, "times" => 0}

statuses = [
  {"all mul", fn _ -> :mul end},
  {"all lex", fn _ -> :lex end},
  {"diff lex, rest mul", fn name -> if name == "diff", do: :lex, else: :mul end}
]

rows =
  Enum.map_join(statuses, "\n", fn {label, status} ->
    params = Parameters.new const_precedence: prec_diff, status: status
    cells = Enum.map_join(diff_rules, " | ", fn {l, r} -> "`#{ShotTo.gt? l, r, params}`" end)
    "| #{label} | #{cells} |"
  end)

Kino.Markdown.new("| status | rule 1 | rule 2 |\n| :-- | :-- | :-- |\n" <> rows)

ShotTo.Parameters holds these as sort_precedence, const_precedence, status, basic_sorts, and accessible. Each accepts a map, a MapSet, or a predicate function, so a caller can be as coarse or as fine-grained as needed. Precedences are given as integer ranks: larger means greater, equal means $\simeq_{\mathcal{F}}$. The lookup helpers prec/2, sort_prec/2, status/2, basic?/2, accessible?/3, together with gt?/3 and equiv?/3 on constants, are what the core predicate calls.

Note that ShotTo's own defaults are permissive to the point of uselessness: all sorts basic and equivalent, all positions accessible, all constants equivalent with :lex status. Under them NCPO collapses to the bare subterm order plus lexicographic comparison inside shared heads and almost nothing is oriented. The defaults are chosen this way so the API is usable without further configuration while every meaningful orientation forces the caller to supply at least a constant precedence. A caller that forgot to configure the order would find demodulation silently doing nothing, not silently doing something unsound.

The prover is such a caller, and it supplies exactly that one parameter. ShotTx.Data.Parameters carries term_order: %ShotTo.Parameters{const_precedence: &:erlang.phash2/1}: every constant name gets a stable hash-based rank, so the precedence is total and well-founded on symbols and NCPO-LNF can orient equations between arbitrary distinct constants, including parameters introduced by $\delta$-expansion, which carry no name by which they could be ranked. Status, basicness and accessibility stay at their permissive defaults. A user-supplied map or function overrides the whole struct.

Moreover, on soundness of the parameters themselves: NCPO-LNF's stability depends on $\mathrm{Acc}$ and $\mathrm{basic}$ satisfying the compatibility conditions with the chosen type precedence. ShotTo does not enforce these, leaving them to the caller, but offers Parameters.validate/2 as a best-effort check, and documents a vacuously sound fallback: leaving accessible: :all and basic_sorts: :all makes the compatibility conditions hold trivially, at the cost of a more conservative (weaker) order. The prover takes this conservative-but-safe route, which is the right trade for a soundness-critical component.

The Order

With types and parameters in place, the term order is a mutual recursion over the shapes of the two terms. Rather than the full rule set of Definition 8, we name the rules that fire and let the implementation stand as the precise statement.

The comparison $s >^1_\tau t$ first checks $\tau(s) \succeq_{\mathcal{T}} \tau(t)$, then dispatches on the shape of $s$:

• $s$ has a constant head $f(\bar{t})$. Three families of rules apply in order. $\langle \mathcal{FX} \rangle$ closes immediately if $t$ is one of the fresh variables introduced while descending under a $\lambda$ on the right. $\langle \mathcal{F}\triangleright\rangle$ succeeds if some argument $t_i$ of $s$ already dominates $t$ through the accessible-subterm relation, the higher-order rule that a term is greater than its subterms, routed through accessibility and basicness. Failing those, the comparison dispatches on $t$:
  • against another constant head $g(\bar{u})$: if $f \simeq_{\mathcal{F}} g$ with equal status, compare the argument lists by that status ($\langle \mathcal{F}{=}\mathsf{lex}\rangle$ / $\langle \mathcal{F}{=}\mathsf{mul}\rangle$); if $f \succ_{\mathcal{F}} g$, require $s$ to dominate every argument of $t$ ($\langle \mathcal{F}{\succ}\rangle$);
  • against a variable-headed $y(\bar{u})$: the $\langle \mathcal{FV}\rangle$ rule, which fires only at the top recursion level, requiring $s$ to dominate the $\eta$-expanded head and each argument;
  • against an abstraction $\lambda \tau.,v$: the $\langle \mathcal{F}\lambda\rangle$ rule opens $t$ on a fresh variable added to the auxiliary set and recurses.
• $s$ is an abstraction $\lambda \tau.,u$. The $\langle\lambda\triangleright\rangle$ rule opens $s$ and checks whether its body already dominates $t$; otherwise, if $t$ is also an abstraction, $\langle\lambda{=}\rangle$/$\langle\lambda{\neq}\rangle$ align the two binders (reusing the same fresh variable when their types agree) and recurse.
• $s$ is variable-headed. No rule makes a variable-headed term greater than anything; the order never orients out of a flex term, which is what keeps it stable under the substitutions those variables may receive.

ShotTo.Ncpo.ncpo_gt?/3 is the entry point; the internal ncpo/6 carries the paper's two extra parameters explicitly: the level $b \in {0,1}$ (some rules, among them $\langle\mathcal{FV}\rangle$, fire only at $b = 1$) and the auxiliary variable set $X$ that accumulates the fresh variables introduced by $\lambda$-openings. The rule names above match the implementation's private functions (fx_rule?, f_subterm_rule?, ncpo_ff_case, ncpo_fv_rule, ncpo_flam_rule, ncpo_lam_head) and the computability helpers bawo/awo/sswo mirror the auxiliary relations of the reference. The last bullet is enforced structurally: dispatch_on_s returns false whenever $s$'s head is not a constant and $s$ is not an abstraction.

Two worked comparisons. First the subterm rule (a term is greater than a constant nested in its arguments) which needs only a constant precedence:

import ShotDs.Hol.{Definitions, Sigils, Dsl}
alias ShotDs.Stt.TermFactory, as: TF
alias ShotDs.Util.LatexFormatter, as: LF
alias ShotTo.Parameters

prec = Parameters.new const_precedence: %{"f" => 1, "c" => 0}

f = const "f", type_ii()
c = const "c", type_i()
fc = app f, c

# f(c) > c by the accessible-subterm rule (c is an accessible subterm);
# the converse fails.
"""
| Query                               | Result                              |
| ----------------------------------- | ----------------------------------- |
| $#{LF.format! fc, hide_types: true} > #{LF.format! c, hide_types: true}$  |\
#{ShotTo.gt? fc, c, prec}                                                   |
| $#{LF.format! c, hide_types: true} > #{LF.format! fc, hide_types: true}$  |\
#{ShotTo.gt? c, fc, prec}                                                   |
"""
|> Kino.Markdown.new

The precedence rule states that a term headed by a greater constant dominates one headed by a lesser, provided it dominates the lesser term's arguments:

import ShotDs.Hol.{Definitions, Dsl}
alias ShotDs.Util.LatexFormatter, as: LF
alias ShotTo.Parameters

# g outranks h in the constant precedence. Then g(c) > h(c) by the precedence
# rule, since g(c) > c handles h's argument.
prec2 = Parameters.new const_precedence: %{"g" => 2, "h" => 1, "c" => 0}

g = const "g", type_ii()
h = const "h", type_ii()
c = const "c", type_i()
gc = app g, c
hc = app h, c

"""
| Query                               | Result                              |
| ----------------------------------- | ----------------------------------- |
| $#{LF.format! gc, hide_types: true} > #{LF.format! hc, hide_types: true}$ |\
#{ShotTo.gt? gc, hc, prec2}                                                 |
| $#{LF.format! hc, hide_types: true} > #{LF.format! gc, hide_types: true}$ |\
#{ShotTo.gt? hc, gc, prec2}                                                 |
"""
|> Kino.Markdown.new

Both examples supply only a constant precedence and rely on the vacuously-sound accessible: :all / basic_sorts: :all defaults, which is the configuration the prover itself uses.

A third comparison is the one the prover actually faces. Chapter 3's Leibniz expansion replaces an equation by a quantification over predicates, so the two sides of that expansion are a pair the order can be asked about: the primitive equality constant at $\iota$ against its Leibniz encoding.

$$ \lambda \iota, \iota.; 2 =!\langle\iota\rangle; 1 \qquad\qquad \lambda \iota, \iota.; \forall \iota {\to} o.; 1(3) \equiv 1(2) $$

import ShotDs.Hol.Definitions
alias ShotTo.Parameters

prim = equals_term type_i()
leibniz = leibniz_equality type_i()

expand = Parameters.new const_precedence: %{"=" => 1}
# "\u2200" is the forall constant, "\u2261" the equivalence constant; written as
# escapes to keep the cell ASCII.
flat = Parameters.new const_precedence: %{"=" => 0, "\u2200" => 1, "\u2261" => 2}

"""
| Precedence                          | `compare/3`                         |
| ----------------------------------- | ----------------------------------- |
| $= \\succ_\\mathcal{F} \\forall, \\equiv$                                 |\
`#{inspect ShotTo.compare(prim, leibniz, expand)}`                          |
| $\\equiv \\succ_\\mathcal{F} \\forall \\succ_\\mathcal{F} =$              |\
`#{inspect ShotTo.compare(prim, leibniz, flat)}`                            |
"""
|> Kino.Markdown.new

With $=$ above the connectives the encoding introduces, the pair is oriented left to right, so the expansion may be used as a rewrite and rewriting with it terminates. Reversing the precedence yields :incomparable rather than the opposite orientation, since contracting the encoding back to $=$ would raise the head's rank without decreasing anything else. Orientability of a definitional expansion is therefore a property of the precedence, and the precedence does not make the contraction available by being reversed.

The prover's own precedence is &:erlang.phash2/1, which ranks $=$ at $25{,}810{,}966$ and $\forall$ at $106{,}440{,}513$, so under the default parameters this pair is :incomparable and the expansion is not available as a rewrite. Whether any particular definitional expansion is orientable is thus arbitrary under the default, though stable across runs, and a user who wants a specific expansion oriented has to supply a precedence that puts its head symbol on top. Nothing in Chapter 3 depends on this: Leibniz expansion is a tableau rule with its own cost, and the order gates demodulation alone.

No Transitivity: One Pair at a Time

An important caveat, because it shapes how the prover is allowed to use the order: NCPO-LNF is not (yet known to be) transitive [NM25a]. It is well-founded and stable, the two properties a reduction order needs, but transitivity is an open question. The practical consequence is sharp: the order may be used to decide the orientation of one pair at a time, but must not be used as a comparator to sort a list of terms or to build a total order over a set, because sorting silently assumes transitivity. ShotTo's public surface reflects this: it offers gt?/3, geq?/3, and a four-valued compare/3, but no sort and no claim of a total order.

The limitation is a property of the order and cannot be avoided by the prover. What the prover can do is confine every use to pairwise orientation decisions, which is all demodulation and connective normalisation actually require. The next section is how that confinement is arranged.

The Total Prover-Side Wrapper

The paper's order is sound but partial: for many pairs it answers neither $s \succ t$ nor $t \succ s$. ShotTo.compare/3 reports this as a fourth verdict, :incomparable, alongside :greater, :less, and :equal. Partiality is appropriate when the question is whether $\ell$ may be rewritten to $r$, since the safe answer for an incomparable pair is to block the rewrite, and unhelpful when the question is which of two commutative arguments is the canonical left, where any deterministic answer suffices. ShotTx.Prover.TermOrder addresses both cases with two separated layers.

The sound layer. strict_gt?/3 is a direct passthrough to ShotTo.gt?/3, NCPO-LNF unmodified. By the paper's Theorem 2 the pair (NCPO-LNF, CPO) is a $\beta\eta$-normal higher-order reduction order: well-founded on $\beta\eta$-long-normal terms, monotone, and stability-compatible under $\beta\eta$-long-normal substitutions. This is the only decision suitable for gating a rewrite. It may return false both ways for the same pair, and every caller must be prepared to block the step in that case.

This is what Chapter 3's demodulation relies on. ShotTx.Prover.Demodulation rewrites a subterm to an equation's right-hand side only when TermOrder.strict_gt?(lhs, rhs, order) holds. Every rewrite step strictly decreases the term in a well-founded order, so rewriting to normal form terminates, and equations that fail the strict gate contribute no rewrite rule at all (demodulation.ex). The termination argument is therefore a local invariant enforced at each rewrite rather than an external claim about the prover. The order is one of the two independent filters on Chapter 3's $\mathcal{E}(B)$; the other, groundness, is a refutational condition and has nothing to do with the order.

The heuristic layer. compare/3 and gt?/3 wrap ShotTo.compare/3 and, only on :incomparable, break the tie deterministically, first by alphabetic order on the printed term, then by the raw integer term IDs. The result is total and decidable, but is not in general a reduction order: it is not guaranteed well-founded or monotone. Its sole use is to pick a canonical direction where any consistent choice suffices, and it must never gate a rewrite.

The prover uses this heuristic layer in exactly two places, both cosmetic. orient_pair in branch.ex stores an equation $\ell = r$ by trying strict_gt? in each direction first, and only if both fail falls back to the heuristic gt? to pick a storage direction. The connective-canonicalisation cases ($\lor$, $\land$, $\equiv$, $=$) use gt? purely to decide whether to swap the two sides into a fixed order; that pass is governed by the orient parameter. :none (the default) skips it entirely, :shallow normalises only each formula's outermost connective, :deep recurses bottom-up through every nested commutative connective, including those inside atom arguments. In both places the choice affects which syntactic representative is stored, never whether a logically-significant rewrite fires. Conflating the two layers would be the classic superposition bug: orienting a rewrite by a non-well-founded relation, and losing termination. Keeping them apart should keep demodulation sound.

The two layers can be made to diverge. Under a precedence that leaves two unrelated constants incomparable, the sound layer refuses to orient the pair while the heuristic layer still returns a deterministic direction:

alias ShotTx.Prover.TermOrder
alias ShotTo.Parameters
import ShotDs.Hol.{Definitions, Dsl}

# a and b are equivalent in precedence (both rank 0) and unrelated by
# structure, so NCPO-LNF cannot orient {a, b} either way.
flat = Parameters.new const_precedence: %{"a" => 0, "b" => 0}

a = const "a", type_i()
b = const "b", type_i()

[
  :sound_a_gt_b, TermOrder.strict_gt?(a, b, flat),
  :sound_b_gt_a, TermOrder.strict_gt?(b, a, flat),
  :heuristic_compare, TermOrder.compare(a, b, flat)
]
|> Kino.Layout.grid(columns: {1, 1})

:sound_a_gt_b

false

:sound_b_gt_a

false

:heuristic_compare

:less

Both strict_gt? queries are false. NCPO-LNF declines to orient the pair, so demodulation between $a$ and $b$ is correctly blocked. The heuristic compare still returns :less (here by alphabetic tie-break, $a < b$), which is fine for choosing a canonical connective side and would be unsound as a rewrite gate.

Summary and Forward Pointers

NCPO-LNF gives the tableau a higher-order reduction order that is well-founded and stable, enough to make demodulation terminating and sound. The order is decided pairwise as a boolean predicate over fixed parameters rather than solved as an SMT termination problem. The prover consumes it at two strengths: the sound, partial strict_gt? gates every rewrite, and a total heuristic extension is confined to cosmetic orientation of commutative connectives. Its main open problem, non-transitivity, is contained by only ever asking pairwise questions.

Why the stability property is required rather than incidental is shown in Chapter 6: because branch-level rules never commit free-variable substitutions and the substitution arrives only later, from global reconciliation, an orientation decided on a branch must survive that late substitution. Chapter 8's ablation study varies the parameters of this order (constant precedence, status, the accessibility and basicness fallbacks) among its parameters, measuring how much orientation strength the prover actually needs.

Chapter References

• [BG94] Leo Bachmair and Harald Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217–247, 1994.
• [BJR15] Frédéric Blanqui, Jean-Pierre Jouannaud, and Albert Rubio. The computability path ordering. Logical Methods in Computer Science, 11(4:3), 2015.
• [BN98] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
• [Der82] Nachum Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279–301, 1982.
• [NM25a] Johannes Niederhauser and Aart Middeldorp. The computability path order for $\beta\eta$-normal higher-order rewriting. In Automated Deduction (CADE-30), LNCS 15943, pages 207–225. Springer, 2025.
• [NM25b] Johannes Niederhauser and Aart Middeldorp. NCPO goes $\beta\eta$-long normal form. In Proceedings of the 20th International Workshop on Termination (WST 2025), Leipzig, Germany, 2025. Informal proceedings.

Previous: Chapter 4: Higher-Order Unification  $\cdot$  Contents  $\cdot$  Next: Chapter 6: A Concurrent Actor-Based Architecture