Rules, derivations, and untyped operational semantics

Finitary rule schemes over arbitrary judgment forms, finite derivation trees, least closed sets, and hypothetical derivability. The concrete programming signature is the untyped call-by-value lambda calculus with booleans, numerals, conditionals, successor, and addition, together with small-step, evaluation-context, many-step, and big-step relations. It has no typing judgment, recursion operator, store, or error term.

The least closed set agrees with finite derivability. Rule induction and its strengthened form, the structural properties of hypothetical derivability, and the equivalence between admissibility and conservative rule extension are proved in chapter 1. Arithmetic small-step evaluation and untyped call-by-value evaluation are deterministic. The untyped language has unique evaluation-context decomposition; fresh renaming and term substitution preserve its evaluation derivations; and its big-step evaluation is simulated by many small steps.

Normalization would require every reduction sequence to terminate, but the untyped language contains a divergent closed term. Progress would require every closed term to be a value or take a step, but the language contains a stuck closed term. The chapter’s proof enumeration is only a semidecision procedure for an effective rule set.

None is used for these metatheorems.