pulsatrix
Loading...
Searching...
No Matches
pulsatrix::datalog Namespace Reference

Classes

class  Atom
 An atom is a predicate name applied to a tuple of Terms, e.g. edge(a, b) or ancestor(X, Y) – never a nested/compound structure, since Term itself cannot nest (see datalog_term.hpp). More...
 
struct  AtomHash
 Hash functor for Atom, for use in std::unordered_map/std::unordered_set. More...
 
struct  BooleanSemiring
 A "Semiring" here is not a base class – it is a compile-time trait shape a type must satisfy to be usable as naive_evaluate_weighted<Semiring>'s template parameter: a nested Value type alias plus four static functions, zero(), one(), add(Value,Value) (⊕), mul(Value,Value) (⊗). There is no virtual interface anywhere in this file. More...
 
struct  DualNumber
 A dual number (value, grad): value is the ordinary real-valued semiring result, grad is its derivative w.r.t. whichever single base fact's weight was seeded with grad = 1 (every other base fact's weight is seeded with grad = 0, i.e. treated as a constant). More...
 
struct  DualSemiring
 The dual-number semiring: ⊕/⊗ are ordinary dual-number addition/multiplication (sum rule / product rule), zero = (0, 0), one = (1, 0) – the multiplicative identity carries no derivative of its own, matching the fact that a constant contributes nothing to any derivative. More...
 
class  FactDatabase
 A fact database: a set of ground atoms. Boolean semiring only (Mission 0's scope) – a fact is simply present or absent, with no associated weight/provenance (Mission 1's scope). More...
 
class  NeuralPredicateDatalogBridge
 Bridges one neural-predicate-weighted base fact into the real-valued weighted Datalog engine. More...
 
struct  NeuralPredicateQueryResult
 The two numbers a forward pass through the bridge produces: the derived query fact's real-valued weight, and its exact partial derivative w.r.t. the neural predicate's (sigmoid-squashed) output – both computed in the same DualSemiring<double> evaluation pass (see datalog_dual_semiring.hpp). More...
 
struct  NeuralPredicateRelevanceResult
 The result of one NeuralPredicateDatalogBridge::propagate_relevance() call – Phase 3 Mission 3's own deliverable (LRP for the Datalog/provenance-semiring circuit), extended end-to-end through the neural predicate's own Module chain. More...
 
struct  RealSemiring
 The real-valued (+, x) semiring: ⊕ = floating-point addition, ⊗ = floating-point multiplication, zero = 0.0, one = 1.0 – the differentiable-provenance case. More...
 
struct  RelevanceResult
 The result of one propagate_relevance_weighted call: relevance recorded at every atom the recursion visited (all_atoms, useful for inspection/debugging), and relevance recorded only at atoms with zero matching derivations in fixpoint – the extensional/base facts (base_facts) – which is what an end-to-end conservation check must sum against the seeded relevance, per ordinary LRP convention (intermediate/derived atoms are redistribution waypoints, not part of the conserved total, exactly as an ordinary Module chain's intermediate activations are not summed alongside its raw inputs). More...
 
class  Rule
 A rule: a head atom entailed whenever every body atom is simultaneously satisfiable under one consistent variable substitution. More...
 
class  Term
 A Datalog term: either a constant (e.g. a) or a variable (e.g. X) – never a compound/function-symbol term. More...
 
struct  TermHash
 Hash functor for Term, for use in std::unordered_map/std::unordered_set. More...
 
class  WeightedFactDatabase
 A weighted fact database: a map from ground atom to a semiring value type T (bool for the trivial/boolean instantiation, double/float for the real-valued (+, x) instantiation). More...
 

Typedefs

using FactSet = std::unordered_set< Atom, AtomHash >
 The concrete set type a FactDatabase stores facts in and the engine derives into.
 
using RelevanceMap = std::unordered_map< Atom, double, AtomHash >
 A map from ground atom to its accumulated relevance (real-valued, per the RealSemiring<double> circuit this rule operates over).
 
template<typename T >
using WeightedFactSet = std::unordered_map< Atom, T, AtomHash >
 The concrete map type a WeightedFactDatabase<T> stores facts in.
 

Enumerations

enum class  TermKind { Constant , Variable }
 Which of the two (and only two) term alternatives this Term is. More...
 

Functions

FactDatabase naive_evaluate (const std::vector< Rule > &rules, const FactDatabase &initial_facts)
 Naive bottom-up fixpoint evaluation: repeatedly re-evaluates every rule against the entire accumulated fact set until a round derives no new facts.
 
FactDatabase semi_naive_evaluate (const std::vector< Rule > &rules, const FactDatabase &initial_facts)
 Semi-naive bottom-up fixpoint evaluation: each round only considers rule applications where at least one body atom is matched against facts newly derived in the previous round (the "delta"), rather than re-scanning the full accumulated fact set for every body-atom position every round.
 
RelevanceResult propagate_relevance_weighted (const std::vector< Rule > &rules, const WeightedFactDatabase< double > &fixpoint, const Atom &query, double relevance_seed, double epsilon=1e-6)
 Propagates relevance from query's derived weight back through every derivation path in fixpoint (a stable, already-evaluated naive_evaluate_weighted< RealSemiring<double>> result), down to every extensional/base fact that contributed to it – see this file's header doc comment for the full hand-derived rule and worked numeric example.
 
template<typename Semiring >
WeightedFactDatabase< typename Semiring::Value > naive_evaluate_weighted (const std::vector< Rule > &rules, const WeightedFactDatabase< typename Semiring::Value > &initial_facts)
 Naive bottom-up fixpoint evaluation, generalized over any Semiring-shaped Semiring (see datalog_semiring.hpp): each round, every rule/substitution combination is matched against the entire current weighted fact set, and every derivation's weight (the ⊗-product of the weights of the facts it matched) is combined via ⊕ with every other derivation of the same head atom found in that same round. The atom's stored weight is then replaced with that round's freshly recomputed total (never added to the previous round's total) – see Stage 3 design decision 2 below for why replace-with-a-fresh-full-recompute, not incremental accumulate-across-rounds, is the correct generalization.
 
