# All reduction orders through length 4

KL-FCS-034 · Term rewriting · version 1.0.0

## Problem

Establish a unique sorted normal form for every bounded binary word.

## Context

Inspect every allowed reduction order in a finite family, and compare all reachable normal forms.

## Definitions

- **Rewrite rule**: A permitted local replacement; here 10 → 01.
- **Normal form**: A word containing no reducible 10 substring.
- **Confluence on a domain**: Every reduction path from each declared input can reach a common result.

## Checked result

Unique normal forms on the domain: yes.

The checker explores every enabled rewrite, not just the trace shown. Each result preserves the symbol multiset and reaches a block of zeros followed by ones.

## Checker reasoning

1. Enumerate every binary word through the declared length.
2. Explore all possible one-step adjacent rewrites.
3. Collect terminal words, memoizing the reduction graph.
4. Require one normal form per input and replay the supplied concrete trace.

## Dataset construction

{
  "family": "rewriting",
  "task": "Establish a unique sorted normal form for every bounded binary word.",
  "input_encoding": "Structured JSON; field meanings are stated in the specification.",
  "coverage": "All reduction paths over 31 bounded inputs",
  "acceptance": [
    "Enumerate every binary word through the declared length.",
    "Explore all possible one-step adjacent rewrites.",
    "Collect terminal words, memoizing the reduction graph.",
    "Require one normal form per input and replay the supplied concrete trace."
  ],
  "generation": "Deterministic finite fixture; full enumeration or witness replay as stated.",
  "split_policy": "Reference corpus for exposition and reproduction; no train/test evaluation split is claimed."
}

## Formal payload

```json
{
  "specification": {
    "max_length": 4,
    "rule": [
      "10",
      "01"
    ],
    "sample_word": "1100"
  },
  "claim": {
    "unique_normal_forms": true
  },
  "witness": {
    "trace": [
      "1100",
      "1010",
      "0110",
      "0101",
      "0011"
    ]
  }
}
```

## Complexity

Each rewrite decreases the number of inverted 1-before-0 pairs. Exhaustive graph exploration is restricted to the stated length.

## Limits

The mechanical confluence result is restricted to the declared finite word family.

## Common error and further work

Two chosen reduction strategies agreeing does not establish that all strategies agree.

Publish a general inversion-measure termination argument and a separately checked confluence proof.

## Verification

All reduction paths over 31 bounded inputs. 31 checker units.
Replay with `python3 tools/verify.py`. Mechanical status: checked; human review
has not yet been recorded. Custom Python verification, not a proof-assistant
claim. Checker 1.0.0 and exact source hashes are in `verification.json`.

## Provenance and references

Original Kenton Labs reference instance, authored with Codex assistance on 2026-10-11.
No external dataset or model-generation experiment. Reuse-license selection
remains pending.

- [Conceptual reference](https://isa-afp.org/entries/Abstract-Rewriting.html)