# `ShotTo`
[🔗](https://github.com/jcschuster/ShotTo/blob/v0.1.0/lib/shot_to.ex#L1)

`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

# `compare`

```elixir
@spec compare(ShotDs.Data.Term.term_id(), ShotDs.Data.Term.term_id()) ::
  :greater | :less | :equal | :incomparable
```

Compares two term IDs in NCPO-LNF. Returns

  * `:greater`      if `s > t`,
  * `:less`         if `t > s`,
  * `:equal`        if the terms are structurally equal (same term ID), and
  * `:incomparable` otherwise.

Because NCPO-LNF is not (yet known to be) transitive, the `:incomparable`
case is a genuine possibility even for terms that intuitively "ought to
be" comparable under some total ordering.

Two NCPO-LNF calls are made in the worst case (once in each direction).
Both are run inside a single scratchpad so intermediate fresh variables
are collected together.

# `compare`

```elixir
@spec compare(
  ShotDs.Data.Term.term_id(),
  ShotDs.Data.Term.term_id(),
  ShotTo.Parameters.t()
) ::
  :greater | :less | :equal | :incomparable
```

# `geq?`

```elixir
@spec geq?(ShotDs.Data.Term.term_id(), ShotDs.Data.Term.term_id()) :: boolean()
```

Returns `true` iff `s ⪰^1_τ t` in NCPO-LNF, i.e. either the two terms are
(structurally, thanks to ETS memoisation: referentially) equal or
`s >^1_τ t`.

# `geq?`

```elixir
@spec geq?(
  ShotDs.Data.Term.term_id(),
  ShotDs.Data.Term.term_id(),
  ShotTo.Parameters.t()
) :: boolean()
```

# `gt?`

```elixir
@spec gt?(ShotDs.Data.Term.term_id(), ShotDs.Data.Term.term_id()) :: boolean()
```

Returns `true` iff `s >^1_τ t` in NCPO-LNF under the given parameters.

`s_id` and `t_id` are term IDs as produced by `ShotDs.Stt.TermFactory`.

With no parameters supplied, the default (permissive) parameter set is
used; see `ShotTo.Parameters` for details on the defaults.

# `gt?`

```elixir
@spec gt?(
  ShotDs.Data.Term.term_id(),
  ShotDs.Data.Term.term_id(),
  ShotTo.Parameters.t()
) :: boolean()
```

---

*Consult [api-reference.md](api-reference.md) for complete listing*