Program Hypergraph

The Program Hypergraph (PHG) is the Program Semantic Graph with explicit directed relations of arbitrary source arity. A relation retains the participants of a joint requirement: buffers sharing a capacity budget, the ordered operands of a geometric operation, or mesh elements sharing a boundary. A binary graph can encode the same relation using a relation node and role-labelled links. Ordered hyperedges make that identity direct and available to the analyses that need it. Pairwise equality of locations already establishes a common location; checking whether all buffers fit there additionally requires their joint resource constraint.

The program’s semantic nodes and structural/reference relationships remain its computational spine. A local fact may remain a node coeffect. When its justification depends on several participants, the PHG retains that incidence, the premises, and the applicable rule as a joint relation. Elaboration can construct operational nodes as well as analysis relations. These are different roles within one graph; an obligation edge is not an executable instruction. The lattice used by an analysis orders its information, not the graph’s topology.

1. Structure

A directed hyperedge is a triple $f = (I_f, t_f, \lambda_f)$: an ordered sequence of source occurrences $I_f = (v_1,\ldots,v_k)$, a single target node $t_f \in V$, and a hyperedge annotation $\lambda_f$. The same node may occupy more than one input position. The PHG is the tuple $(V, F, \alpha, \beta)$ where $V$ is the node set with its vertex annotation function $\alpha$ (type, dimension, coeffect, and lifetime annotations), $F$ is the hyperedge set, and $\beta$ assigns each hyperedge its relational annotation. Write $S_f$ for the set of nodes occurring in $I_f$ when only dependency membership is needed.

1. A binary PSG edge SHALL be represented as the degenerate hyperedge with $|I_f| = 1$.
2. Every valid PSG SHALL be a valid PHG under that embedding, and every PSG discipline of this specification (saturation, coeffect carriage, node activation, enrichment) SHALL apply without modification when restricted to binary hyperedges.
3. A hyperedge’s source occurrences and their roles SHALL be enumerated at elaboration before a constraint over that relation is discharged. This establishes a finite static incidence, not a bound on the number of runtime instances or on data reachable through a participant.
4. A relation SHALL preserve source order and multiplicity unless its declared interpretation justifies a permutation or identifies repeated occurrences. Dependency scheduling MAY use $S_f$ without replacing the operational input sequence $I_f$.

Finite incidence permits obligations about those participants to be generated explicitly. It does not by itself make their propositions quantifier-free, decidable, or cheap to check. Each admitted rule SHALL specify the meaning of its obligations and the inference or verification procedure that establishes them. The procedures and their composition remain subject to the owning domain contracts (Grade Discipline §4.1).

2. Hyperedge Annotations

The annotation $\lambda_f$ SHALL carry a relational kind and a target-reachability bitvector, and MAY carry kind-specific fields:

A kind-specific field SHALL be interpreted only by the analyses and pathways that declare that kind; an unrecognized kind on a target where the reachability bit is clear imposes no obligation.

3. Saturation

Saturation applies admitted elaboration and analysis rules until the facts required by a demanded compilation boundary are established. Each analysis has its own information domain and transfer rules. Lifecycle labels such as Fresh, Elaborated, and Saturated summarize progress; they do not supply the domain’s convergence proof or a complexity bound.

1. An inference rule SHALL identify the premises required for each conclusion. It MAY derive a sound partial result while other facts remain pending, but SHALL NOT assume an unavailable premise or omit a participant required by that conclusion. Changed premises SHALL cause dependent conclusions to be reconsidered or invalidated.
2. Recursive analysis components SHALL use a worklist or an equivalent procedure with a sound convergence policy for their domains. Requiring every participant to be globally saturated before any rule can run SHALL NOT substitute for handling an inference cycle.
3. For a fixed finite collection of finite-height annotation domains, monotone inflationary rules with fair scheduling reach a fixed point after finitely many successful updates. An analysis with an infinite ascending chain SHALL provide a separate termination argument or sound acceleration policy, such as widening followed by an admitted narrowing procedure. Structural elaboration that generates further nodes or rules also requires its own termination argument. No $O(|V|+|F|)$ iteration bound follows from lifecycle labels alone.
4. A known contradiction SHALL be diagnosed under Conformance §5. An unsupported, cancelled, timed-out, or otherwise unresolved required obligation SHALL remain pending during partial analysis and SHALL prevent the commitment that relies on it. Quiescence of an incomplete graph is not witness readiness.
5. A multi-way constraint SHALL NOT be replaced by weaker pairwise projections. A decomposition is permitted when its declared rule establishes the required preservation or sound implication and retains the original relation’s provenance.

