Scope of mu (μ) bindings in type theory

Scoping of μ works no different from other binders, so yes, all your examples are valid. They are also regular, because they do not even contain a λ. (*)

As for equality, that depends on what sort of μ-types you have. There are basically two different notions:

• equi-recursive: in that case, the typing rules assume an equivalence

  μα.T = T[μα.T / α]

  i.e., a recursive type is considered equal to its one-level 'unrolling', where the μ is removed and the μ-bound variable is replaced by the type itself (and because this rule can be applied repeatedly, one can unroll arbitrary many times).

• iso-recursive: here, no such equivalence exists. Instead, a μ-type is a separate form of type with its own expression forms to introduce and eliminate it -- they are usually called roll and unroll (or fold and unfold), and are typed as follows:

  roll : T[μα.T / α] → μα.T

  unroll : μα.T → T[μα.T / α]

  These must be applied explicitly on the term level to mirror the equation above (once for each level of unrolling).

Functional languages like ML or Haskell usually use the latter for their interpretation of datatypes. However, the roll/unroll is built into the use of the data constructors. So each constructor is an injection into an iso-recursive type composed with an injection into a sum type (and inversely when matched).

Your examples are all different under the iso-recursive interpretation. The first and the third are the same under an equi-recursive interpretation, because the outer μ just disappears when you apply the above equivalence.

(*) Edit: An irregular recursive type is one whose infinite expansion does not correspond to a regular tree (or equivalently, can not be represented by a finite cyclic graph). Such a case can only be expressed with recursive type constructors, i.e., a λ that occurs under a μ. For example, μα.λβ.1+α(β×β) -- corresponding to the recursive equation t(β) = 1+t(β×β) -- would be irregular, because the recursive type constructor α is recursively applied to a type "larger" than its argument, and hence every application is a recursive type that "grows" indefinitely (and consequently, you cannot draw it as a graph).

It's worth noting, however, that in most type theories with μ, its bound variable is restricted to ground kind, so cannot express irregular types at all. In particular, a theory with unrestricted equi-recursive type constructors would have non-terminating type normalisation, so type equivalence (and thus type checking) would be undecidable. For iso-recursive types you'd need higher-order roll/unroll, which is possible, but I'm not aware of much literature investigating it.

Your μ type expressions are valid. I believe your types are regular as well since you only use recursion, sum, and products.

The type

T1 = μγ.1+(μβ.1+γβ)γ

does not look equal to

T2 = μβ.μγ.1+(1+γβ)γ

since inr (inr (inl *, inr (inl *)), inl *) has the second type but not the first.

The last type

T3 = μβ.μγ.1+(μβ.1+γβ)γ

is equal to (α-converting the first β)

μ_.μγ.1+(μβ.1+γβ)γ

which is, unfolding the top-level μ,

μγ.1+(μβ.1+γβ)γ

which is T1.

Basically, the scope of μ-bound variables follows the same rules of λ-bound variables. That is, the value of each occurrence of a variable β is provided by the closest μβ on top of it.