Skip to main content

Module minimize

Module minimize 

Source
Expand description

Schema minimization: partition-refinement to the canonical minimal form. Ported from ~/dev/omnist/omnist/ops/minimize.py.

normalize(s) returns an equivalent schema with the fewest possible env records, unique up to record naming (paper Theorems 3-4).

Algorithm:

  1. s = prune(s) – mandatory first step. Two semantically-equal records must not be kept apart by never-emittable fields or unreachable records; pruning first is what makes the partition canonical.
  2. Initial partition: env records grouped by local_signature – a target-blind structural key, so records that might turn out equivalent via differently-named ref targets still start in the same block.
  3. Refine: split any block whose members disagree, for some label, on which block their same-labeled ref-typed field points to. Repeat until no block splits (a fixpoint – always reached on a finite env).
  4. Merge: collapse each stable block to a single representative – its lexicographically smallest member name (deterministic) – and remap every ref and the root to representatives.

Special case: an unsatisfiable (empty-language) root. prune deliberately leaves such a root’s fields untouched (see its own doc comment), so partition refinement over the unsatisfiable core isn’t meaningful – normalize just returns the pruned schema unchanged in that case.

Functions§

equivalence_classes
Partitions s.env’s record names into structural-equivalence classes via MinimizeSA-style partition refinement (module doc comment, steps 2-3): an initial local_signature grouping refined to a fixpoint by which block each same-labeled ref field points to.
normalize
The canonical minimal schema equivalent to s: fewest env records, unique up to record naming. See the module doc comment for the algorithm (paper’s Algorithm 2, MinimizeSA).