Enum RecursiveEpistemicClass 

pub enum RecursiveEpistemicClass {
    NonRecursive,
    CaseA,
    CaseB,
    ModalCycle,
}

Structural classification of an epistemic program with respect to ordinary (non-modal) recursion.

Recursion through positive/negated body literals normally fails closed in an epistemic program because the single-pass world-view executor cannot iterate a fixpoint. The well-defined sub-fragment “Case A” — recursion lives in the ordinary predicate while every modal atom in a recursion-participating rule is a positive know/possible over an invariant relation (an EDB or a lower non-recursive, non-epistemic stratum) — is admitted instead: the modal atom’s extension is fixed independent of the recursion, so it can be resolved to its gated relation and the reduced ordinary program iterated by the existing recursive/semi-naive engine.

Variants

NonRecursive

The program has no ordinary or modal dependency cycle; the single-pass epistemic world-view executor handles it.

CaseA

Case A: ordinary recursion with every recursion-participating modal atom over an invariant relation. Routed to the ordinary recursive engine after a Case-A reduction (see reduce_case_a_epistemic_program_to_ordinary).

CaseB

Case B: ordinary recursion where at least one POSITIVE know/possible modal ranges over a NON-invariant relation that CO-EVOLVES with the recursion (the modal target sits in the recursive SCC, or transitively depends on it). The modal truth and the ordinary derivation are a single co-evolving founded least fixpoint: resolving each positive modal to its (now recursive) ordinary atom and iterating the existing semi-naive engine computes the FAEEL founded least fixpoint directly — unfounded self-support is excluded by construction (the least model of a positive program IS its founded model), so no separate foundedness drop is needed. Routed exactly like Case A through reduce_case_a_epistemic_program_to_ordinary and the ordinary recursive engine.

ADMISSION IS POLARITY/MODE-SCOPED (proved in classify_recursive_epistemic_program): a NEGATED modal over a non-invariant target is admitted when the reduced ordinary program is stratified; a genuine negation cycle is delegated to the high-level GPU-backed WFS alternating-fixpoint executor. A possible modal over a co-evolving target is admitted under FAEEL as the founded least fixpoint. Under G91, exact head-tuple cycles are intercepted by try_prepare_g91_compatibility_reduction and evaluated by an explicit descending compatibility fixpoint.

ModalCycle

Recursion arises entirely through modal dependencies rather than an ordinary body cycle. FAEEL resolves the modal edges into an ordinary founded least fixpoint. G91 exact head-tuple possible cycles use the explicit descending compatibility plan; other admitted modal edges resolve to ordinary atoms. This class cannot use the single-pass planner, which cannot distinguish a founded predecessor chain from an unfounded tuple cycle.

Trait Implementations

impl Clone for RecursiveEpistemicClass

fn clone(&self) -> RecursiveEpistemicClass

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for RecursiveEpistemicClass

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Eq for RecursiveEpistemicClass

impl PartialEq for RecursiveEpistemicClass

fn eq(&self, other: &RecursiveEpistemicClass) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for RecursiveEpistemicClass