constraint-generalization

Files (1)

• SKILL.md

SKILL.md (first lines)

# 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.

From plurigrid/asi, MIT.

More from plurigrid/asi