ShotUn.Matching (shot_un v0.1.9)

Decidable higher-order matching for the second-order fragment.

Higher-order matching is the task of finding a substitution σ such that σ(s) ≡βη t for two given terms s and t where t is _ground (contains no free variables). General higher-order matching is decidable (Stirling 2009) but impractical to implement; this module restricts to Huet's second-order fragment, where every variable and constant in the problem has a type of order at most 2.

Termination is guaranteed by a structural argument on the multi-set of right-hand sides: every imitation step strictly decreases the total size of the targets, and every projection step eliminates a flex variable without introducing new ones (for order-1 flex arguments) or introduces strictly-smaller-order metas (for order-2 flex arguments). No depth bound is needed.

Inputs that violate the second-order or ground-target preconditions raise ArgumentError.

Pass vis: true in opts to receive a {stream, %ShotUn.Trace{}} tuple instead of a bare stream. Under vis: true the stream is materialised eagerly so the trace is complete on return.

Summary

Functions

match(pair_or_pairs, opts \\ [])

Returns the lazy stream of all matchers for the given problem.

Functions

match(pair_or_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 for the given problem.

Raises ArgumentError if any right-hand side has free variables, or if any type in the problem has order greater than 2.

opts:

:vis — when true, returns {stream, %ShotUn.Trace{}}. The stream is materialised eagerly. Defaults to false.