Untyping Typed Algebras and Colouring Cyclic Linear Logic

TL;DR

This paper demonstrates that in certain typed algebraic theories, typed equations can be derived from untyped equations, enabling the extension of untyped decision procedures to typed contexts and improving proof search algorithms.

Contribution

It introduces untyping theorems for various algebraic structures and connects them to cyclic linear logic to optimize proof search processes.

Findings

Typed equations derive from untyped equations in specific algebraic theories.

Untyped decision procedures extend to typed settings without additional complexity.

Proof search algorithms are significantly optimized through these untyping theorems.

Abstract

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