Formal Computer Science / Languages & logic

Kenton Labs / Languages & logic

Term rewriting

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

The vocabulary.

These definitions state the objects and properties used by the dataset. The complete instance specification remains the authority for each result.

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.

How the dataset works.

Three deterministic instances define this family. Each includes its input model, a checked result, evidence, and an acceptance procedure. Download the complete dataset JSON ↘ or the area’s readable source ↘.

Acceptance procedure

  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.

Cost and scope

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

A common failure

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

Explore the mechanics.

Change a local input or follow the steps. The stored result and its scope remain attached to the downloadable record.

Worked records.

Three instances expose concrete claims and the artifacts that establish or refute them. Expand a record for the problem, checker reasoning, formal payload, and verification metadata.

KL-FCS-034
Term rewritingAll reduction orders through length 4All reduction paths over 31 bounded inputs

The problem

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

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

Why the checker accepts it

  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.

Formal specification

{
  "max_length": 4,
  "rule": [
    "10",
    "01"
  ],
  "sample_word": "1100"
}

Claim and evidence

{
  "claim": {
    "unique_normal_forms": true
  },
  "witness": {
    "trace": [
      "1100",
      "1010",
      "0110",
      "0101",
      "0011"
    ]
  }
}

Dataset construction

Deterministic finite fixture; full enumeration or witness replay as stated. Structured JSON; field meanings are stated in the specification. Acceptance covers 31 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

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

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

A boundary to investigate

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 and provenance metadata

Mechanical status: checked. Human review: not yet recorded. Checker version 1.0.0, Python 3.9.6. The report contains source hashes. The trust boundary includes Python and the custom checker implementations; no proof-assistant validation is claimed.

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

Replay from the source bundle: python3 tools/verify.py.

Readable source ↘Record JSON ↘Full area ↗Related KL-FCS-035 ↘Related KL-FCS-036 ↘
KL-FCS-035
Term rewritingAll reduction orders through length 6All reduction paths over 127 bounded inputs

The problem

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

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

Why the checker accepts it

  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.

Formal specification

{
  "max_length": 6,
  "rule": [
    "10",
    "01"
  ],
  "sample_word": "101010"
}

Claim and evidence

{
  "claim": {
    "unique_normal_forms": true
  },
  "witness": {
    "trace": [
      "101010",
      "011010",
      "010110",
      "001110",
      "001101",
      "001011",
      "000111"
    ]
  }
}

Dataset construction

Deterministic finite fixture; full enumeration or witness replay as stated. Structured JSON; field meanings are stated in the specification. Acceptance covers 127 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

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

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

A boundary to investigate

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 and provenance metadata

Mechanical status: checked. Human review: not yet recorded. Checker version 1.0.0, Python 3.9.6. The report contains source hashes. The trust boundary includes Python and the custom checker implementations; no proof-assistant validation is claimed.

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

Replay from the source bundle: python3 tools/verify.py.

Readable source ↘Record JSON ↘Full area ↗Related KL-FCS-034 ↘Related KL-FCS-036 ↘
KL-FCS-036
Term rewritingAll reduction orders through length 8All reduction paths over 511 bounded inputs

The problem

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

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

Why the checker accepts it

  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.

Formal specification

{
  "max_length": 8,
  "rule": [
    "10",
    "01"
  ],
  "sample_word": "11110000"
}

Claim and evidence

{
  "claim": {
    "unique_normal_forms": true
  },
  "witness": {
    "trace": [
      "11110000",
      "11101000",
      "11011000",
      "10111000",
      "01111000",
      "01110100",
      "01101100",
      "01011100",
      "00111100",
      "00111010",
      "00110110",
      "00101110",
      "00011110",
      "00011101",
      "00011011",
      "00010111",
      "00001111"
    ]
  }
}

Dataset construction

Deterministic finite fixture; full enumeration or witness replay as stated. Structured JSON; field meanings are stated in the specification. Acceptance covers 511 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

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

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

A boundary to investigate

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 and provenance metadata

Mechanical status: checked. Human review: not yet recorded. Checker version 1.0.0, Python 3.9.6. The report contains source hashes. The trust boundary includes Python and the custom checker implementations; no proof-assistant validation is claimed.

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

Replay from the source bundle: python3 tools/verify.py.

Readable source ↘Record JSON ↘Full area ↗Related KL-FCS-034 ↘Related KL-FCS-035 ↘

Go further.

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

Questions to investigate

  1. Two chosen reduction strategies agreeing does not establish that all strategies agree.
  2. Which assumption in the specification can be changed to make the current evidence insufficient?
  3. Publish a general inversion-measure termination argument and a separately checked confluence proof.

Conceptual references

These sources explain the surrounding theory. The linked material was not imported as a dataset, and these records do not claim checking by the source’s software.

Primary conceptual reference ↗

Related areas

AutomataProgramming-language semanticsType systemsSAT / SMTFormal languages