Partial Recursive Signatures
A response (2026-05-23) to a collaborator’s concern about partial recursive signatures in the recursive modules system: when is a signature exposing only some recursive equations well-behaved?
The observation
Signature traversal is acyclic; only the leaf type equations are recursive.
So a partial view (exposing some components, hiding others) is sound provided the recursion is confined to leaf type-field equations, not to the structural traversal of the signature.
Worked shape: Tree / Forest
Mutually recursive Tree and Forest admit partial views — each exposes its own type equation while referring to the other’s external view.
Side conditions for a valid partial recursive signature
- type fields only — the recursive equations are over type components, not value components;
- contractive equations — each recursive equation is contractive (no immediate self-reference);
- scoped / component-local visibility — strengthening is visible only where it should be;
- compatibility of partial equation witnesses — the exposed witnesses must agree with the hidden ones.
Related
Double-Vision Recursive Modules · Locator-Anchored Signatures · project note Recursive floating type fields as partial recursive signatures