Structural Induction in Programming Language Semantics A Note for C S 386L Students
John A. Thywissen · 2015
Programming language syntax and semantics use various structured objects. Languages and derivations (proofs) are two examples. Often, one wishes to prove that a property holds for some set of these structured objects. Typically these objects are defined recursively, so induction is a natural proof approach. Structural induction is one pattern of inductive proof. In this note, we will (1) define this kind of structured object, then (2) present general induction axiom schemes, then (3) specialize them to induction on languages and derivations, and finally (4) discuss their application in operational semantics. 1. Definitions: Structures, Atoms, Components, and Constituents