Skip to main content

try_reduce_case_a_recursive_epistemic_program

Function try_reduce_case_a_recursive_epistemic_program 

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

Validate a Case-A recursive epistemic program and return its ordinary reduction.

This is the Case-A counterpart to compile_epistemic_gpu_execution: instead of building a single-pass GPU world-view plan, it proves the program is admissible Case A and resolves it to an ordinary recursive program for the existing fixpoint engine. Validation still flows through the EIR boundary (build_eir) via classify_recursive_epistemic_program, which already requires EVERY modal literal to range over an INVARIANT relation. A direct modal self-support over the recursive head (possible p with p the recursive/derived head) ranges over a NON-invariant relation and is therefore rejected as non-Case-A upstream — so unfounded modal self-support never reaches this reduction. Only EXECUTION routes through the ordinary engine.

Returns Ok(Some(reduced)) when the program is admissible Case A, Ok(None) when the program has no ordinary recursion (the caller should use the single-pass epistemic path), and a typed error for any non-Case-A recursive shape.