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.
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 | IRI | Subclass Of | Disjoint With | Comment |
|---|---|---|---|---|
| Predicate | https://uor.foundation/predicate/Predicate | http://www.w3.org/2002/07/owl#Thing | A total, pure, boolean-valued function on a kernel object. Evaluation terminates for all inputs and produces no side effects. | |
| TypePredicate | https://uor.foundation/predicate/TypePredicate | https://uor.foundation/predicate/Predicate | A predicate over type:TypeDefinition. Used for resolver dispatch. | |
| StatePredicate | https://uor.foundation/predicate/StatePredicate | https://uor.foundation/predicate/Predicate | A predicate over state:Context or reduction:ReductionState. Used for reduction step guards. | |
| SitePredicate | https://uor.foundation/predicate/SitePredicate | https://uor.foundation/predicate/Predicate | A predicate over partition:SiteIndex. Used for site-level selection in geodesic resolution. | |
| DispatchRule | https://uor.foundation/predicate/DispatchRule | http://www.w3.org/2002/07/owl#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 | https://uor.foundation/predicate/DispatchTable | http://www.w3.org/2002/07/owl#Thing | An ordered set of DispatchRules for a single dispatch point. Must satisfy exhaustiveness and mutual exclusion. | |
| GuardedTransition | https://uor.foundation/predicate/GuardedTransition | http://www.w3.org/2002/07/owl#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 | https://uor.foundation/predicate/MatchArm | http://www.w3.org/2002/07/owl#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 | https://uor.foundation/predicate/MatchExpression | https://uor.foundation/schema/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 | https://uor.foundation/predicate/Predicate | http://www.w3.org/2002/07/owl#Class | The OWL class of objects this predicate accepts as input. |
| dispatchPredicate | Object | true | https://uor.foundation/predicate/DispatchRule | https://uor.foundation/predicate/Predicate | The predicate that triggers this dispatch rule. |
| dispatchTarget | Object | true | https://uor.foundation/predicate/DispatchRule | http://www.w3.org/2002/07/owl#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 | https://uor.foundation/predicate/DispatchTable | https://uor.foundation/predicate/DispatchRule | The ordered set of rules in this table. |
| dispatchPriority | Datatype | true | https://uor.foundation/predicate/DispatchRule | http://www.w3.org/2001/XMLSchema#nonNegativeInteger | Non-negative integer priority. Lower priority values are evaluated first; ties within a DispatchTable are resolved by declaration order. |
| evaluatorTerm | Object | true | https://uor.foundation/predicate/Predicate | https://uor.foundation/schema/Term | The evaluator term that must reduce to a boolean-shaped datum on every input of the declared input type. |
| terminationWitness | Datatype | true | https://uor.foundation/predicate/Predicate | http://www.w3.org/2001/XMLSchema#string | An IRI or identifier of the proof:Proof / proof:ComputationCertificate attesting that the evaluator halts on all inputs. |
| guardPredicate | Object | true | https://uor.foundation/predicate/GuardedTransition | https://uor.foundation/predicate/StatePredicate | The guard predicate for this transition. |
| guardEffect | Object | true | https://uor.foundation/predicate/GuardedTransition | https://uor.foundation/effect/Effect | The effect applied when the guard is satisfied. |
| guardTarget | Object | true | https://uor.foundation/predicate/GuardedTransition | https://uor.foundation/reduction/ReductionStep | The reduction step to advance to. |
| matchArms | Object | false | https://uor.foundation/predicate/MatchExpression | https://uor.foundation/predicate/MatchArm | The ordered arms of this match expression. |
| armPredicate | Object | true | https://uor.foundation/predicate/MatchArm | https://uor.foundation/predicate/Predicate | The predicate guarding this arm. |
| armResult | Object | true | https://uor.foundation/predicate/MatchArm | https://uor.foundation/schema/Term | The result term if this arm matches. |
| boundedEvaluator | Object | false | https://uor.foundation/predicate/Predicate | https://uor.foundation/recursion/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 | https://uor.foundation/predicate/DispatchRule | http://www.w3.org/2001/XMLSchema#nonNegativeInteger | Position in the dispatch table (evaluation order). |
| isExhaustive | Datatype | true | https://uor.foundation/predicate/DispatchTable | http://www.w3.org/2001/XMLSchema#boolean | True iff the disjunction of all dispatch predicates is a tautology over the input class. |
| isMutuallyExclusive | Datatype | true | https://uor.foundation/predicate/DispatchTable | http://www.w3.org/2001/XMLSchema#boolean | True iff no two dispatch predicates can be simultaneously true for any input. |
| armIndex | Datatype | true | https://uor.foundation/predicate/MatchArm | http://www.w3.org/2001/XMLSchema#nonNegativeInteger | Position in the match expression (evaluation order). |
Named Individuals
| Name | Type | Properties | Comment |
|---|---|---|---|
| always | https://uor.foundation/predicate/Predicate |
| True on every Datum. Match-arm default catch-all. |
| never | https://uor.foundation/predicate/Predicate |
| False on every Datum. Disabled-arm marker. |
| isZero | https://uor.foundation/predicate/TypePredicate |
| True iff the Datum is the additive identity of its ring. |
| isUnit | https://uor.foundation/predicate/TypePredicate |
| True iff the Datum is the multiplicative identity. |
| isOdd | https://uor.foundation/predicate/TypePredicate |
| True iff the Datum parity bit is 1. |
| isEven | https://uor.foundation/predicate/TypePredicate |
| True iff the Datum parity bit is 0. |
| isInvolution | https://uor.foundation/predicate/TypePredicate |
| True iff op(op(x)) = x for the bound op. |
| sitePinned | https://uor.foundation/predicate/SitePredicate |
| True iff the named site coordinate is currently pinned. |
| siteFree | https://uor.foundation/predicate/SitePredicate |
| True iff the named site coordinate is currently free. |
| contradictionReached | https://uor.foundation/predicate/StatePredicate |
| True iff the resolver has entered a ContradictionBoundary. |
| budgetExhausted | https://uor.foundation/predicate/StatePredicate |
| True iff the FreeRank deficit is zero. |
| reductionConverged | https://uor.foundation/predicate/StatePredicate |
| True iff the reduction fixpoint has been reached. |
| Is2SatShape | https://uor.foundation/predicate/TypePredicate |
| True on ConstrainedType instances whose constraint nerve contains only disjunctions of width ≤ 2. |
| IsHornShape | https://uor.foundation/predicate/TypePredicate |
| True on ConstrainedType instances whose disjunctions each contain at most one positive literal. |
| IsResidualFragment | https://uor.foundation/predicate/TypePredicate |
| Default (catch-all) predicate. True on ConstrainedType instances not classified by Is2SatShape or IsHornShape. |
| InhabitanceDispatchTable | https://uor.foundation/predicate/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. |
| inhabitance_rule_2sat | https://uor.foundation/predicate/DispatchRule |
| Dispatch rule 1 of InhabitanceDispatchTable: Is2SatShape → TwoSatDecider at priority 0. |
| inhabitance_rule_horn | https://uor.foundation/predicate/DispatchRule |
| Dispatch rule 2 of InhabitanceDispatchTable: IsHornShape → HornSatDecider at priority 1. |
| inhabitance_rule_residual | https://uor.foundation/predicate/DispatchRule |
| Dispatch rule 3 (catch-all) of InhabitanceDispatchTable: IsResidualFragment → ResidualVerdictResolver at priority 2. Ensures total coverage. |