Computer Laboratory, University of Cambridge, Cambridge, UK.
Equational reasoning is fundamental in automated theorem proving (that is, the proving of mathematical theorems by a computer program), and rewriting is a powerful method for equational reasoning. Category theory is a mathematical theory that deals in an abstract way with mathematical structures and relationships between them.
Using category theory, we have developed a framework for equational reasoning. A Term Equational System (TES) is given by a semantic universe and an abstract notion of syntax; and given this, we automatically derive a sound logical deduction system, called Term Equational Logic (TEL). Furthermore, we provide an algebraic free construction for the system, which may be used to synthesize a sound and complete rewriting system for it.
Existing systems arising in this framework include:
- first-order equational logic and rewriting system;
- combinatory reduction system of Klop;
- binding equational logic and rewriting system of Hamana; and
- nominal equational logics independently developed by Gabbay and Matheijssen, and Clouston and Pitts.
Especially, following the above scenario in our framework, we have newly developed a sound and complete rewriting system for nominal equational logic.
In this talk, rather than going into the technical details, I will focus on explaining basic ideas of category theory and how it can be used in practice.
This is joint work with Marcelo Fiore.