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	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.

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.

Named Individuals

Name	Type	Properties	Comment
CriticalIdentityRule	`https://uor.foundation/derivation/RewriteRule`	`groundedIn`: `https://uor.foundation/op/criticalIdentity`	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).