UOR Bounded Recursion
- IRI
https://uor.foundation/recursion/- Prefix
recursion:- Space
- kernel
- Comment
- Self-referential computations with well-founded descent measures guaranteeing termination.
Imports
https://uor.foundation/op/https://uor.foundation/schema/https://uor.foundation/predicate/https://uor.foundation/morphism/https://uor.foundation/effect/https://uor.foundation/failure/https://uor.foundation/trace/
Classes
| Name | IRI | Subclass Of | Disjoint With | Comment |
|---|---|---|---|---|
| BoundedRecursion | https://uor.foundation/recursion/BoundedRecursion | http://www.w3.org/2002/07/owl#Thing | A self-referential computation parameterized by a descent measure. Each recursive step strictly decreases the measure; the computation terminates when the base case predicate is satisfied. | |
| DescentMeasure | https://uor.foundation/recursion/DescentMeasure | http://www.w3.org/2002/07/owl#Thing | A well-founded function from computation state to xsd:nonNegativeInteger. Strictly decreases on every recursive step. | |
| BaseCase | https://uor.foundation/recursion/BaseCase | https://uor.foundation/predicate/MatchArm | The match arm selected when the descent measure reaches zero or the base predicate is satisfied. Produces a direct result without further recursion. | |
| RecursiveCase | https://uor.foundation/recursion/RecursiveCase | https://uor.foundation/predicate/MatchArm | The match arm selected when the descent measure is positive. Applies a decomposition step, decreases the measure, and invokes the recursion. | |
| RecursiveStep | https://uor.foundation/recursion/RecursiveStep | http://www.w3.org/2002/07/owl#Thing | A single step in a bounded recursion: the decomposition applied before the recursive invocation. Must strictly decrease the DescentMeasure. | |
| RecursionTrace | https://uor.foundation/recursion/RecursionTrace | https://uor.foundation/trace/ComputationTrace | A computation trace recording the sequence of recursive steps, measure values, and the base case result. The trace length is bounded by the initial measure value. | |
| StructuralRecursion | https://uor.foundation/recursion/StructuralRecursion | https://uor.foundation/recursion/BoundedRecursion | A bounded recursion where the descent measure is the structural size of the input type (site count, constraint count, or operad nesting depth). |
Properties
| Name | Kind | Functional | Domain | Range | Comment |
|---|---|---|---|---|---|
| measure | Object | true | https://uor.foundation/recursion/BoundedRecursion | https://uor.foundation/recursion/DescentMeasure | The descent measure guaranteeing termination. |
| baseCase | Object | true | https://uor.foundation/recursion/BoundedRecursion | https://uor.foundation/recursion/BaseCase | The base case match arm. |
| recursiveCase | Object | true | https://uor.foundation/recursion/BoundedRecursion | https://uor.foundation/recursion/RecursiveCase | The recursive case match arm. |
| stepDecomposition | Object | true | https://uor.foundation/recursion/RecursiveStep | https://uor.foundation/morphism/Transform | The transform applied to decompose the input before recursion. |
| stepMeasurePre | Object | true | https://uor.foundation/recursion/RecursiveStep | https://uor.foundation/recursion/DescentMeasure | The measure value before this step. |
| stepMeasurePost | Object | true | https://uor.foundation/recursion/RecursiveStep | https://uor.foundation/recursion/DescentMeasure | The measure value after this step. |
| basePredicate | Object | true | https://uor.foundation/recursion/BoundedRecursion | https://uor.foundation/predicate/Predicate | The predicate that identifies the base case. |
| recursionBody | Object | true | https://uor.foundation/recursion/BoundedRecursion | https://uor.foundation/morphism/ComputationDatum | The computation applied at each recursive step (may reference itself via its content address). |
| initialMeasure | Datatype | true | https://uor.foundation/recursion/BoundedRecursion | http://www.w3.org/2001/XMLSchema#nonNegativeInteger | The measure value at the start of recursion. Bounds the maximum recursion depth. |
| measureValue | Datatype | true | https://uor.foundation/recursion/DescentMeasure | http://www.w3.org/2001/XMLSchema#nonNegativeInteger | The current value of the descent measure. |