This is a kernel-space namespace in the Define stage of the PRISM pipeline. It provides the immutable algebraic substrate — ring structure, schema vocabulary, and operation algebra.
A total, pure, boolean-valued function on a kernel object. Evaluation terminates for all inputs and produces no side effects.
TypePredicate
Predicate
A predicate over type:TypeDefinition. Used for resolver dispatch.
StatePredicate
Predicate
A predicate over state:Context or reduction:ReductionState. Used for reduction step guards.
SitePredicate
Predicate
A predicate over partition:SiteIndex. Used for site-level selection in geodesic resolution.
DispatchRule
Thing
A pair (Predicate, Target) where Target is a resolver:Resolver class. The kernel evaluates the predicate; if true, the target resolver is selected.
DispatchTable
Thing
An ordered set of DispatchRules for a single dispatch point. Must satisfy exhaustiveness and mutual exclusion.
GuardedTransition
Thing
A triple (StatePredicate, effect:Effect, reduction:ReductionStep). The guard is a StatePredicate; if true, the effect is applied and the reduction advances to the target step.
MatchArm
Thing
A single case in a pattern match: a Predicate and a result Term. The match evaluates predicates in order and returns the result of the first matching arm.
MatchExpression
Term
A term formed by evaluating a sequence of MatchArms. Extends the term language with deterministic conditional evaluation.
Properties
Name
Kind
Functional
Domain
Range
Comment
evaluatesOver
Object
true
Predicate
Class
The OWL class of objects this predicate accepts as input.
dispatchPredicate
Object
true
DispatchRule
Predicate
The predicate that triggers this dispatch rule.
dispatchTarget
Object
true
DispatchRule
Resolver
The resolver selected when the predicate is satisfied.
dispatchRules
Object
false
DispatchTable
DispatchRule
The ordered set of rules in this table.
guardPredicate
Object
true
GuardedTransition
StatePredicate
The guard predicate for this transition.
guardEffect
Object
true
GuardedTransition
Effect
The effect applied when the guard is satisfied.
guardTarget
Object
true
GuardedTransition
ReductionStep
The reduction step to advance to.
matchArms
Object
false
MatchExpression
MatchArm
The ordered arms of this match expression.
armPredicate
Object
true
MatchArm
Predicate
The predicate guarding this arm.
armResult
Object
true
MatchArm
Term
The result term if this arm matches.
boundedEvaluator
Object
false
Predicate
DescentMeasure
A termination witness for user-declared predicates. Kernel predicates are total by construction; user-declared predicates must carry a descent measure certifying termination.
dispatchIndex
Datatype
true
DispatchRule
nonNegativeInteger
Position in the dispatch table (evaluation order).
isExhaustive
Datatype
true
DispatchTable
boolean
True iff the disjunction of all dispatch predicates is a tautology over the input class.
isMutuallyExclusive
Datatype
true
DispatchTable
boolean
True iff no two dispatch predicates can be simultaneously true for any input.
armIndex
Datatype
true
MatchArm
nonNegativeInteger
Position in the match expression (evaluation order).
Named Individuals
Name
Type
Comment
always
Predicate
True on every Datum. Match-arm default catch-all.
evaluatesOver: Datum
never
Predicate
False on every Datum. Disabled-arm marker.
evaluatesOver: Datum
isZero
TypePredicate
True iff the Datum is the additive identity of its ring.
evaluatesOver: Datum
isUnit
TypePredicate
True iff the Datum is the multiplicative identity.
evaluatesOver: Datum
isOdd
TypePredicate
True iff the Datum parity bit is 1.
evaluatesOver: Datum
isEven
TypePredicate
True iff the Datum parity bit is 0.
evaluatesOver: Datum
isInvolution
TypePredicate
True iff op(op(x)) = x for the bound op.
evaluatesOver: Datum
sitePinned
SitePredicate
True iff the named site coordinate is currently pinned.
evaluatesOver: SiteIndex
siteFree
SitePredicate
True iff the named site coordinate is currently free.
evaluatesOver: SiteIndex
contradictionReached
StatePredicate
True iff the resolver has entered a ContradictionBoundary.