Expand description
Subschema compatibility and equivalence. Ported from
~/dev/omnist/omnist/ops/subschema.py.
Implements the paper’s Algorithm 4 (SubschemaSA) restricted to omnist’s
counting cardinality languages; equivalent is bidirectional
inclusion.
Algorithm 4 assumes its precondition MakeUsefulSA (useless-state removal,
super::prune) has already run: the coinductive cycle rule below only
coincides with true (finite-document) language inclusion once every
A-side record is known satisfiable. Rather than requiring callers to
pre-prune, compatible_with computes a’s satisfiable set once up
front and consults it directly – an unsatisfiable A-side record is
vacuously a subschema of anything (it emits no documents at all), and an
optional A-field whose type is unsatisfiable is skipped (it can never
actually be emitted, so it imposes no obligation on B).
Functions§
- compatible_
with - True if every document
aaccepts is also accepted byb(ais a subschema /bis backward-compatible). - equivalent
- True if both schemas accept exactly the same documents.