Parameters that define a concrete instance of NCPO-LNF.
NCPO-LNF is parameterised by the following data (see Definition 8 and the surrounding text in Niederhauser & Middeldorp, NCPO goes Beta-Eta-Long Normal Form, 2025):
- A well-founded strict order
≻_Son base sorts (atoms). The admissible type order≻_Tused inside NCPO is derived from this by Lemma 4. - A precedence
≿_Fon function symbols (constants) with a well-founded strict part≻_Fand equivalence≃_F. - A status
stat(f) ∈ {:mul, :lex}for each constant. - A predicate
basic(a)selecting which base sorts are basic. - An accessibility predicate
Acc(f, i)selecting which argument positions of each constant are accessible.
For the Haskell reference, these are unknowns decided by an SMT solver so
that termination of an entire rewrite system can be proven. In ShotTo
we take them as fixed inputs and obtain a decidable boolean predicate on
pairs of terms, which is what a tableau prover or equational-reasoning
engine typically needs.
Defaults
The default parameter set is deliberately permissive: all sorts are
basic and equivalent, all positions are accessible, all constants are
equivalent in precedence with :lex status. Under these defaults NCPO
reduces to the simple argument-subterm order together with lexicographic
comparison inside shared heads, which is rarely what a user wants — the
point is to make the API usable out of the box and to make it explicit
that every meaningful orientation requires the user to supply at least
a constant precedence.
Validity of parameters
Soundness of NCPO-LNF depends on Acc and basic satisfying the
compatibility conditions of Definitions 5 & 6 with respect to the chosen
type precedence. ShotTo does not currently check these conditions — it
trusts the caller. ShotTo.Parameters.validate/2 gives a best-effort
check for a given set of constants; callers who need a soundness
guarantee should either invoke it or default to accessible: :all and
basic_sorts: :all, which are vacuously sound (the compatibility
conditions become trivial when every position is accessible and every
sort is basic).
Summary
Types
Which argument positions of which constants are accessible. :all
treats every position as accessible. A MapSet contains {const_id, index} tuples. A predicate function is also accepted.
Argument position, counted from 1.
Which sorts are basic. :all treats every sort as basic. A MapSet
explicitly lists the basic sorts. A predicate function is also accepted.
Identifier for a constant as used in ShotDs.Data.Declaration.name. In
practice either a binary name or an Erlang reference (for generated
constants).
Constant precedence. Either a map from constant identifiers to integers
(larger integer means greater in ≻_F; equal integers mean ≃_F), or a
one-argument function with the same meaning.
Identifier for a base sort, corresponding to ShotDs.Data.Type.type_id
with the type-variable case excluded: an atom such as :i, :o, etc.
Sort precedence. Either a map from sort identifiers to integers or a one-argument function with the same meaning.
Symbol status.
Status assignment. Either a map or a one-argument function.
Functions
Returns true if the 1-based argument position i of the constant
identified by name is declared accessible.
Returns true if the given base sort is declared basic.
Returns true if name1 and name2 are equivalent in ≃_F.
Convenience: builds parameters from a total precedence given as an
ordered list, most-greater first. Each constant is placed at the rank
corresponding to its position (so the first element in the list is
strictly greater than the rest). Constants not listed are assigned rank
0 by default lookup.
Returns true if name1 is strictly greater than name2 in ≻_F.
Builds a parameter struct. All keys are optional; unspecified fields fall back to the permissive defaults described in the module docs.
Looks up the precedence rank of a constant. Defaults to 0 for unknown
constants, which makes unknown constants equivalent to each other and to
any other rank-0 constant.
Looks up the precedence rank of a sort. Defaults to 0 for unknown sorts.
Looks up the status of a constant. Defaults to :lex for unknown constants.
Best-effort validity check for Acc and basic against the types of a
given set of constants. Returns :ok if no violations were found, or
{:error, violations} with a list of human-readable strings describing
the issues.
Types
@type accessible() :: :all | MapSet.t({const_id(), arg_index()}) | (const_id(), arg_index() -> boolean())
Which argument positions of which constants are accessible. :all
treats every position as accessible. A MapSet contains {const_id, index} tuples. A predicate function is also accepted.
@type arg_index() :: pos_integer()
Argument position, counted from 1.
Which sorts are basic. :all treats every sort as basic. A MapSet
explicitly lists the basic sorts. A predicate function is also accepted.
Identifier for a constant as used in ShotDs.Data.Declaration.name. In
practice either a binary name or an Erlang reference (for generated
constants).
Constant precedence. Either a map from constant identifiers to integers
(larger integer means greater in ≻_F; equal integers mean ≃_F), or a
one-argument function with the same meaning.
@type sort_id() :: atom()
Identifier for a base sort, corresponding to ShotDs.Data.Type.type_id
with the type-variable case excluded: an atom such as :i, :o, etc.
Sort precedence. Either a map from sort identifiers to integers or a one-argument function with the same meaning.
@type status() :: :lex | :mul
Symbol status.
Status assignment. Either a map or a one-argument function.
@type t() :: %ShotTo.Parameters{ accessible: accessible(), basic_sorts: basic_sorts(), const_precedence: const_precedence(), sort_precedence: sort_precedence(), status: status_map() }
Functions
Returns true if the 1-based argument position i of the constant
identified by name is declared accessible.
Returns true if the given base sort is declared basic.
Returns true if name1 and name2 are equivalent in ≃_F.
Convenience: builds parameters from a total precedence given as an
ordered list, most-greater first. Each constant is placed at the rank
corresponding to its position (so the first element in the list is
strictly greater than the rest). Constants not listed are assigned rank
0 by default lookup.
Inner lists group equivalent constants.
iex> alias ShotTo.Parameters
iex> p = Parameters.from_precedence_list([["f"], ["g", "h"], ["c"]])
iex> Parameters.gt?(p, "f", "g")
true
iex> Parameters.equiv?(p, "g", "h")
true
iex> Parameters.gt?(p, "h", "c")
trueReturns true if name1 is strictly greater than name2 in ≻_F.
Builds a parameter struct. All keys are optional; unspecified fields fall back to the permissive defaults described in the module docs.
Example
iex> alias ShotTo.Parameters
iex> params = Parameters.new(
...> const_precedence: %{"f" => 2, "g" => 1, "c" => 0},
...> status: %{"f" => :lex, "g" => :mul}
...> )
iex> Parameters.prec(params, "f")
2Looks up the precedence rank of a constant. Defaults to 0 for unknown
constants, which makes unknown constants equivalent to each other and to
any other rank-0 constant.
Looks up the precedence rank of a sort. Defaults to 0 for unknown sorts.
Looks up the status of a constant. Defaults to :lex for unknown constants.
@spec validate(t(), %{optional(const_id()) => ShotDs.Data.Type.t()}) :: :ok | {:error, [String.t()]}
Best-effort validity check for Acc and basic against the types of a
given set of constants. Returns :ok if no violations were found, or
{:error, violations} with a list of human-readable strings describing
the issues.
The checks performed:
- For each accessible
{f, i}wheref : T_1 → … → T_n → a, the base sortamust appear only at positive positions ofT_i(approximated here as: every base sort that appears inT_imust beaor less thanain the sort precedence). - For each basic sort
a, every smaller-or-equal sort appearing in an accessible argument type (whose host constant returnsa) must also be basic.
These are the implementation-level approximations of the conditions sketched in Definition 5 and following in the NCPO-LNF paper. They are best-effort: they cover the common cases without attempting the full positive-sort-position analysis of [2, Definition 7.2].