# Programming-language semantics

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.

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

## Complexity

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

## Common failure

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

## Extensions

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

## Instances

- KL-FCS-003: Replay an arithmetic reduction — Normal form: 10
- KL-FCS-016: Evaluation order in a nested product — Normal form: 21
- KL-FCS-017: Signed integer reduction — Normal form: 14

## References

- https://softwarefoundations.cis.upenn.edu/plf-current/Smallstep.html