ShotTo provides a decidable instance of the βη-long-normal Computability Path Order (NCPO-LNF) of Niederhauser and Middeldorp (NCPO goes Beta-Eta-Long Normal Form, 2025) for terms of Church's simple type theory as represented by the shot_ds library.

The order is parameterised by a sort precedence, a constant precedence with associated statuses and accessibility, and a choice of basic sorts; see ShotTo.Parameters. Given a fixed choice of parameters the relation s > t is a decidable boolean predicate that ShotTo implements directly rather than as an SMT constraint, making it suitable for use as an orientation order inside tableau and other proof-search procedures.

Status

As of the date of the paper, NCPO-LNF is not known to be transitive; the authors prove only the properties needed for termination of higher-order rewrite systems (well-foundedness, monotonicity, βη-long-normal stability). ShotTo is therefore best used pairwise — to decide whether one term should be oriented above another — rather than as the basis of a total comparator over a collection of terms. Using it as a key for sorting in particular may give surprising results until transitivity is established.

Example

iex> import ShotDs.Hol.Definitions
iex> alias ShotDs.Stt.TermFactory, as: TF
iex> alias ShotTo.Parameters
...>
iex> # Constants f and c of base type i, with f > c in precedence.
iex> params = Parameters.new(const_precedence: %{"f" => 1, "c" => 0})
iex> f = TF.make_const_term("f", Type.new(:i, :i))
iex> c = TF.make_const_term("c", type_i())
iex> fc = ShotDs.Hol.Dsl.app(f, c)
...>
iex> # f(c) > c by ⟨F▷⟩ (c is a subterm of f(c)).
iex> ShotTo.gt?(fc, c, params)
true
iex> ShotTo.gt?(c, fc, params)
false