Mechanizing Term Relation Algebras: The Basic Theory

The metatheory of operational semantics, type theories, rewriting systems, and similar formal systems is typically developed syntactically, forcing similar results to be reproved for every new language or syntactic structure. Term Relation Algebras (TRAs) have been recently introduced as an extension of relation algebras with operators accounting for relations defined structurally on syntax, through structural recursion, substitution, and pattern-matching. Despite their simplicity, TRAs can faithfully account for notions such as parallel reduction, big-step evaluation, and applicative bisimilarity, as well as express their metatheoretical properties, which are then proved by purely algebraic means, with no reference to any underlying term structure. This thesis develops a formalization of the basic theory of TRAs in the Lean 4 proof assistant. We mechanize the TRAs as allegories (positive relation algebras) extended with suitable operators: Howe extension, relation substitution, cohesive modalities of open and closed terms, and operational decompositions. On this basis, we explore the formalization of core semantic notions and their properties within TRAs, thereby testing the effectiveness of TRAs in formal system metatheory within a mechanized setting.