ShotTo

Copy Markdown View Source

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

ShotTo is developed at the University of Bamberg, Chair for AI Systems Engineering, primarily as an orientation order for a higher-order tableau prover.

What it does

Given two terms s and t in βη-long normal form and a choice of ordering parameters, ShotTo decides the boolean predicate $s >^1_\tau t$ of Definition 8 of the paper. It is a drop-in decision procedure rather than an SMT-constraint generator: the parameters (precedences, statuses, accessibility, basicness) are fixed inputs supplied by the caller, not unknowns.

import ShotDs.Hol.Dsl
import ShotDs.Hol.Definitions
alias ShotDs.Stt.TermFactory, as: TF
alias ShotTo.Parameters

params = Parameters.new(const_precedence: %{"f" => 1, "c" => 0})
f  = TF.make_const_term("f", Type.new(:i, :i))
c  = TF.make_const_term("c", type_i())
fc = app(f, c)

ShotTo.gt?(fc, c, params)       # => true   (by ⟨F▷⟩: c is a subterm of f(c))
ShotTo.gt?(c, fc, params)       # => false
ShotTo.compare(fc, c, params)   # => :greater

API surface

ShotTo

  • gt?(s_id, t_id, params \\ default) — decides $s >^1_\tau t$.
  • geq?(s_id, t_id, params \\ default) — reflexive closure.
  • compare(s_id, t_id, params \\ default) — returns :greater, :less, :equal, or :incomparable.

ShotTo.Parameters

A struct with fields

  • sort_precedence — map or function on atoms giving the rank of each base sort (higher is greater in $\succ_{\mathcal{S}}$).
  • const_precedence — map or function on constant identifiers giving the rank in $\succ_{\mathcal{F}}$.
  • status — map or function assigning :lex or :mul to each constant.
  • basic_sorts — :all, a MapSet, or a predicate.
  • accessible — :all, a MapSet of {name, index} pairs, or a binary predicate.

Helpers:

  • Parameters.new/1, Parameters.from_precedence_list/2, and lookup functions prec/2, sort_prec/2, status/2, basic?/2, accessible?/3, equiv?/3, gt?/3.
  • Parameters.validate/2 for a best-effort sanity-check against a map of constant types.

Defaults are permissive: all sorts equivalent and basic, all positions accessible, all constants equivalent with :lex status. Under these defaults NCPO-LNF reduces to the simple subterm order plus lexicographic-in-the-same-head comparison, which is rarely what you want; at a minimum supply a const_precedence.

Status and caveats

  • NCPO-LNF is not (yet known to be) transitive. Use ShotTo to decide orientation of one pair at a time, not as a comparator for sorting or for building total orders on sets of terms.
  • ShotTo.Parameters.validate/2 is a best-effort check of the accessibility and basicness conditions (Definition 5 of the paper). A sound but conservative choice is to leave accessible: :all and basic_sorts: :all — the conditions then hold vacuously.
  • Every lambda opening allocates a fresh ShotDs free variable. Callers concerned with global ETS growth should wrap their comparisons in ShotDs.Stt.TermFactory.with_scratchpad!/1; fresh variables generated during the comparison will then die with the scratchpad.

Installation

Add shot_to to your dependencies:

def deps do
  [
    {:shot_to, "~> 0.1"}
  ]
end

License

MIT.