# Replay an arithmetic reduction

KL-FCS-003 · Programming-language semantics · version 1.0.0

## Problem

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

## Context

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

## Definitions

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

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

## Checker reasoning

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.

## Dataset construction

{
  "family": "semantics",
  "task": "Evaluate (2 × 3) + 4 using left-to-right small-step reduction on integer literals, addition, and multiplication.",
  "input_encoding": "Structured JSON; field meanings are stated in the specification.",
  "coverage": "Exact reduction replay · 2 steps",
  "acceptance": [
    "Check that the trace begins with the declared syntax tree.",
    "Reduce the left non-literal operand before the right operand.",
    "Apply arithmetic only when both operands are integer literals.",
    "Check each adjacent trace pair and require a terminal integer."
  ],
  "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": {
    "term": [
      "add",
      [
        "mul",
        2,
        3
      ],
      4
    ],
    "rules": "Reduce the left non-literal operand first, then the right; combine two integer literals."
  },
  "claim": {
    "normal_form": 10
  },
  "witness": {
    "trace": [
      [
        "add",
        [
          "mul",
          2,
          3
        ],
        4
      ],
      [
        "add",
        6,
        4
      ],
      10
    ]
  }
}
```

## Complexity

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

## Limits

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

## Common error and further work

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

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

## Verification

Exact reduction replay · 2 steps. 2 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://softwarefoundations.cis.upenn.edu/plf-current/Smallstep.html)