Many semantic aspects of a formal language can be defined as structural predicates on its abstract syntax, and much of its metatheory can be understood through the 'logical' properties of these predicates. Typical examples include results such as congruence of bisimilarity, type safety, confluence of evaluation, and termination of reduction. While several general theories have been proposed to study some of these properties — notable examples include mathematical operational semantics and categorical rewriting — a theory accounting for all of them, uniformly and abstractly, independently of specific languages and syntactic structures, is still missing.

In a recent line of research, I have proposed to develop such a theory in the form of an algebra of structural predicates, extending traditional logical algebras with operations akin to the structural definitions of predicates, such as structural recursion and substitution. This talk gives an introduction to such algebras in their relational form — Term Relation Algebras (TRAs) — and to their applications to the metatheory of programming languages and formal systems.

The first part of the talk introduces TRAs from an 'algebraic logic' perspective. TRAs arise as algebras of relations on term structures, internalizing such structure through logical operations on relations. Remarkably, not only is this 'logical internalization' possible on virtually all term structures — first- and second-order terms, nominal terms, string diagrams, and so on — but it yields, in all these cases, essentially the same algebras. TRAs axiomatize these algebras abstractly, with no reference to any underlying term structure.

The second part shifts to applications of TRAs to language metatheory, showing how many of the semantic notions and properties mentioned above can be studied algebraically within TRAs. The payoff of the algebraization is generality and unification: on the one hand, metatheorems that are otherwise reproved system by system are proved once and for all as algebraic properties (mostly quasi-equations) in the framework of TRAs; on the other hand, the algebraic lens reveals how conceptually different metatheorems, such as confluence of reduction and congruence of bisimilarity, are actually deeply related. 

Time permitting, the last part of the talk is devoted to some informal comparisons between TRAs and 'proof-theoretic' approaches to language metatheory.