UOR Derivations
This is a bridge-space namespace in the Resolve stage of the PRISM pipeline. It provides the resolution infrastructure — queries, partitions, observables, proofs, derivations, and traces that transform inputs into certified results.
Learn more: Pipeline Overview · Proofs, Derivations & Traces
Imports
https://uor.foundation/observable/https://uor.foundation/op/https://uor.foundation/resolver/https://uor.foundation/schema/https://uor.foundation/type/
Classes
| Name | Subclass Of | Disjoint With | Comment |
|---|---|---|---|
Derivation | Thing | A complete term rewriting witness: the full sequence of rewrite steps transforming an original term into its canonical form. | |
DerivationStep | Thing | An abstract step in a derivation. Concrete subclasses are RewriteStep (term-level rewriting) and RefinementStep (type-level refinement). | |
RewriteStep | DerivationStep | A single rewrite step in a derivation: the application of one rewrite rule to transform a term. | |
RefinementStep | DerivationStep | A type-level refinement step: the application of a constraint to narrow a type, pinning additional site coordinates. Complements RewriteStep (term-level) in the derivation hierarchy. | |
RewriteRule | Thing | A named rewrite rule that can be applied in a derivation step. Each RewriteRule individual represents a specific algebraic law or normalization strategy used during term rewriting. | |
TermMetrics | Thing | Metrics describing the size and complexity of a term. | |
SynthesisStep | Thing | A single step in the construction of a SynthesizedType: one constraint added to the synthesis candidate and the resulting change in the constraint nerve's topological signature. Ordered by derivation:stepIndex. Analogous to derivation:RewriteStep in the forward pipeline. | |
SynthesisCheckpoint | Thing | A persistent snapshot of a ConstraintSearchState at a specific SynthesisStep, allowing a TypeSynthesisResolver to resume exploration after interruption. Essential at Q1+ scale where exhaustive synthesis is computationally significant. | |
InhabitanceStep | SynthesisStep | A peer of derivation:SynthesisStep specialised to inhabitance search. Each step represents one navigation in the constraint nerve, either pinning a site to a value or confirming that a predicate evaluates true on the current partial assignment. | |
InhabitanceCheckpoint | SynthesisCheckpoint | A peer of derivation:SynthesisCheckpoint specialised to inhabitance search. Marks an audit point where the resolver state can be restored if the search backtracks. | |
DerivationDepthObservable | Observable | Observes the derivation depth of a Datum, computed as the maximum nesting level of derivation:RewriteStep applications producing it. Used as the bound observable for the depthConstraintKind BoundConstraint. | |
DerivationTrace | Thing | An ordered sequence of derivation:RewriteStep events produced by replaying a Derivation. Used by uor-foundation-verify to re-derive a certificate from a content-addressed trace without running the deciders. The traceEventCount property records the trace length. |
Properties
| Name | Kind | Functional | Domain | Range | Comment |
|---|---|---|---|---|---|
originalTerm | Object | true | Derivation | Term | The term at the start of the derivation, before any rewriting. |
canonicalTerm | Object | true | Derivation | Term | The canonical form produced at the end of the derivation. |
result | Object | true | Derivation | Datum | The datum value obtained by evaluating the canonical term. |
step | Object | false | Derivation | RewriteStep | A rewrite step in this derivation. |
termMetrics | Object | true | Derivation | TermMetrics | Metrics for the canonical term produced by this derivation. |
from | Object | true | RewriteStep | Term | The term before this rewrite step. |
to | Object | true | RewriteStep | Term | The term after this rewrite step. |
hasRewriteRule | Object | true | RewriteStep | RewriteRule | The typed rewrite rule applied in this step. Provides a structured reference to a named RewriteRule individual, complementing the string-valued derivation:rule property. |
groundedIn | Object | true | RewriteRule | Identity | The algebraic identity that grounds this rewrite rule. Links a RewriteRule to the op:Identity individual that justifies its application. |
stepCount | Datatype | true | TermMetrics | nonNegativeInteger | The total number of rewrite steps in this derivation. |
termSize | Datatype | true | TermMetrics | nonNegativeInteger | The number of nodes in the canonical term's syntax tree. |
previousType | Object | true | RefinementStep | TypeDefinition | The type before this refinement step was applied. |
appliedConstraint | Object | true | RefinementStep | Constraint | The constraint that was applied in this refinement step. |
refinedType | Object | true | RefinementStep | TypeDefinition | The type after this refinement step was applied. |
sitesClosed | Datatype | true | RefinementStep | nonNegativeInteger | The number of site coordinates pinned by this refinement step. |
stepIndex | Datatype | true | SynthesisStep | nonNegativeInteger | Zero-based sequential index of this step within the synthesis derivation. |
addedConstraint | Object | true | SynthesisStep | Constraint | The constraint added in this synthesis step. |
signatureBefore | Object | true | SynthesisStep | SynthesisSignature | The constraint nerve signature before this synthesis step. |
signatureAfter | Object | true | SynthesisStep | SynthesisSignature | The constraint nerve signature after this synthesis step. |
checkpointStep | Object | true | SynthesisCheckpoint | SynthesisStep | The SynthesisStep at which this checkpoint was taken. |
checkpointState | Object | true | SynthesisCheckpoint | ConstraintSearchState | The ConstraintSearchState snapshot captured by this checkpoint. |
towerCheckpoint | Object | false | TowerCompletenessResolver | SynthesisCheckpoint | Links a TowerCompletenessResolver to a SynthesisCheckpoint issued at each completed step. Cross-namespace bridge property: domain is resolver:TowerCompletenessResolver. |
priorState | Object | true | InhabitanceStep | ConstraintSearchState | The ConstraintSearchState before this InhabitanceStep was taken. |
successorState | Object | true | InhabitanceStep | ConstraintSearchState | The ConstraintSearchState after this InhabitanceStep was taken. |
rule | Object | true | InhabitanceStep | DispatchRule | The predicate:DispatchRule whose evaluation drove this InhabitanceStep. |
checkpointIndex | Datatype | true | InhabitanceCheckpoint | integer | Ordinal index of this checkpoint within the InhabitanceSearchTrace's checkpoint sequence. |
traceEventCount | Datatype | true | DerivationTrace | nonNegativeInteger | Number of RewriteStep events recorded in this DerivationTrace. Used by Derivation::replay() to size the fixed-capacity event arena without allocation. |
Named Individuals
| Name | Type | Comment |
|---|---|---|
CriticalIdentityRule | RewriteRule | The rewrite rule applying the critical identity: neg(bnot(x)) → succ(x). Grounded in op:criticalIdentity. |
| ||
InvolutionRule | RewriteRule | The rewrite rule applying involution cancellation: f(f(x)) → x for any involution f. |
AssociativityRule | RewriteRule | The rewrite rule applying associativity to re-bracket nested binary operations. |
CommutativityRule | RewriteRule | The rewrite rule applying commutativity to reorder operands of commutative operations. |
IdentityElementRule | RewriteRule | The rewrite rule eliminating identity elements: add(x, 0) → x, mul(x, 1) → x, xor(x, 0) → x. |
NormalizationRule | RewriteRule | The rewrite rule normalizing compound expressions to canonical ordering (e.g., sorting operands by address). |