An Algebraic Approach to Formal System Metatheory

We introduce an algebraic approach to the metatheory of formal systems of term assertions akin to those of structural and natural operational semantics, type theories, rewriting systems, and equational theories. We rest on Term Relation Algebras, viz. pointfree algebras of structurally-defined predicates on terms, to give a common algebraic semantics to different kinds of formal systems, regardless of their inferential mechanisms and underlying term structures. This enables abstract reasoning about formal systems, and their metatheory, through the algebra of the term predicates they define. We give a faithfully term-free algebraization of semantically-relevant term predicates, such as parallel reduction, big-step evaluation, and applicative bisimilarity. We extend this algebraization also to fundamental metatheoretical properties of these notions - including congruence of applicative bisimilarity, determinacy of evaluation, and confluence of reduction - and prove these properties using algebraic methods.