ShotUn (shot_un v0.1.7)

Copy Markdown View Source

Higher-order unification for the data structures and semantics of ShotDs.

Three algorithms are available:

  • unify/3 (default) — depth-bounded pre-unification (Huet 1975): handles arbitrary higher-order problems but is a semi-decision procedure; flex-flex pairs are returned as constraints.
  • pattern_unify/2 — Miller pattern unification (Miller 1991): a decidable, unitary fragment in which every flex variable is applied only to distinct bound variables. Returns at most one MGU.
  • match/2 — Huet second-order matching: the right-hand side is ground, every variable in the problem has type of order ≤ 2. Returns the complete (lazy) stream of matchers without a depth bound.

unify/3 accepts a :strategy option (:pre_unification, :auto, :pattern, :matching). With :auto, the problem is inspected and routed to the most specific decidable algorithm it falls into:

  • if every pair is a pattern → pattern_unify/2,
  • otherwise if it satisfies the matching precondition → match/2,
  • otherwise pre-unification.

See ShotUn.Pattern, ShotUn.Matching and ShotUn.Fragment for details on the individual algorithms and the fragment classifiers.

Visualisation

Every public entry point accepts a vis: true option that wraps the result in a {result, %ShotUn.Trace{}} tuple. The trace is a tree of ShotUn.Trace.Node records covering only the paths from the initial state to a :solution leaf — failed branches and dead-end steps are pruned out before the tuple is returned. Render with ShotUn.Trace.Mermaid.render/2. When vis: true the search is materialised eagerly (the lazy Stream is consumed before the call returns) so that the trace is complete.

Summary

Types

strategy()

Functions

match(pairs, opts \\ [])

Returns the (lazy) stream of all matchers σ such that σ(s) ≡_βη t for each pair {s, t}. With vis: true, returns {stream, trace}. Equivalent to ShotUn.Matching.match/2.

pattern_unify(pairs, opts \\ [])

Returns {:ok, %UnifSolution{}} (or :error) for a problem in Miller's pattern fragment. With vis: true, returns {result, trace}. Equivalent to ShotUn.Pattern.unify/2.

unify(term_pairs, depth \\ 10, opts \\ [])

Solves a higher-order unification problem.

Types

strategy()

@type strategy() :: :pre_unification | :auto | :pattern | :matching

Functions

match(pairs, opts \\ [])

@spec match(
  [term_pair()] | term_pair(),
  keyword()
) ::
  Enumerable.t(ShotUn.UnifSolution.t())
  | {Enumerable.t(ShotUn.UnifSolution.t()), ShotUn.Trace.t()}

Returns the (lazy) stream of all matchers σ such that σ(s) ≡_βη t for each pair {s, t}. With vis: true, returns {stream, trace}. Equivalent to ShotUn.Matching.match/2.

pattern_unify(pairs, opts \\ [])

@spec pattern_unify(
  [term_pair()] | term_pair(),
  keyword()
) ::
  {:ok, ShotUn.UnifSolution.t()}
  | :error
  | {{:ok, ShotUn.UnifSolution.t()} | :error, ShotUn.Trace.t()}

Returns {:ok, %UnifSolution{}} (or :error) for a problem in Miller's pattern fragment. With vis: true, returns {result, trace}. Equivalent to ShotUn.Pattern.unify/2.

unify(term_pairs, depth \\ 10, opts \\ [])

@spec unify([term_pair()] | term_pair(), non_neg_integer(), keyword()) ::
  Enumerable.t(ShotUn.UnifSolution.t())
  | {Enumerable.t(ShotUn.UnifSolution.t()), ShotUn.Trace.t()}

Solves a higher-order unification problem.

Accepts a single term pair {l, r} or a list of pairs. depth is the search-depth budget for the pre-unification fragment; it is ignored by the matching and pattern strategies. opts accepts:

  • :strategy — one of :pre_unification (default), :auto, :pattern, :matching. See module docs for dispatch rules.
  • :vis — when true, returns {stream, %ShotUn.Trace{}} instead of a bare stream. Defaults to false.

Returns a lazy Stream of ShotUn.UnifSolution structs, or — under vis: true — a {stream, trace} tuple in which the stream contains the same solutions but is fully materialised before the call returns.