UOR Predicates and Dispatch

IRI: https://uor.foundation/predicate/
Prefix: predicate:
Space: kernel
Comment: Boolean-valued functions on kernel objects. Formalizes resolver dispatch, reduction guard evaluation, and conditional resolution paths.

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.

Learn more: Pipeline Overview

Class hierarchy

Imports

https://uor.foundation/op/
https://uor.foundation/schema/
https://uor.foundation/type/
https://uor.foundation/state/
https://uor.foundation/effect/
https://uor.foundation/partition/

Classes

Name	Subclass Of	Comment
`Predicate`	`Thing`	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`	`Class`	The resolver class selected when the predicate is satisfied. Range is the OWL class IRI of a resolver:Resolver subclass; v0.2.1 uses class IRIs so the codegen can construct façade structs.
`dispatchRules`	Object	false	`DispatchTable`	`DispatchRule`	The ordered set of rules in this table.
`dispatchPriority`	Datatype	true	`DispatchRule`	`nonNegativeInteger`	Non-negative integer priority. Lower priority values are evaluated first; ties within a DispatchTable are resolved by declaration order.
`evaluatorTerm`	Object	true	`Predicate`	`Term`	The evaluator term that must reduce to a boolean-shaped datum on every input of the declared input type.
`terminationWitness`	Datatype	true	`Predicate`	`string`	An IRI or identifier of the proof:Proof / proof:ComputationCertificate attesting that the evaluator halts on all inputs.
`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.
`evaluatesOver`: `ContradictionBoundary`
`budgetExhausted`	`StatePredicate`	True iff the FreeRank deficit is zero.
`evaluatesOver`: `FreeRank`
`reductionConverged`	`StatePredicate`	True iff the reduction fixpoint has been reached.
`evaluatesOver`: `ReductionState`
`Is2SatShape`	`TypePredicate`	True on ConstrainedType instances whose constraint nerve contains only disjunctions of width ≤ 2.
`evaluatesOver`: `ConstrainedType`
`IsHornShape`	`TypePredicate`	True on ConstrainedType instances whose disjunctions each contain at most one positive literal.
`evaluatesOver`: `ConstrainedType`
`IsResidualFragment`	`TypePredicate`	Default (catch-all) predicate. True on ConstrainedType instances not classified by Is2SatShape or IsHornShape.
`evaluatesOver`: `ConstrainedType`
`InhabitanceDispatchTable`	`DispatchTable`	The predicate:DispatchTable governing resolver:InhabitanceResolver. Three rules form a partition of type:ConstrainedType: Is2SatShape → TwoSatDecider (priority 0), IsHornShape → HornSatDecider (priority 1), IsResidualFragment → ResidualVerdictResolver (priority 2, catch-all). Total coverage is enforced by reduction:DispatchCoverageCheck; DispatchMiss is unreachable for this table.
`isExhaustive`: true `isMutuallyExclusive`: true
`inhabitance_rule_2sat`	`DispatchRule`	Dispatch rule 1 of InhabitanceDispatchTable: Is2SatShape → TwoSatDecider at priority 0.
`dispatchPredicate`: `Is2SatShape` `dispatchTarget`: `TwoSatDecider` `dispatchPriority`: 0
`inhabitance_rule_horn`	`DispatchRule`	Dispatch rule 2 of InhabitanceDispatchTable: IsHornShape → HornSatDecider at priority 1.
`dispatchPredicate`: `IsHornShape` `dispatchTarget`: `HornSatDecider` `dispatchPriority`: 1
`inhabitance_rule_residual`	`DispatchRule`	Dispatch rule 3 (catch-all) of InhabitanceDispatchTable: IsResidualFragment → ResidualVerdictResolver at priority 2. Ensures total coverage.
`dispatchPredicate`: `IsResidualFragment` `dispatchTarget`: `ResidualVerdictResolver` `dispatchPriority`: 2