ShotTo.Ncpo (shot_to v0.1.0)

Copy Markdown View Source

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

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.

Summary

Types

b()

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

x_set()

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

Functions

ncpo_gt?(s_id, t_id, params)

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

Types

b()

@type b() :: 0 | 1

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

x_set()

@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.

Functions

ncpo_gt?(s_id, t_id, params)

@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.