FPRD LabShare an approach

Left-quotient finite audit

Run:

python3 check_left_quotient.py

The checker compares two independently implemented finite procedures for each test case:

  1. the published-page construction, which interprets the quotienting regular expression as a relation on the normalized derivative carrier of the target expression; and
  2. a synchronized derivative-product oracle, which searches for a prefix accepted by the quotienting expression and then tests the supplied suffix in the reached target state.

The finite domain contains 27 quotienting expressions, 15 target expressions, and all 31 binary suffixes of length at most four. This gives 12,555 membership comparisons. The certificate records zero mismatches and a transcript digest.

The same corpus also runs four negative controls that inject errors into the construction side only:

  1. reverse the order of relational composition for concatenation;
  2. replace reflexive-transitive star closure by paths of length at most one;
  3. reverse every letter-transition edge; and
  4. forget that quotient reachability must start at the target expression.

All four controls are detected. The certificate preserves the mismatch count and first failing witness for each; notably, the truncated-star error has only two witnesses in this corpus. These controls show that the audit is sensitive to the four named proof obligations. They are not evidence that every possible implementation error would be detected.

The second checker is a common-mode audit:

python3 check_antimirov_independent.py

It parses a separately listed infix corpus into an unsimplified binary syntax tree, implements Antimirov partial derivatives for the construction, and uses Thompson epsilon-NFAs with subset-product reachability as the oracle. It shares the fixed expression strings, alphabet, and case order with the first audit, but does not share regular-expression normalization, nullability, derivative code, or acceptance logic. Its 12,555 decisions have zero mismatches and the same semantic transcript digest as the first audit. The independent certificate records the exact implementation boundary.

This is a new replacement audit. It deliberately has the same comparison count as the unavailable historical check, but it does not claim to reproduce that check’s exact expression corpus or implementation.