UOR Derivations
- IRI
https://uor.foundation/derivation/- Prefix
derivation:- Space
- bridge
- Comment
- Computation witnesses recording term rewriting sequences from original terms to their canonical forms.
Imports
https://uor.foundation/observable/https://uor.foundation/op/https://uor.foundation/resolver/https://uor.foundation/schema/https://uor.foundation/type/
Classes
| Name | IRI | Subclass Of | Disjoint With | Comment |
|---|---|---|---|---|
| Derivation | https://uor.foundation/derivation/Derivation | http://www.w3.org/2002/07/owl#Thing | A complete term rewriting witness: the full sequence of rewrite steps transforming an original term into its canonical form. | |
| DerivationStep | https://uor.foundation/derivation/DerivationStep | http://www.w3.org/2002/07/owl#Thing | An abstract step in a derivation. Concrete subclasses are RewriteStep (term-level rewriting) and RefinementStep (type-level refinement). | |
| RewriteStep | https://uor.foundation/derivation/RewriteStep | https://uor.foundation/derivation/DerivationStep | A single rewrite step in a derivation: the application of one rewrite rule to transform a term. | |
| RefinementStep | https://uor.foundation/derivation/RefinementStep | https://uor.foundation/derivation/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 | https://uor.foundation/derivation/RewriteRule | http://www.w3.org/2002/07/owl#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 | https://uor.foundation/derivation/TermMetrics | http://www.w3.org/2002/07/owl#Thing | Metrics describing the size and complexity of a term. | |
| SynthesisStep | https://uor.foundation/derivation/SynthesisStep | http://www.w3.org/2002/07/owl#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 | https://uor.foundation/derivation/SynthesisCheckpoint | http://www.w3.org/2002/07/owl#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 | https://uor.foundation/derivation/InhabitanceStep | https://uor.foundation/derivation/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 | https://uor.foundation/derivation/InhabitanceCheckpoint | https://uor.foundation/derivation/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 | https://uor.foundation/derivation/DerivationDepthObservable | https://uor.foundation/observable/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 | https://uor.foundation/derivation/DerivationTrace | http://www.w3.org/2002/07/owl#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 | https://uor.foundation/derivation/Derivation | https://uor.foundation/schema/Term | The term at the start of the derivation, before any rewriting. |
| canonicalTerm | Object | true | https://uor.foundation/derivation/Derivation | https://uor.foundation/schema/Term | The canonical form produced at the end of the derivation. |
| result | Object | true | https://uor.foundation/derivation/Derivation | https://uor.foundation/schema/Datum | The datum value obtained by evaluating the canonical term. |
| step | Object | false | https://uor.foundation/derivation/Derivation | https://uor.foundation/derivation/RewriteStep | A rewrite step in this derivation. |
| termMetrics | Object | true | https://uor.foundation/derivation/Derivation | https://uor.foundation/derivation/TermMetrics | Metrics for the canonical term produced by this derivation. |
| from | Object | true | https://uor.foundation/derivation/RewriteStep | https://uor.foundation/schema/Term | The term before this rewrite step. |
| to | Object | true | https://uor.foundation/derivation/RewriteStep | https://uor.foundation/schema/Term | The term after this rewrite step. |
| hasRewriteRule | Object | true | https://uor.foundation/derivation/RewriteStep | https://uor.foundation/derivation/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 | https://uor.foundation/derivation/RewriteRule | https://uor.foundation/op/Identity | The algebraic identity that grounds this rewrite rule. Links a RewriteRule to the op:Identity individual that justifies its application. |
| stepCount | Datatype | true | https://uor.foundation/derivation/TermMetrics | http://www.w3.org/2001/XMLSchema#nonNegativeInteger | The total number of rewrite steps in this derivation. |
| termSize | Datatype | true | https://uor.foundation/derivation/TermMetrics | http://www.w3.org/2001/XMLSchema#nonNegativeInteger | The number of nodes in the canonical term's syntax tree. |
| previousType | Object | true | https://uor.foundation/derivation/RefinementStep | https://uor.foundation/type/TypeDefinition | The type before this refinement step was applied. |
| appliedConstraint | Object | true | https://uor.foundation/derivation/RefinementStep | https://uor.foundation/type/Constraint | The constraint that was applied in this refinement step. |
| refinedType | Object | true | https://uor.foundation/derivation/RefinementStep | https://uor.foundation/type/TypeDefinition | The type after this refinement step was applied. |
| sitesClosed | Datatype | true | https://uor.foundation/derivation/RefinementStep | http://www.w3.org/2001/XMLSchema#nonNegativeInteger | The number of site coordinates pinned by this refinement step. |
| stepIndex | Datatype | true | https://uor.foundation/derivation/SynthesisStep | http://www.w3.org/2001/XMLSchema#nonNegativeInteger | Zero-based sequential index of this step within the synthesis derivation. |
| addedConstraint | Object | true | https://uor.foundation/derivation/SynthesisStep | https://uor.foundation/type/Constraint | The constraint added in this synthesis step. |
| signatureBefore | Object | true | https://uor.foundation/derivation/SynthesisStep | https://uor.foundation/observable/SynthesisSignature | The constraint nerve signature before this synthesis step. |
| signatureAfter | Object | true | https://uor.foundation/derivation/SynthesisStep | https://uor.foundation/observable/SynthesisSignature | The constraint nerve signature after this synthesis step. |
| checkpointStep | Object | true | https://uor.foundation/derivation/SynthesisCheckpoint | https://uor.foundation/derivation/SynthesisStep | The SynthesisStep at which this checkpoint was taken. |
| checkpointState | Object | true | https://uor.foundation/derivation/SynthesisCheckpoint | https://uor.foundation/resolver/ConstraintSearchState | The ConstraintSearchState snapshot captured by this checkpoint. |
| towerCheckpoint | Object | false | https://uor.foundation/resolver/TowerCompletenessResolver | https://uor.foundation/derivation/SynthesisCheckpoint | Links a TowerCompletenessResolver to a SynthesisCheckpoint issued at each completed step. Cross-namespace bridge property: domain is resolver:TowerCompletenessResolver. |
| priorState | Object | true | https://uor.foundation/derivation/InhabitanceStep | https://uor.foundation/resolver/ConstraintSearchState | The ConstraintSearchState before this InhabitanceStep was taken. |
| successorState | Object | true | https://uor.foundation/derivation/InhabitanceStep | https://uor.foundation/resolver/ConstraintSearchState | The ConstraintSearchState after this InhabitanceStep was taken. |
| rule | Object | true | https://uor.foundation/derivation/InhabitanceStep | https://uor.foundation/predicate/DispatchRule | The predicate:DispatchRule whose evaluation drove this InhabitanceStep. |
| checkpointIndex | Datatype | true | https://uor.foundation/derivation/InhabitanceCheckpoint | http://www.w3.org/2001/XMLSchema#integer | Ordinal index of this checkpoint within the InhabitanceSearchTrace's checkpoint sequence. |
| traceEventCount | Datatype | true | https://uor.foundation/derivation/DerivationTrace | http://www.w3.org/2001/XMLSchema#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 | Properties | Comment |
|---|---|---|---|
| CriticalIdentityRule | https://uor.foundation/derivation/RewriteRule |
| The rewrite rule applying the critical identity: neg(bnot(x)) → succ(x). Grounded in op:criticalIdentity. |
| InvolutionRule | https://uor.foundation/derivation/RewriteRule | — | The rewrite rule applying involution cancellation: f(f(x)) → x for any involution f. |
| AssociativityRule | https://uor.foundation/derivation/RewriteRule | — | The rewrite rule applying associativity to re-bracket nested binary operations. |
| CommutativityRule | https://uor.foundation/derivation/RewriteRule | — | The rewrite rule applying commutativity to reorder operands of commutative operations. |
| IdentityElementRule | https://uor.foundation/derivation/RewriteRule | — | The rewrite rule eliminating identity elements: add(x, 0) → x, mul(x, 1) → x, xor(x, 0) → x. |
| NormalizationRule | https://uor.foundation/derivation/RewriteRule | — | The rewrite rule normalizing compound expressions to canonical ordering (e.g., sorting operands by address). |