Skip to main content

try_plan_stratified_epistemic_program

Function try_plan_stratified_epistemic_program 

Source
pub fn try_plan_stratified_epistemic_program(
    program: &Program,
) -> Result<Option<EpistemicStratifiedPlan>>
Expand description

Plan a STRATIFIED epistemic execution when the program contains a modal literal over an epistemic-derived head that is itself epistemically DETERMINED.

This intercepts exactly the chained/nested-epistemic coupling that the joint single-enumeration path fails closed on (b :- know a where a :- know p, p invariant). It partitions the program’s epistemic heads into strata by modal dependency, where a head whose modal ranges over a lower DETERMINED head sits in a strictly-higher stratum. Each stratum is a self-contained sub-program compiled through the EXISTING single/joint epistemic path; at runtime the executor materializes each stratum’s GATED head into the store before the next stratum runs, so the higher stratum gates against the materialized (now-base) relation via the existing membership filter — never via resolve-into-body.

Returns:

  • Ok(Some(plan)) when the program genuinely needs (and admits) stratification: at least one modal literal ranges over an epistemically-determined derived head, and a sound stratification exists.
  • Ok(None) when no modal ranges over a determined derived head (the existing joint/split/single paths own the program — e.g. example 18’s shared base modal, where the modal target q is EDB, not a determined derived head), OR when the nested target is NOT determined (circular modality / recursion / unfounded self-support is handed back to the recursive + FAEEL/G91 guards, which keep ownership and fail closed there).