Untyping Typed Algebras and Colouring Cyclic Linear Logic

摘要

We prove "untyping" theorems: in some typed theories (semirings, Kleenealgebras, residuated lattices, involutive residuated lattices), typed equationscan be derived from the underlying untyped equations. As a consequence, thecorresponding untyped decision procedures can be extended for free to the typedsettings. Some of these theorems are obtained via a detour through fragments ofcyclic linear logic, and give rise to a substantial optimisation of standardproof search algorithms.