Type Synthesis
Definition
Type synthesis is the process of running the ψ-pipeline in inverse mode: given a target topological signature (Euler characteristic χ* and Betti profile β*), the TypeSynthesisResolver searches the space of constraint combinations and produces a SynthesizedType that achieves the target.
A TypeSynthesisGoal carries the target signature via targetEulerCharacteristic (functional, one χ* value) and targetBettiNumber (non-functional, one assertion per Betti degree).
Output Classes
A successful synthesis run produces:
- TypeSynthesisResult — the abstract result record linking goal to synthesized type.
- SynthesizedType — a ConstrainedType distinguished by a synthesisResult link.
- MinimalConstraintBasis — the smallest set of constraints sufficient to realise the target signature, with basisSize giving the cardinality.
Search State
The resolver maintains a ConstraintSearchState tracking explored combinations (exploredCount) and the current candidate (currentCandidate). Each step in the construction is recorded as a SynthesisStep ordered by stepIndex.
Intermediate topological signatures are captured in SynthesisSignature individuals with realisedEuler and realisedBetti assertions.
Identity Algebra (TS_ series)
| Identity | Statement |
|---|---|
| TS_1 | ∃ SynthesizedType T realising target iff χ* ≤ n and β₀*=1, βₖ*=0 k≥1 |
| TS_2 | basisSize(T) = n for an n-site target |
| TS_3 | χ(T + constraint) ≥ χ(T) for any synthesis candidate |
| TS_4 | TypeSynthesisResolver takes ≤ n steps for a realisable n-site target |
| TS_5 | SynthesizedType achieves IT_7d iff CompletenessResolver certifies CompleteType |
| TS_6 | Expected steps with Jacobian-guided search is O(n log n) |
| TS_7 | β₀(non-empty ConstrainedType) ≥ 1 |