Weak mu-equality is decidable

TL;DR

This paper proves that weak mu-equality, an extension of simple types with recursive mu operators, is decidable by establishing a derivation system with bounded derivation trees.

Contribution

It introduces a decidability proof for weak mu-equality of mu-types using a new derivation system based on standard mu-type reduction.

Findings

Decidability of weak mu-equality for mu-types and alpha-equivalence classes.

Bounded derivation trees for mu-type equalities.

Elementary proofs for the decidability result.

Abstract

In this paper we consider the set of mu-types, an extension of the set of simple types freely generated from a set of atomic types and the type constructor ->, by a new operator mu, to explicitly denote solutions of recursive equations like A = A -> beta. We show that this so-called weak mu-equality for mu-types is decidable by defining a derivation system for weak mu-equality based on standard reduction for mu-types such that the number of nodes in a derivation tree for A = B is bounded as a function of A, B. We give two proofs. One for decidability of = for alpha-equivalence classes of mu-types and one for = for mu-types theselves. Both proofs are straightforward and elementary.