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:

julia

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

julia

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)

Generalization works upward in this lattice: from specific constraints to general ones.

API

Constraint Extraction

extract_constraints(navigator::Navigator) :: Vector{Constraint} Pulls constraints from a compiled Navigator.

julia

nav = @late_nav([ALL, pred(x -> iseven(x) && x > 0)])
constraints = extract_constraints(nav)
# => [
#      Constraint(:even, iseven, proof=...),
#      Constraint(:positive, x > 0, proof=...)
#    ]

named_constraint(name::Symbol, predicate::Function) :: Constraint Creates a named, reusable constraint.

julia

constraint_even = named_constraint(:even, iseven)
constraint_gt5 = named_constraint(:gt5, x -> x > 5)
constraint_string = named_constraint(:string, x -> isa(x, String))

Constraint Composition

compose_constraints(c1::Constraint, c2::Constraint) :: ComposedConstraint Combines two constraints, proving they're satisfiable together.

julia

c_even = named_constraint(:even, iseven)
c_positive = named_constraint(:positive, x > 0)

c_composed = compose_constraints(c_even, c_positive)
# => ComposedConstraint(
#     name: :even_and_positive,
#     predicate: x -> iseven(x) && x > 0,
#     proof: (satisfiable evidence),
#     refinement_type: EvenPositiveInt
#   )

compose_constraints(constraints::Vector) :: ComposedConstraint Composes multiple constraints at once.

julia

constraints = [
  named_constraint(:even, iseven),
  named_constraint(:gt5, x -> x > 5),
  named_constraint(:lt100, x -> x < 100)
]

composed = compose_constraints(constraints)
# => Constraint proven satisfiable for ints in [6, 8, 10, ..., 98]

Constraint Generalization

generalize_constraint(constraint::Constraint) :: GeneralConstraint Finds the most general constraint that subsumes the given one.

julia

c_eq42 = named_constraint(:eq42, x -> x == 42)
general = generalize_constraint(c_eq42)
# => :positive (42 is positive—more general)
# => Or :nonzero, :nonnegative, etc. (depending on strategy)

abstract_constraint(constraint::Constraint, level::Int) :: GeneralConstraint Applies abstract interpretation to weaken constraints.

julia

c_detailed = named_constraint(:detailed, x -> iseven(x) && x > 5 && x < 100)

abstract_constraint(c_detailed, 1)  # Weaken slightly
# => iseven(x) && x > 5

abstract_constraint(c_detailed, 2)  # Weaken more
# => iseven(x)

abstract_constraint(c_detailed, 3)  # Very weak
# => numeric(x)  # Only knows it's a number

Refinement Types

refine_type(base_type::Type, constraint::Constraint) :: RefinementType Creates a refined type with proven constraint.

julia

refine_type(Int, named_constraint(:even, iseven))
# => RefinementType(Int, :even)
# Meaning: "An Int that is proven even"

refine_type(String, named_constraint(:nonempty, x -> length(x) > 0))
# => RefinementType(String, :nonempty)
# Meaning: "A String that is proven non-empty"

Proof Certificates

generate_proof(constraint::Constraint) :: ProofCertificate Creates a formal proof that the constraint is satisfiable.

julia

c = named_constraint(:even_positive, x -> iseven(x) && x > 0)
proof = generate_proof(c)
# => ProofCertificate(
#     constraint: c,
#     witnesses: [2, 4, 6, 8, ...],  # Examples that satisfy
#     satisfiability: SAT,             # Satisfiable
#     hardness: #P,                    # Complexity class
#     explanation: "Constraint is satisfiable; even positive integers exist"
#   )

Constraint Propagation

Once constraints are proven, they propagate through compositions:

Path A: X → even(X)
Path B: Y → positive(Y)

Compose A then B:
  => even(X) ∧ positive(Y)
  => If Y = A(X), then: positive(even(X))
  => Generalization: IntegersEvenAndPositive type

Compose again with Path C:
Path C: Z → Z < 100

  => even(X) ∧ positive(Y) ∧ (Y < 100)
  => Refines to: {2, 4, 6, ..., 98}

Integration with 3-MATCH

Constraint composition uses 3-MATCH for satisfiability:

julia

constraints = [
  :even,        # iseven(x)
  :positive,    # x > 0
  :lt100        # x < 100
]

# 3-MATCH checks:
# Satisfiable? (iseven(x) ∧ x > 0 ∧ x < 100)
# => YES: x ∈ {2, 4, 6, ..., 98}

# If constraints were contradictory:
constraints_bad = [:even, :odd]  # Can't be both!
# => 3-MATCH: UNSAT
# => Reject composition

Integration with Type Inference

Refined types emerge from constraint composition:

julia

