constraint-generalization

Constraint Generalization

Core Concept

Given proven constraints on individual paths, synthesize new constraints that hold across composed paths. This skill moves from "validation" (rejecting bad paths) to "generation" (creating better paths).

Example: If path A proves outputs are even, and path B proves outputs are positive, the composed path AB proves outputs are both even AND positive.

Why Constraint Generalization?

Without it, constraints are lost during composition:

nav_even = @late_nav([ALL, pred(iseven)])      # proves: even
nav_positive = @late_nav([ALL, pred(x > 0)])   # proves: positive

# Compose them:
nav_composed = compose_navigators(nav_even, nav_positive)
# What can we prove about the result?
# Without generalization: nothing! Constraints are forgotten.

# With generalization:
# => Proves: even(x) ∧ positive(x)
# => More refined type: EvenPositiveInt

This refinement typing enables:

• Automatic constraint propagation downstream
• Fewer re-checks (prove once, use many times)
• Smarter composition (know which paths can combine)
• Proof generation (formal certificates for constraints)

Architecture

Constraint Representation

struct Constraint
    predicate::Function           # The boolean test
    name::Symbol                  # :even, :positive, :non_null, ...
    arity::Int                    # 1 for unary, 2 for binary, etc.
    proof::Proof                  # Evidence constraint holds
    refinement_type::RefinementType  # Int → EvenInt
end

Constraint Composition

CNF (Conjunctive Normal Form) for constraint composition:

C₁ ∧ C₂ ∧ C₃ = (iseven AND positive AND nonzero)

Satisfiable? Check via 3-MATCH:
  - Find x where iseven(x) ∧ positive(x) ∧ nonzero(x)
  - If no x exists → constraints are contradictory
  - If x exists → constraints compose validly

Constraint Lattice

        ⊤ (True, no constraint)
       / \
    even  odd
     / \   / \
    ... ∧ ... (conjunctions)
     \ /   \ /
     ⊥ (False, unsatisfiable)