template<typename Semiring >
WeightedFactDatabase< typename Semiring::Value > semi_naive_evaluate_weighted (const std::vector< Rule > &rules, const WeightedFactDatabase< typename Semiring::Value > &initial_facts)
 The semi-naive-named weighted counterpart of naive_evaluate_weighted.
 
template WeightedFactDatabase< bool > naive_evaluate_weighted< BooleanSemiring > (const std::vector< Rule > &, const WeightedFactDatabase< bool > &)
 
template WeightedFactDatabase< double > naive_evaluate_weighted< RealSemiring< double > > (const std::vector< Rule > &, const WeightedFactDatabase< double > &)
 
template WeightedFactDatabase< bool > semi_naive_evaluate_weighted< BooleanSemiring > (const std::vector< Rule > &, const WeightedFactDatabase< bool > &)
 
template WeightedFactDatabase< double > semi_naive_evaluate_weighted< RealSemiring< double > > (const std::vector< Rule > &, const WeightedFactDatabase< double > &)
 
template WeightedFactDatabase< DualNumber< double > > naive_evaluate_weighted< DualSemiring< double > > (const std::vector< Rule > &, const WeightedFactDatabase< DualNumber< double > > &)
 
template WeightedFactDatabase< DualNumber< double > > semi_naive_evaluate_weighted< DualSemiring< double > > (const std::vector< Rule > &, const WeightedFactDatabase< DualNumber< double > > &)
 

Typedef Documentation

◆ FactSet

using pulsatrix::datalog::FactSet = typedef std::unordered_set<Atom, AtomHash>

The concrete set type a FactDatabase stores facts in and the engine derives into.

◆ RelevanceMap

using pulsatrix::datalog::RelevanceMap = typedef std::unordered_map<Atom, double, AtomHash>

A map from ground atom to its accumulated relevance (real-valued, per the RealSemiring<double> circuit this rule operates over).

◆ WeightedFactSet

template<typename T >
using pulsatrix::datalog::WeightedFactSet = typedef std::unordered_map<Atom, T, AtomHash>

The concrete map type a WeightedFactDatabase<T> stores facts in.

Enumeration Type Documentation

◆ TermKind

enum class pulsatrix::datalog::TermKind
strong

Which of the two (and only two) term alternatives this Term is.

Enumerator
Constant 
Variable 

Function Documentation

◆ naive_evaluate()

FactDatabase pulsatrix::datalog::naive_evaluate ( const std::vector< Rule > &  rules,
const FactDatabase &  initial_facts 
)

Naive bottom-up fixpoint evaluation: repeatedly re-evaluates every rule against the entire accumulated fact set until a round derives no new facts.

Parameters
rulesThe Datalog program (each rule already validated safe by its own constructor).
initial_factsThe starting fact database (extensional database, e.g. edge facts).
Returns
The fixpoint: initial_facts plus every fact derivable by any finite number of rule applications (the intensional database), boolean semiring (a fact is either present or absent – no weight/provenance).
Note
Always terminates on a function-symbol-free, range-restricted program over a finite initial fact set: every derived atom's constants come from the finite set of constants already present in rules/initial_facts (no function symbols to manufacture new ones), so the space of possible ground atoms is finite and facts only ever accumulate (monotone) – the fixpoint is reached in a bounded number of rounds. This is Decision Point 1's whole rationale for choosing Datalog over Prolog.

◆ naive_evaluate_weighted()

