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

Implementation of NCPO-LNF (the βη-long-normal Computability Path Order).

Entry point: `ncpo_gt?/3` decides whether `s >^1_τ t` for two term IDs in
the βη-long normal representation provided by
`ShotDs.Stt.TermFactory`. This is the order referred to as `>_τ^1`
(`NCPO-LNF`) in Definition 8 of Niederhauser & Middeldorp,
*NCPO goes Beta-Eta-Long Normal Form*, 2025.

The internal predicate `ncpo/6` implements the parameterised relation
`>^{b,X}` (with a boolean `type_check?` toggling whether the type
comparison `τ(s) ⪰_T τ(t)` is included, corresponding to the choice
between `>^{b,X}` and `>^{b,X}_τ`). The helpers `bawo`, `awo`, `sswo`,
`mul_ext?`, and `lex_ext?` mirror the ones in `OrderingLnf.hs` of the
Haskell reference (`https://github.com/niedjoh/hrsterm`).

> ## Note {:.info}
>
> Callers that care about the size of the global ETS term pool should
> invoke `ShotDs.Stt.TermFactory.with_scratchpad/1` (or
> `with_scratchpad!`) around their calls; the fresh variables generated
> during a comparison will then be collected when the scratchpad exits.

# `b`

```elixir
@type b() :: 0 | 1
```

The inductive-rule level parameter `b ∈ {0, 1}` of Definition 8.

# `x_set`

```elixir
@type x_set() :: MapSet.t(ShotDs.Data.Declaration.t())
```

Auxiliary variable set `X` of Definition 8. Each element is a fresh
`ShotDs.Data.Declaration.free_var_t()` generated by lambda-opening.

# `ncpo_gt?`

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

Decides `s >^1_τ t`, i.e. whether the left term is strictly greater than
the right in NCPO-LNF with the given parameters.

Wraps the computation in a scratchpad (if none is active) so that the
fresh variables introduced by lambda-opening do not pollute the global
ETS table.

---

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