[RESEARCH][materialization] Incremental semantic-ledger → Prolog materialization, invalidation, and replay contract #388

Open
opened 2026-09-08 01:29:17 +00:00 by nsaspy · 0 comments
Owner

Related: #392 #394 #400 #402 #408 #409

Research question

Specify the generic materialization contract that turns an append-only semantic ledger into a current Prolog reasoning view while preserving exact replay, provenance, lifecycle semantics, and deterministic rebuildability.

This issue is backend-neutral. CouchDB/#408 is one candidate transport; the materialization semantics must not depend on CouchDB-specific behavior.

This is a research/design issue only. Do not implement a materializer here.

Target architecture

canonical semantic ledger
  immutable semantic objects
  assertion/support episodes
  lifecycle events
  provenance / source identity
        ↓
ordered or frontier-scoped change stream
        ↓
semantic materializer
        ↓
Prolog extensional facts + dependency metadata
        ↓
profile-specific tabled/derived views
        ↓
query / explanation / VERIFY

Canonical ledger history remains authoritative. Materialized Prolog state is rebuildable derived state.

Core questions

  1. What is the smallest backend-neutral change/event envelope required by Prolog-RLM?
  2. How are exact ledger cuts/frontiers identified and compared?
  3. What does a materialization checkpoint contain, and what must never be inferred from an opaque backend cursor alone?
  4. How should duplicate delivery be handled idempotently?
  5. How should out-of-order arrival caused by replication be represented when semantic dependencies require predecessor records?
  6. What are the required reactions to:
    • new assertion/support;
    • withdrawal/retraction;
    • supersession/correction;
    • source redaction/unavailability;
    • validity-time update;
    • schema/profile version change;
    • identity/bridge change;
    • provenance/dependence change?
  7. What data should be loaded as base/extensional facts versus left in generic semantic records interpreted by trusted predicates?
  8. When may dynamic predicates be used, and when should state instead be queried through indexed ledger adapters?
  9. How should table invalidation interact with #409's tabled/incremental profiles?
  10. How are explanations kept valid after a dependency changes?
  11. How should historical queries select an old cut without mutating the current materialization?
  12. When materialization becomes too large for one SWI process, what partitioning/projection model preserves semantics?

Required invariants

Research and formalize at least:

Rebuild equivalence

materialize_from_empty(Cut, Profile)
==
materialize_incrementally_to(Cut, Profile)

under normalized query outcomes and receipts.

Canonical-state separation

materialized fact/table/cache != canonical semantic history

Deleting a cache or restarting Prolog must never destroy knowledge.

Lifecycle correctness

withdraw(P) != assert(not(P))
supersede(P) != erase historical P
redacted payload != nonexistent historical commitment
replica copy != independent support

No execution laundering

Ledger records are data. Materialization must never consult/1, call/1, or otherwise execute arbitrary source/model-supplied Prolog.

Candidate strategies to compare

Evaluate at least:

  1. dynamic extensional predicates + tabled derived predicates;
  2. generic ground semantic-record store + interpreted reasoning predicates;
  3. generated safe profile-specific predicates after closed validation;
  4. demand-driven projection from the durable store rather than full heap materialization;
  5. hybrid hot working-set + external canonical store;
  6. XSB/SWI/Soufflé-style externalized evaluation where scale justifies it.

Compare memory use, update latency, query latency, invalidation complexity, explanation quality, historical-cut support, and failure behavior.

Incremental invalidation graph

Research an explicit dependency graph such as:

ledger record
 -> normalized extensional record
 -> proposition/assertion/context index
 -> profile rule dependency
 -> table/materialized answer
 -> explanation / query receipt

A change should invalidate only actual downstream dependents where supported.

But incremental optimization must never change semantics: if dependency tracking is uncertain, fall back to a bounded safe rebuild of the affected projection.

Checkpoint / crash semantics

Specify crash points including:

ledger commit durable, materializer not notified
change received, base fact not applied
base fact applied, derived tables not refreshed
queries running during generation switch
checkpoint written before/after projection publish
process crash during rebuild