Constraint propagation may carry requirements from uses toward definitions as well as facts toward uses. This analysis-time direction does not reverse runtime effects or solve an arbitrary recursively defined value. Any admitted runtime cycle, delayed computation, or dynamic matching operation requires its own operational contract and realization.

4. Constraint Discharge

Hyperedge constraints SHALL use the admitted procedures of the node-level annotation disciplines. Under the separate-discharge contract of Grade Discipline §4.1, a relation spanning families SHALL produce per-family obligation projections rather than a combined query. The projections SHALL retain their common participants, premises, and dependencies. Separate variable names or separate solver calls do not establish semantic independence: any fact exchanged between domains SHALL have a sound transfer rule, and a changed premise SHALL invalidate its dependents.

The owning obligation determines its theory. Dimensional equations, blade-support calculations, resource inequalities, and synchronization predicates need not use the same procedure. A finite wait-for acyclicity check can use integer rank constraints (Synchronous RPC and Wait Classification); that certificate establishes program progress only under the wait-completeness and execution assumptions of its contract. A solver result SHALL justify the required proposition under its stated premises, not merely demonstrate a compatible assignment.

5. Emission Transport

A hyperedge is an analysis-time structure. It participates in saturation and constraint discharge; it is not a query target for code generation.

1. A hyperedge’s consequence SHALL reach emission in exactly one of two forms: as saturated annotations on the nodes it governs, read as codata during lowering (Backend Lowering Architecture §4.5), or as a reified annotation, an attribute set on emitted operations that a later pass consumes.
2. The emission traversal SHALL NOT query the hyperedge set. The zipper elides only what the graph has already saturated (Closure Representation §11); its context is positional, and every semantic fact it consumes is node-local codata or reified structure.
3. A backend pass that consumes a multi-way constraint (a partitioner consuming co-location constraints, a tile-assignment pass) SHALL consume the reified annotation, not the graph hyperedge.
4. The stage separation of Grade Discipline §3.3.1 applies to every hyperedge annotation: present on the PHG, read during lowering, absent from emitted MLIR except where reified deliberately under item 1.

Clef Note: The two forms of item 1 are one rule with two carriers. Node-local codata carries settled consequences such as a sparse layout or storage placement. Reification carries an annotation a backend pass must still consume, such as the co-location annotation on the operations a partitioner groups. CCS/Baker elaborates a $k$-ary geometric operation’s sparse arithmetic and settles its joint premises before publication (Grade Discipline §5.3). Alex witnesses the resulting operations and reads their settled local facts. It does not enumerate the hyperedge’s participants or derive a layout or arithmetic construction during emission.

The witness SHALL retain or establish the correspondence between each consumed fact and the operations that realize it. A later transformation SHALL preserve that correspondence through an admitted rule or re-establish the affected property. Copying an attribute alone does not meet this requirement. Static discharge may justify an executable dynamic check or protocol; it does not establish the outcome of an unknown runtime input.

5.1 Scoped re-evaluation and witness authorization

A compiler that reuses analysis or emitted artifacts across source changes SHALL identify the accepted checked revision to which each current judgment belongs. The revision identifier SHALL distinguish revisions within its compilation session. Region identity, artifact content identity and an individual traversal’s identity SHALL remain separately identifiable. A timestamp or content match alone SHALL NOT authorize a result for the accepted revision.

The source analysis SHALL determine the affected semantic region from the changed facts and their complete dependencies. These dependencies SHALL include the participants of joint constraints, consumed rule and declaration identities, and any collection membership or absence on which a judgment relies. Adding a previously absent participant SHALL invalidate dependent conclusions. Where precise support is unavailable, the compiler SHALL conservatively re-evaluate the complete owning analysis region. Dependency propagation SHALL account for effects, captures, inferred type and dimension instances, representations, layout and proof premises whenever they support the affected judgment.