template<typename Semiring >
WeightedFactDatabase< typename Semiring::Value > pulsatrix::datalog::naive_evaluate_weighted ( const std::vector< Rule > &  rules,
const WeightedFactDatabase< typename Semiring::Value > &  initial_facts 
)

Naive bottom-up fixpoint evaluation, generalized over any Semiring-shaped Semiring (see datalog_semiring.hpp): each round, every rule/substitution combination is matched against the entire current weighted fact set, and every derivation's weight (the ⊗-product of the weights of the facts it matched) is combined via ⊕ with every other derivation of the same head atom found in that same round. The atom's stored weight is then replaced with that round's freshly recomputed total (never added to the previous round's total) – see Stage 3 design decision 2 below for why replace-with-a-fresh-full-recompute, not incremental accumulate-across-rounds, is the correct generalization.

Note
Stage 3 design decision 2 (multi-path weight accumulation): the correctness pitfall the mission flags – "first write wins" vs. "accumulate" being indistinguishable under boolean ⊕ = OR but not under real-valued ⊕ = + – is resolved as follows:
  • Within one round, every rule/substitution pair that derives the same head atom has its weight ⊕-summed into that atom's round_totals entry before anything is written back to the fact database. This is what makes a genuine multi-path fact (e.g. ancestor(a,d) derivable via two different intermediate nodes in a diamond graph) correctly get the sum of both paths' products, not just one of them (verified by WeightedDatalogEngineTest.MultiplePathsAccumulateViaSemiringAdd).
  • Across rounds, the atom's weight is replaced by each round's freshly recomputed total, not added to the prior round's stored value. This is the subtle part: naive evaluation re-scans the entire fact set every round, so the same derivation combination is rediscovered every round for as long as its inputs remain unchanged – if the round total were ⊕-accumulated onto the existing stored weight every round (the naive-looking-but-wrong translation of "accumulate, don't overwrite"), the same path's contribution would be re-added every single round forever, diverging rather than reaching a fixpoint. Replacing with a freshly recomputed total instead means: the total is always "the full `⊕`-sum over every derivation visible in *this* round's snapshot of the database," which is monotone non-decreasing round-over-round (later rounds only ever have equal-or-larger dependency weights to draw on, for a nonnegative semiring) and stabilizes at exactly the sum-of-products-over-all-derivation-paths value once every dependency has itself stabilized – proven against the hand-derived expected weights below, not merely asserted.
  • A fact derivable via zero paths never appears in round_totals at all and is therefore never written into the result database – weight_of() reports the caller-supplied default (conventionally Semiring::zero()) for it, per WeightedFactDatabase::weight_of's own contract.
  • A fact derivable via exactly one path gets round_totals[head] = Semiring::add( Semiring::zero(), that_one_path's_product), which for every semiring here satisfies add(zero(), x) == x (the semiring identity law) – so a single-path fact's stored weight is exactly that path's product, with no spurious contribution from anywhere else (verified by WeightedDatalogEngineTest.SinglePathWeightEqualsThatPathsProductExactly).
Parameters
rulesThe Datalog program (each rule already validated safe by its own constructor).
initial_factsThe starting weighted fact database (extensional database).
Returns
The fixpoint: every atom reachable from initial_facts by any finite number of rule applications, each carrying the ⊕-sum-of-⊗-products weight standard weighted-Datalog/provenance-semiring semantics assigns it.

◆ naive_evaluate_weighted< BooleanSemiring >()

template WeightedFactDatabase< bool > pulsatrix::datalog::naive_evaluate_weighted< BooleanSemiring > ( const std::vector< Rule > &  ,
const WeightedFactDatabase< bool > &   
)
extern

◆ naive_evaluate_weighted< DualSemiring< double > >()

template WeightedFactDatabase< DualNumber< double > > pulsatrix::datalog::naive_evaluate_weighted< DualSemiring< double > > ( const std::vector< Rule > &  ,
const WeightedFactDatabase< DualNumber< double > > &   
)
extern

◆ naive_evaluate_weighted< RealSemiring< double > >()

template WeightedFactDatabase< double > pulsatrix::datalog::naive_evaluate_weighted< RealSemiring< double > > ( const std::vector< Rule > &  ,
const WeightedFactDatabase< double > &   
)
extern

◆ propagate_relevance_weighted()

RelevanceResult pulsatrix::datalog::propagate_relevance_weighted ( const std::vector< Rule > &  rules,
const WeightedFactDatabase< double > &  fixpoint,
const Atom &  query,
double  relevance_seed,
double  epsilon = 1e-6 
)

Propagates relevance from query's derived weight back through every derivation path in fixpoint (a stable, already-evaluated naive_evaluate_weighted< RealSemiring<double>> result), down to every extensional/base fact that contributed to it – see this file's header doc comment for the full hand-derived rule and worked numeric example.

Parameters
rulesThe Datalog program (used to re-derive, from the stable fixpoint, exactly which (rule, substitution) matches produced query's weight and every intermediate derived atom's weight along the way).
fixpointA stable (already-converged) weighted fact database – the output of naive_evaluate_weighted<RealSemiring<double>> (or equivalent), not an intermediate round's snapshot. Re-matching rule bodies against a non-fixpoint database would not reproduce the derivation structure that actually produced the atom's stored weight.
queryThe atom whose weight's relevance is being explained (typically the query fact a caller cares about, e.g. ancestor(a,d)).
relevance_seedThe relevance value seeded at query (mirrors every other conservation test in this codebase's own convention of seeding an arbitrary value at a chain's output and checking it is conserved at the input).
epsilonStabilizer for both the ⊕-level weighted-sum split and the ⊗-level bilinear split, matching LRPRuleConfig::epsilon's own role and default (1e-6f, widened to double here since this circuit's own weights are double).
Exceptions
std::logic_errorif any rule body actually matched during propagation has arity greater than 2 – see this file's own "Scope restriction" note; no toy program in this campaign needs a wider rule body, so this is an honest, logged boundary rather than a silently-approximated n-ary split.

