Title: 

Categorical equational systems

Abstract:

We introduce two abstract notions of system of equations, called
Equational System and Term Equational System.

Equational Systems provide a very abstract notion of equation, which
is general enough to represent non-classical notions of equations as
needed in modern applications such as nominal algebras and pi-calculus
algebras.  For Equational Systems we present an explicit construction
of free algebras under reasonably general conditions.

Term Equational Systems (TESs) are given by a more concrete, yet still
abstract notion of equation.  For TESs, we provide two means of
equational reasoning: reasoning by deduction and reasoning by
rewriting.  For the reasoning by deduction, a set of sound deduction
rules is given, but we do not have a general completeness result for
it.  However, we have an internal completeness result for TESs that
admit free algebras.  Together with this result, by analyzing the
explicit construction of free algebras given by the theory of
Equational Systems, one may synthesize a sound and complete equational
reasoning by rewritng.

Existing systems that arise as TESs include:

 - First-order equational logic and rewriting system;
 - Nominal equational logics independently developed
   by Gabbay and Mathijssen, and Clouston and Pitts;
 - Binding equational logic and rewriting system of Hamana;
 - Combinatory reduction systems of Klop;
 - Second-order abstract syntax of Marcelo Fiore. 

This is joint work with Marcelo Fiore.