After the required elaboration and saturation, the source analysis SHALL supply the witness with an authorized collection of scopes. Each scope SHALL identify its checked revision, actual source occurrences and traversal context, settled boundary contracts, and the artifacts it replaces or retires. The whole checked program MAY be one such scope. A Huet zipper SHALL navigate those authorized occurrences while preserving their context. Scope selection and dependency closure remain source-analysis responsibilities; emission SHALL obey §5’s transport rules within each scope.

A changed dependency structure MAY split or merge regions. The replacement account SHALL cover every affected definition, storage allocation and activation owner, including objects removed by the new partition. Reuse SHALL require validation of the reused artifact’s consumed premises and boundary contracts against the accepted revision. This requirement applies to semantic dependencies introduced by specialization, inlining or proof discharge as well as dependencies represented by retained calls. Equal physical signatures alone SHALL NOT justify reuse of a changed semantic contract.

The compiler SHALL publish diagnostics and executable artifacts only under the revision authorization governing their claimed source state. Superseded work SHALL NOT replace the accepted result. Reused content MAY originate in an older revision when its complete support has been revalidated for the accepted one. For live execution, replacement and retirement SHALL preserve the admitted lifetime and activation contracts of code and storage still in use.

Applied elaborations and proof transformations SHALL retain the correspondence between their source participants and current results through invalidation and replacement. Historical evidence SHALL remain distinguishable from current premises and executable roots. Artifact projections MAY omit inactive material only while preserving the correspondence required for the claims they expose.

6. Domain Instances

The rows below identify hyperedge kinds and the chapters that define their requirements.

7. Normative Requirements

1. Embedding: Every valid PSG SHALL be a valid PHG under the $|I_f| = 1$ embedding, with all PSG disciplines applying unchanged to binary hyperedges.
2. Enumerated occurrences: A hyperedge SHALL retain the enumerated positions, roles, order, and multiplicity required by its interpretation.
3. Sound inference: Every conclusion SHALL have its required premises; unresolved participants SHALL NOT become assumed facts. Sound partial inference is permitted.
4. Convergence and readiness: Each admitted analysis and structural elaboration SHALL provide the convergence or termination policy required by §3. Pending required facts SHALL prevent the dependent compilation commitment.
5. No weakening: Decomposition SHALL preserve the required joint conclusion and provenance under a justified rule.
6. Per-family discharge: A hyperedge spanning solver families SHALL retain coherent premises through separate per-family projections; exchanges between domains SHALL obey sound transfer rules.
7. Emission transport: A hyperedge’s consequence SHALL reach emission only as saturated node-local codata or as a reified annotation (an attribute set on emitted operations); the emission traversal SHALL NOT query the hyperedge set; a backend pass SHALL consume reified annotations only.
8. Diagnosis: A contradiction or a required unresolved obligation at commitment SHALL be diagnosed under Conformance §5. An admitted dynamic check SHALL retain its specified runtime success and failure behavior.
9. Scoped preservation: Reuse and scoped witnessing across source revisions SHALL obey §5.1’s dependency, authorization, replacement and provenance requirements.

8. Related Chapters

• Program Semantic Graph, the binary structure this chapter generalizes
• Grade Discipline, the annotation disciplines whose multi-way composition rules ride hyperedges
• Backend Lowering Architecture, carrier realization and the target pathways
• Synchronous RPC and Wait Classification, the wait-for relation whose tuples are hyperedge instances
• Conformance, the diagnostic obligation hyperedge discharge inherits

References

• Haynes, H. (2026). The Program Hypergraph: Multi-Way Relational Structure for Geometric Algebra, Spatial Compute, and Physics-Aware Compilation.
• Haynes, H. (2026). Dimensional Type Systems and Deterministic Memory Management. (DTS+DMM.)
• Karypis, G., Kumar, V. (2000). Multilevel k-way hypergraph partitioning. VLSI Design 11(3).