|
| 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...
|
| |
|
| 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 > > &) |
| |
template<typename Semiring >
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
-
| rules | The Datalog program (each rule already validated safe by its own constructor). |
| initial_facts | The 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.