ShotTx.Prover.Branch (ShotTx v0.0.3)

Pure functional core representing a single branch in the proof tree. Applies rules and returns the resulting state and any intended side-effects (Outbox pattern) for the stateful Worker to execute.

History format

Each history entry is a triple {source | nil, rule, [produced_id]}:

source — term id of the formula that was processed. Reinserted gamma /

         prim_subst rules carry the originating formula's id through the
         queue, so every entry is tagged with a real parent.

rule — the classified rule tuple from Rules.

produced — term ids of the formulas that this rule spawned onto the

         branch. For beta / `instantiate`, the produced list mirrors the
         sibling branches.

History is recorded inside apply_rule/6 after the rule runs, so the produced list is exact and {:closed, branch} carries a branch whose history includes the closing step.

Equality handling

Every formula added to the branch is run through insert_formula/5. This preserves the existing decomposition of equality via the :equality_expansion rule (Leibniz / extensional / o-type iff) and additionally invokes ShotTx.Prover.Demodulation at two points:

Forward demodulation — maybe_demodulate/3 inside insert_formula/5 reduces every incoming term to normal form under the current branch.equations before it lands on the queue.
Backward demodulation — when ingest_equation/4 records a new equation, backward_demodulate/3 re-normalizes every existing branch literal under the enlarged equation set and discards any that changed.

