Enum RecursiveEpistemicClass 

pub enum RecursiveEpistemicClass {
    NonRecursive,
    CaseA,
    CaseB,
}

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 recursion among epistemic rules; the existing 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 and under G91 as the compatibility self-support assumption.

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 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 Eq for RecursiveEpistemicClass

impl StructuralPartialEq for RecursiveEpistemicClass