◆ semi_naive_evaluate()

FactDatabase pulsatrix::datalog::semi_naive_evaluate ( const std::vector< Rule > &  rules,
const FactDatabase &  initial_facts 
)

Semi-naive bottom-up fixpoint evaluation: each round only considers rule applications where at least one body atom is matched against facts newly derived in the previous round (the "delta"), rather than re-scanning the full accumulated fact set for every body-atom position every round.

Parameters
rulesThe Datalog program.
initial_factsThe starting fact database.
Returns
The identical fixpoint naive_evaluate would produce on the same program and initial facts (proven by a direct equivalence test, not merely "also seems to work" – see datalog_engine_test.cpp's SemiNaiveEvaluationProducesIdenticalFixpointToNaiveEvaluation).

◆ semi_naive_evaluate_weighted()

template<typename Semiring >
WeightedFactDatabase< typename Semiring::Value > pulsatrix::datalog::semi_naive_evaluate_weighted ( const std::vector< Rule > &  rules,
const WeightedFactDatabase< typename Semiring::Value > &  initial_facts 
)

The semi-naive-named weighted counterpart of naive_evaluate_weighted.

Note
Deliberately scoped, logged limitation (not silently dropped): a genuinely incremental semi-naive optimization for weighted/provenance-semiring accumulation is materially harder than the boolean case's delta-restriction trick, because a derived atom's weight is not monotone-and-idempotent the way boolean presence is – a later round can still add a new, previously-undiscovered derivation path's contribution to an atom whose weight had already stopped changing for several rounds (e.g. a longer path stabilizing later than a shorter one to the same destination), which breaks the boolean semi-naive algorithm's core assumption that "once an atom is in the delta set, and then leaves it, it never needs revisiting." Correctly generalizing semi-naive's delta-restriction to semirings (tracking which dependency weight changes require which downstream atoms to be recomputed) is real, uncommitted future work – this mission's own scoping note explicitly warns against silently absorbing extra scope (that note names Mission 2's gradient work; the same discipline applies here to a correctness-vs-effort tradeoff this mission's own exit condition does not require). This function therefore delegates to the already-proven-correct naive_evaluate_weighted<Semiring> algorithm, preserving the requested API surface (parity with Mission 0's naive/semi-naive pairing) without claiming a performance optimization this mission did not actually implement. WeightedDatalogEngineTest's equivalence test therefore checks this function returns identically what naive_evaluate_weighted returns, by construction, not as an emergent property.
Parameters
rulesThe Datalog program.
initial_factsThe starting weighted fact database.
Returns
Exactly what naive_evaluate_weighted<Semiring>(rules, initial_facts) returns.

◆ semi_naive_evaluate_weighted< BooleanSemiring >()

template WeightedFactDatabase< bool > pulsatrix::datalog::semi_naive_evaluate_weighted< BooleanSemiring > ( const std::vector< Rule > &  ,
const WeightedFactDatabase< bool > &   
)
extern

◆ semi_naive_evaluate_weighted< DualSemiring< double > >()

template WeightedFactDatabase< DualNumber< double > > pulsatrix::datalog::semi_naive_evaluate_weighted< DualSemiring< double > > ( const std::vector< Rule > &  ,
const WeightedFactDatabase< DualNumber< double > > &   
)
extern

◆ semi_naive_evaluate_weighted< RealSemiring< double > >()

template WeightedFactDatabase< double > pulsatrix::datalog::semi_naive_evaluate_weighted< RealSemiring< double > > ( const std::vector< Rule > &  ,
const WeightedFactDatabase< double > &   
)
extern