Only rewrites whose matcher σ is the empty substitution are admitted (the equation LHS must be structurally identical to the target subterm, or a primitive η-expansion λv̄. h(v̄) matching an applied subterm's head declaration). No variable is ever bound at the branch level; free-variable commitments are reconciled globally by ShotTx.Prover.ContradictionAgent. See ShotTx.Prover.Paramodulation's moduledoc for the soundness argument.

The :instantiate rule additionally performs dual instantiation: the source literal is treated as an atom on the branch in addition to the lazily-instantiated variants being branched on.

Summary

Types

effect()

history_entry()

step_result()

t()

Functions

model_certain?(literals, equations)

Whether a rule-exhausted branch's literal set may be reported as a countermodel.

new(id, formulas, params, opts \\ [])

Constructs a new root branch or an explicitly defined child branch.

Splices a synthetic {:suggested_instantiate, recipe, term} rule onto the branch's priority queue. Called by Worker when it consumes a suggestion from the :suggestions ETS table — the rule enters the ordinary popping loop and fires via the dedicated apply_rule/6 clause, which adds app(recipe, term) to the branch without spawning a child.

step(branch, params, gamma_limit, prim_limit)

Pops the next formula/rule from the queue and applies it. Returns a tuple instructing the Worker on how to proceed. History is recorded inside apply_rule/6.

wake_up(branch, cost_fn)

Wakes up a sleeping branch by reinserting its sleeping gamma rules into the queue.

Types

effect()

@type effect() ::
  :no_effects
  | {:notify_ca, MapSet.t()}
  | {:record_provenance,
     [{ShotDs.Data.Term.term_id(), ShotTx.Prover.Provenance.t()}]}

history_entry()

@type history_entry() ::
  {ShotDs.Data.Term.term_id() | nil, ShotTx.Prover.Rules.rule_t(),
   [ShotDs.Data.Term.term_id()]}

step_result()

@type step_result() ::
  {:continue,
   %ShotTx.Prover.Branch{
     defs: term(),
     equations: term(),
     frontier: term(),
     frontier_version: term(),
     ground_terms: term(),
     history: term(),
     id: term(),
     last_clash: term(),
     literals: term(),
     pending_closure: term(),
     processed_rules: term(),
     queue: term(),
     sleeping_gamma_rules: term(),
     term_ids: term(),
     type_universe: term()
   }, effect()}
  | {:split,
     my_branch :: %ShotTx.Prover.Branch{
       defs: term(),
       equations: term(),
       frontier: term(),
       frontier_version: term(),
       ground_terms: term(),
       history: term(),
       id: term(),
       last_clash: term(),
       literals: term(),
       pending_closure: term(),
       processed_rules: term(),
       queue: term(),
       sleeping_gamma_rules: term(),
       term_ids: term(),
       type_universe: term()
     },
     sibling :: %ShotTx.Prover.Branch{
       defs: term(),
       equations: term(),
       frontier: term(),
       frontier_version: term(),
       ground_terms: term(),
       history: term(),
       id: term(),
       last_clash: term(),
       literals: term(),
       pending_closure: term(),
       processed_rules: term(),
       queue: term(),
       sleeping_gamma_rules: term(),
       term_ids: term(),
       type_universe: term()
     }}
  | {:instantiate,
     branches :: [
       %ShotTx.Prover.Branch{
         defs: term(),
         equations: term(),
         frontier: term(),
         frontier_version: term(),
         ground_terms: term(),
         history: term(),
         id: term(),
         last_clash: term(),
         literals: term(),
         pending_closure: term(),
         processed_rules: term(),
         queue: term(),
         sleeping_gamma_rules: term(),
         term_ids: term(),
         type_universe: term()
       }
     ]}
  | {:idle,
     %ShotTx.Prover.Branch{
       defs: term(),
       equations: term(),
       frontier: term(),
       frontier_version: term(),
       ground_terms: term(),
       history: term(),
       id: term(),
       last_clash: term(),
       literals: term(),
       pending_closure: term(),
       processed_rules: term(),
       queue: term(),
       sleeping_gamma_rules: term(),
       term_ids: term(),
       type_universe: term()
     }}
  | {:saturated, {defs :: map(), literals :: MapSet.t()}}
  | {:exhausted,
     %ShotTx.Prover.Branch{
       defs: term(),
       equations: term(),
       frontier: term(),
       frontier_version: term(),
       ground_terms: term(),
       history: term(),
       id: term(),
       last_clash: term(),
       literals: term(),
       pending_closure: term(),
       processed_rules: term(),
       queue: term(),
       sleeping_gamma_rules: term(),
       term_ids: term(),
       type_universe: term()
     }}
  | {:closed,
     %ShotTx.Prover.Branch{
       defs: term(),
       equations: term(),
       frontier: term(),
       frontier_version: term(),
       ground_terms: term(),
       history: term(),
       id: term(),
       last_clash: term(),
       literals: term(),
       pending_closure: term(),
       processed_rules: term(),
       queue: term(),
       sleeping_gamma_rules: term(),
       term_ids: term(),
       type_universe: term()
     }}

t()

@type t() :: %ShotTx.Prover.Branch{
  defs: term(),
  equations: term(),
  frontier: term(),
  frontier_version: term(),
  ground_terms: term(),
  history: term(),
  id: term(),
  last_clash: term(),
  literals: term(),
  pending_closure: term(),
  processed_rules: term(),
  queue: term(),
  sleeping_gamma_rules: term(),
  term_ids: term(),
  type_universe: term()
}

Functions

model_certain?(literals, equations)

@spec model_certain?(MapSet.t(ShotDs.Data.Term.term_id()), %{
  required(ShotDs.Data.Term.term_id()) => MapSet.t()
}) :: boolean()

Whether a rule-exhausted branch's literal set may be reported as a countermodel.

An empty queue means no syntactic rule is left to fire. That is weaker than satisfiability: literals p s̄ and ¬(p t̄) are complementary as soon as s̄ and t̄ denote the same values, and ShotTx decides that only inside the fragment its equational machinery covers — syntactically identical terms (ground closure), unifiable terms (clash candidates handed to the CSP), and terms related by an oriented equation (demodulation). Extensional equality of two closed λ-terms is left open, so a branch holding P (λ…) and ¬(P (λ…)) for two extensionally equal but syntactically different arguments has not been shown satisfiable. Calling it a countermodel is unsound; it is merely exhausted, and step/4 reports it as :exhausted instead.

Returns true only when every same-head, opposite-polarity literal pair is separated at some argument position by two distinct rigid base-type terms — the case a free term model can satisfy by interpreting them as distinct elements. p a against ¬(p b) for distinct base constants a, b is therefore still a genuine countermodel.

new(id, formulas, params, opts \\ [])

@spec new(
  String.t(),
  [ShotDs.Data.Term.term_id()],
  ShotTx.Data.Parameters.t(),
  keyword()
) ::
  %ShotTx.Prover.Branch{
    defs: term(),
    equations: term(),
    frontier: term(),
    frontier_version: term(),
    ground_terms: term(),
    history: term(),
    id: term(),
    last_clash: term(),
    literals: term(),
    pending_closure: term(),
    processed_rules: term(),
    queue: term(),
    sleeping_gamma_rules: term(),
    term_ids: term(),
    type_universe: term()
  }

Constructs a new root branch or an explicitly defined child branch.

splice_suggested_instantiate(branch, recipe, term, source, params)

@spec splice_suggested_instantiate(
  t(),
  ShotDs.Data.Term.term_id(),
  ShotDs.Data.Term.term_id(),
  ShotDs.Data.Term.term_id() | nil,
  ShotTx.Data.Parameters.t()
) :: t()

step(branch, params, gamma_limit, prim_limit)

@spec step(
  %ShotTx.Prover.Branch{
    defs: term(),
    equations: term(),
    frontier: term(),
    frontier_version: term(),
    ground_terms: term(),
    history: term(),
    id: term(),
    last_clash: term(),
    literals: term(),
    pending_closure: term(),
    processed_rules: term(),
    queue: term(),
    sleeping_gamma_rules: term(),
    term_ids: term(),
    type_universe: term()
  },
  ShotTx.Data.Parameters.t(),
  non_neg_integer(),
  non_neg_integer()
) :: step_result()

Pops the next formula/rule from the queue and applies it. Returns a tuple instructing the Worker on how to proceed. History is recorded inside apply_rule/6.

wake_up(branch, cost_fn)

@spec wake_up(
  %ShotTx.Prover.Branch{
    defs: term(),
    equations: term(),
    frontier: term(),
    frontier_version: term(),
    ground_terms: term(),
    history: term(),
    id: term(),
    last_clash: term(),
    literals: term(),
    pending_closure: term(),
    processed_rules: term(),
    queue: term(),
    sleeping_gamma_rules: term(),
    term_ids: term(),
    type_universe: term()
  },
  (ShotTx.Prover.Rules.rule_t() -> non_neg_integer())
) :: %ShotTx.Prover.Branch{
  defs: term(),
  equations: term(),
  frontier: term(),
  frontier_version: term(),
  ground_terms: term(),
  history: term(),
  id: term(),
  last_clash: term(),
  literals: term(),
  pending_closure: term(),
  processed_rules: term(),
  queue: term(),
  sleeping_gamma_rules: term(),
  term_ids: term(),
  type_universe: term()
}

Wakes up a sleeping branch by reinserting its sleeping gamma rules into the queue.