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.