nav = @late_nav([ALL, pred(x -> iseven(x) && x > 0)])

# Type inference sees:
# Input: Vector{Int}
# Constraints: [even, positive]
# Output type: Vector{EvenPositiveInt}  ← Refined!

sig = navigator_signature(nav)
# => TypeSignature(
#     input: Vector{Int},
#     output: Vector{EvenPositiveInt},  # Refined output type!
#     constraints: [even, positive],
#     proof: ...
#   )

Constraint Algebra

Constraints form an algebraic structure under generalization:

Lattice operations:
  even ∧ positive = even_positive    (Meet/AND)
  even ∨ positive = numeric           (Join/OR, generalize)
  ¬even = odd                         (Complement)
  ⊤ = True                           (Top, no constraint)
  ⊥ = False                          (Bottom, unsatisfiable)

Example derivations:
  even ∧ positive → nonnegative  (generalization)
  odd ∧ gt5 → numeric            (upper bound)
  string ∧ nonempty → string     (redundant, but valid)

Practical Examples

Example 1: Filtering Pipeline

julia

# Stage 1: Filter for positive numbers
nav1 = @late_nav([ALL, pred(x -> x > 0)])
constraints1 = extract_constraints(nav1)
# => [:positive]

# Stage 2: Further filter for even
nav2 = @late_nav([ALL, pred(iseven)])
constraints2 = extract_constraints(nav2)
# => [:even]

# Compose stages
final_constraints = compose_constraints(
  constraints1[1],
  constraints2[1]
)
# => Constraint(:even_positive, x -> iseven(x) && x > 0)

# Proof:
proof = generate_proof(final_constraints)
# => Witnesses: [2, 4, 6, 8, ...]

Example 2: Product Navigation with Constraints

julia

# Navigate to (x, y) pairs where x is positive and y is negative
nav = @tuple_nav([:x, :y])

constraints = compose_constraints([
  named_constraint(:x_positive, px -> px > 0),
  named_constraint(:y_negative, py -> py < 0)
])

# Refined output type: Tuple{PositiveInt, NegativeInt}

Example 3: Iterative Constraint Refinement

julia

# Start with loose constraint
c1 = named_constraint(:numeric, x -> isnumeric(x))

# Refine iteratively
c2 = compose_constraints(c1, named_constraint(:positive, x -> x > 0))
# => numeric ∧ positive = positive

c3 = compose_constraints(c2, named_constraint(:even, iseven))
# => positive ∧ even = even_positive

c4 = compose_constraints(c3, named_constraint(:lt100, x -> x < 100))
# => even_positive ∧ lt100 = {2, 4, 6, ..., 98}

Error Handling

Unsatisfiable constraints:

julia

c_even = named_constraint(:even, iseven)
c_odd = named_constraint(:odd, isodd)

compose_constraints(c_even, c_odd)
# => UnsatisfiableConstraintError("No integer is both even and odd")

Type conflicts:

julia

c_string = named_constraint(:string, x -> isa(x, String))
c_numeric = named_constraint(:numeric, x -> isnumeric(x))

compose_constraints(c_string, c_numeric)
# => TypeError("String and Numeric constraints are disjoint")

Performance

Operation	Complexity	Notes
extract_constraints	O(n)	n = path length
compose_constraints	O(m³)	m = number of constraints (SAT checking)
generalize_constraint	O(1)	Pre-computed lattice
refine_type	O(1)	Type annotation
generate_proof	O(2^m)	SAT solver on constraint space

Note: Proof generation is expensive but cached—proofs are reused.

Related Skills

type-inference-validation - Proves constraint satisfiability
tuple-nav-composition - Applies generalized constraints to products
specter-navigator-gadget - Navigator system that uses constraints
three-match - Underlying SAT solver for constraint composition
color-envelope-preserving - Maintains GF(3) along with constraints

References

Constraint logic programming: "Introduction to CLP" - Jaffar & Maher
Refinement types: "Refinement Types for TypeScript" - Rondon et al.
Abstract interpretation: "The Cousot-Cousot Approach to Program Analysis" - Cousot
Proof assistants: "Formal Proof Assistants" - Coq/Isabelle documentation

Search AI Tools

constraint-generalization

Install this agent skill to your Project

SKILL.md

Constraint Generalization

Core Concept

Why Constraint Generalization?

Architecture

Constraint Representation

Constraint Composition

Constraint Lattice

API

Constraint Extraction

Constraint Composition

Constraint Generalization

Refinement Types

Proof Certificates

Constraint Propagation

Integration with 3-MATCH

Integration with Type Inference

Constraint Algebra

Practical Examples

Example 1: Filtering Pipeline

Example 2: Product Navigation with Constraints

Example 3: Iterative Constraint Refinement

Error Handling

Performance

Related Skills

References