Formal Computer Science / Languages & logic

Kenton Labs / Languages & logic

Programming-language semantics

Turn an expression’s meaning into an inspectable sequence of rule applications. Evaluation order belongs to the specification.

The vocabulary.

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

Term
An integer literal or an add/mul syntax node.
Small step
One permitted local reduction, under an explicitly chosen evaluation context.
Normal form
A term with no further reduction; here it is an integer literal.

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. Check that the trace begins with the declared syntax tree.
  2. Reduce the left non-literal operand before the right operand.
  3. Apply arithmetic only when both operands are integer literals.
  4. Check each adjacent trace pair and require a terminal integer.

Cost and scope

Replay costs one reduction per arithmetic node, plus traversal to find the next reducible node.

A common failure

A final number alone does not certify the declared evaluation sequence.

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-003
Programming-language semanticsReplay an arithmetic reductionExact reduction replay · 2 steps

The problem

Evaluate (2 × 3) + 4 using left-to-right small-step reduction on integer literals, addition, and multiplication.

The checked result

Normal form: 10.

Every adjacent term must follow the declared reduction rule. The final term is the literal 10 and cannot reduce further.

Why the checker accepts it

  1. Check that the trace begins with the declared syntax tree.
  2. Reduce the left non-literal operand before the right operand.
  3. Apply arithmetic only when both operands are integer literals.
  4. Check each adjacent trace pair and require a terminal integer.

Formal specification

{
  "term": [
    "add",
    [
      "mul",
      2,
      3
    ],
    4
  ],
  "rules": "Reduce the left non-literal operand first, then the right; combine two integer literals."
}

Claim and evidence

{
  "claim": {
    "normal_form": 10
  },
  "witness": {
    "trace": [
      [
        "add",
        [
          "mul",
          2,
          3
        ],
        4
      ],
      [
        "add",
        6,
        4
      ],
      10
    ]
  }
}

Dataset construction

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

Complexity and limits

Replay costs one reduction per arithmetic node, plus traversal to find the next reducible node.

One ground term in a deliberately small language; no general termination or confluence theorem.

A boundary to investigate

A final number alone does not certify the declared evaluation sequence. Introduce variables, environments, conditionals, and explicit stuck-state outcomes.

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-016 ↘Related KL-FCS-017 ↘
KL-FCS-016
Programming-language semanticsEvaluation order in a nested productExact reduction replay · 3 steps

The problem

Replay left-to-right integer arithmetic with add and mul nodes.

The checked result

Normal form: 21.

The trace records intermediate terms, so the result’s derivation and the evaluation order are both inspectable.

Why the checker accepts it

  1. Check that the trace begins with the declared syntax tree.
  2. Reduce the left non-literal operand before the right operand.
  3. Apply arithmetic only when both operands are integer literals.
  4. Check each adjacent trace pair and require a terminal integer.

Formal specification

{
  "term": [
    "mul",
    [
      "add",
      1,
      2
    ],
    [
      "add",
      3,
      4
    ]
  ],
  "rules": "Left non-literal operand first, then right; integer arithmetic without overflow."
}

Claim and evidence

{
  "claim": {
    "normal_form": 21
  },
  "witness": {
    "trace": [
      [
        "mul",
        [
          "add",
          1,
          2
        ],
        [
          "add",
          3,
          4
        ]
      ],
      [
        "mul",
        3,
        [
          "add",
          3,
          4
        ]
      ],
      [
        "mul",
        3,
        7
      ],
      21
    ]
  }
}

Dataset construction

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

Complexity and limits

Replay costs one reduction per arithmetic node, plus traversal to find the next reducible node.

This language uses mathematical integers and no side effects; machine overflow requires different semantics.

A boundary to investigate

A final number alone does not certify the declared evaluation sequence. Introduce variables, environments, conditionals, and explicit stuck-state outcomes.

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-003 ↘Related KL-FCS-017 ↘
KL-FCS-017
Programming-language semanticsSigned integer reductionExact reduction replay · 3 steps

The problem

Replay left-to-right integer arithmetic with add and mul nodes.

The checked result

Normal form: 14.

The trace records intermediate terms, so the result’s derivation and the evaluation order are both inspectable.

Why the checker accepts it

  1. Check that the trace begins with the declared syntax tree.
  2. Reduce the left non-literal operand before the right operand.
  3. Apply arithmetic only when both operands are integer literals.
  4. Check each adjacent trace pair and require a terminal integer.

Formal specification

{
  "term": [
    "add",
    [
      "mul",
      -2,
      3
    ],
    [
      "mul",
      4,
      5
    ]
  ],
  "rules": "Left non-literal operand first, then right; integer arithmetic without overflow."
}

Claim and evidence

{
  "claim": {
    "normal_form": 14
  },
  "witness": {
    "trace": [
      [
        "add",
        [
          "mul",
          -2,
          3
        ],
        [
          "mul",
          4,
          5
        ]
      ],
      [
        "add",
        -6,
        [
          "mul",
          4,
          5
        ]
      ],
      [
        "add",
        -6,
        20
      ],
      14
    ]
  }
}

Dataset construction

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

Complexity and limits

Replay costs one reduction per arithmetic node, plus traversal to find the next reducible node.

This language uses mathematical integers and no side effects; machine overflow requires different semantics.

A boundary to investigate

A final number alone does not certify the declared evaluation sequence. Introduce variables, environments, conditionals, and explicit stuck-state outcomes.

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-003 ↘Related KL-FCS-016 ↘

Go further.

Introduce variables, environments, conditionals, and explicit stuck-state outcomes.

Questions to investigate

  1. A final number alone does not certify the declared evaluation sequence.
  2. Which assumption in the specification can be changed to make the current evidence insufficient?
  3. Introduce variables, environments, conditionals, and explicit stuck-state outcomes.

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

AutomataType systemsSAT / SMTFormal languagesTerm rewriting