A checkpoint must not claim a cut is materialized until the corresponding projection is atomically visible under the chosen semantics.

Define stale/lagging/rebuilding/integrity-blocked result states where current exact knowledge cannot be served.

Concurrency

Research whether the first profile should use:

  • one materializer writer + concurrent readers;
  • generation-swapped immutable projections;
  • per-theory/per-project partitions;
  • async rebuild workers using existing runtime primitives;
  • external index/materialization process.

Do not create a second scheduler in the design.

Historical / temporal reasoning

A current materialized projection must not destroy the ability to answer:

what was asserted at cut C?
what was valid at time T?
what did source S claim before correction K?
why did query Q return result R under old profile P?

Research whether historical queries are best served by temporary projections, direct ledger queries, or reusable checkpoints.

Required outputs

Produce a research record containing:

  • backend-neutral change/event contract;
  • materialization state machine;
  • cut/frontier/checkpoint semantics;
  • dependency/invalidation graph;
  • safe lowering/materialization choices;
  • crash/concurrency analysis;
  • historical-query design;
  • scale strategy comparison;
  • deterministic differential oracle;
  • benchmark/fault-injection plan;
  • proposed API surface and follow-up issue changes.

Acceptance

  • Canonical history vs materialized state is explicit.
  • Duplicate/out-of-order/retraction/supersession/profile-change cases are specified.
  • Cold rebuild vs incremental equivalence is a hard conformance oracle.
  • Materialization cannot execute arbitrary semantic/source terms.
  • Table/cache invalidation preserves explanation/provenance correctness.
  • Historical cuts remain queryable in the design.
  • Crash/checkpoint semantics cannot publish a falsely-current projection.
  • Scale discussion includes demand-driven/external-store options rather than assuming all knowledge fits in SWI heap.
  • Result composes with #409 profiles and #408 storage research without depending on either implementation.

Non-goals

  • no concrete CouchDB backend here;
  • no implementation in this issue;
  • no new canonical truth semantics beyond #394/#400;
  • no second scheduler;
  • no assumption that incremental maintenance is always preferable to rebuild.
Related: #392 #394 #400 #402 #408 #409 ## Research question Specify the **generic materialization contract** that turns an append-only semantic ledger into a current Prolog reasoning view while preserving exact replay, provenance, lifecycle semantics, and deterministic rebuildability. This issue is backend-neutral. CouchDB/#408 is one candidate transport; the materialization semantics must not depend on CouchDB-specific behavior. This is a **research/design issue only**. Do not implement a materializer here. ## Target architecture ```text canonical semantic ledger immutable semantic objects assertion/support episodes lifecycle events provenance / source identity ↓ ordered or frontier-scoped change stream ↓ semantic materializer ↓ Prolog extensional facts + dependency metadata ↓ profile-specific tabled/derived views ↓ query / explanation / VERIFY ``` Canonical ledger history remains authoritative. Materialized Prolog state is rebuildable derived state. ## Core questions 1. What is the smallest backend-neutral change/event envelope required by Prolog-RLM? 2. How are exact ledger cuts/frontiers identified and compared? 3. What does a materialization checkpoint contain, and what must never be inferred from an opaque backend cursor alone? 4. How should duplicate delivery be handled idempotently? 5. How should out-of-order arrival caused by replication be represented when semantic dependencies require predecessor records? 6. What are the required reactions to: - new assertion/support; - withdrawal/retraction; - supersession/correction; - source redaction/unavailability; - validity-time update; - schema/profile version change; - identity/bridge change; - provenance/dependence change? 7. What data should be loaded as base/extensional facts versus left in generic semantic records interpreted by trusted predicates? 8. When may dynamic predicates be used, and when should state instead be queried through indexed ledger adapters? 9. How should table invalidation interact with #409's tabled/incremental profiles? 10. How are explanations kept valid after a dependency changes? 11. How should historical queries select an old cut without mutating the current materialization? 12. When materialization becomes too large for one SWI process, what partitioning/projection model preserves semantics? ## Required invariants Research and formalize at least: ### Rebuild equivalence ```text materialize_from_empty(Cut, Profile) == materialize_incrementally_to(Cut, Profile) ``` under normalized query outcomes and receipts. ### Canonical-state separation ```text materialized fact/table/cache != canonical semantic history ``` Deleting a cache or restarting Prolog must never destroy knowledge. ### Lifecycle correctness ```text withdraw(P) != assert(not(P)) supersede(P) != erase historical P redacted payload != nonexistent historical commitment replica copy != independent support ``` ### No execution laundering Ledger records are data. Materialization must never `consult/1`, `call/1`, or otherwise execute arbitrary source/model-supplied Prolog. ## Candidate strategies to compare Evaluate at least: 1. dynamic extensional predicates + tabled derived predicates; 2. generic ground semantic-record store + interpreted reasoning predicates; 3. generated safe profile-specific predicates after closed validation; 4. demand-driven projection from the durable store rather than full heap materialization; 5. hybrid hot working-set + external canonical store; 6. XSB/SWI/Soufflé-style externalized evaluation where scale justifies it. Compare memory use, update latency, query latency, invalidation complexity, explanation quality, historical-cut support, and failure behavior. ## Incremental invalidation graph Research an explicit dependency graph such as: ```text ledger record -> normalized extensional record -> proposition/assertion/context index -> profile rule dependency -> table/materialized answer -> explanation / query receipt ``` A change should invalidate only actual downstream dependents where supported. But incremental optimization must never change semantics: if dependency tracking is uncertain, fall back to a bounded safe rebuild of the affected projection. ## Checkpoint / crash semantics Specify crash points including: ```text ledger commit durable, materializer not notified change received, base fact not applied base fact applied, derived tables not refreshed queries running during generation switch checkpoint written before/after projection publish process crash during rebuild ``` A checkpoint must not claim a cut is materialized until the corresponding projection is atomically visible under the chosen semantics. Define stale/lagging/rebuilding/integrity-blocked result states where current exact knowledge cannot be served. ## Concurrency Research whether the first profile should use: - one materializer writer + concurrent readers; - generation-swapped immutable projections; - per-theory/per-project partitions; - async rebuild workers using existing runtime primitives; - external index/materialization process. Do not create a second scheduler in the design. ## Historical / temporal reasoning A current materialized projection must not destroy the ability to answer: ```text what was asserted at cut C? what was valid at time T? what did source S claim before correction K? why did query Q return result R under old profile P? ``` Research whether historical queries are best served by temporary projections, direct ledger queries, or reusable checkpoints. ## Required outputs Produce a research record containing: - backend-neutral change/event contract; - materialization state machine; - cut/frontier/checkpoint semantics; - dependency/invalidation graph; - safe lowering/materialization choices; - crash/concurrency analysis; - historical-query design; - scale strategy comparison; - deterministic differential oracle; - benchmark/fault-injection plan; - proposed API surface and follow-up issue changes. ## Acceptance - [ ] Canonical history vs materialized state is explicit. - [ ] Duplicate/out-of-order/retraction/supersession/profile-change cases are specified. - [ ] Cold rebuild vs incremental equivalence is a hard conformance oracle. - [ ] Materialization cannot execute arbitrary semantic/source terms. - [ ] Table/cache invalidation preserves explanation/provenance correctness. - [ ] Historical cuts remain queryable in the design. - [ ] Crash/checkpoint semantics cannot publish a falsely-current projection. - [ ] Scale discussion includes demand-driven/external-store options rather than assuming all knowledge fits in SWI heap. - [ ] Result composes with #409 profiles and #408 storage research without depending on either implementation. ## Non-goals - no concrete CouchDB backend here; - no implementation in this issue; - no new canonical truth semantics beyond #394/#400; - no second scheduler; - no assumption that incremental maintenance is always preferable to rebuild.
Sign in to join this conversation.
No milestone
No project
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference
nsaspy/prolog-rlm#388
No description provided.