# Unrolling multi-variable mu (μ) expressions in type theory

Unrolling an iso-recursive μ-type expression such as, say, one isomorphic to natural numbers:

μα.1+α


using

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


by three steps, for example, gives:

μα.1+α
μα.1+(1+α)
μα.1+(1+(1+α))
...


If I instead have a polymorphic list, such as:

λα.μβ.1+αβ


is there a necessary relative order to the expansion of λ and μ? Say I instantiate α to T:

μβ.1+Tβ
μβ.1+T(1+Tβ)
μβ.1+T(1+T(1+Tβ))
...


Can we instead unroll μ before applying the λ at an arbitrary step?

λα.μβ.1+αβ
λα.μβ.1+α(1+αβ)
λα.μβ.1+α(1+α(1+αβ))
...


It looks in this case like we could. What I'd really like to know though is how to expand an expression having more than one μ variable; say:

μα.μβ.1+αβ


μα.μβ.1+αβ
μα.μβ.1+α(1+αβ)
μα.μβ.1+α(1+α(1+αβ))
...


...starting with α instead looks more complicated:

μα.μβ.1+αβ
μα.μβ.1+(μβ.1+αβ)β
μα.μβ.1+(μβ.1+(μβ.1+αβ)β)β
...


...or maybe α-β alternation could work, say starting with β:

μα.μβ.1+αβ
μα.μβ.1+α(1+αβ)
μα.μβ.1+(μβ.1+αβ)(1+(μβ.1+αβ)β)
...


...or starting with α:

μα.μβ.1+αβ
μα.μβ.1+(μβ.1+αβ)β
μα.μβ.1+(μ(1+αβ).1+α(1+αβ))(1+αβ)
...


Where does it all end? I can't imagine they end up equivalent. Is there a standard approach?

• Apart from the mistakes in the question which were cleared up below, you might want to look at regular tree grammars, and in particular, the regular tree unification algorithm. This is the typical method by which it can be decided if two regular trees are equal or not. Jun 12, 2014 at 0:02

I can't image they end up equivalent.

That's where you're wrong! In fact, starting with two different unfoldings of some expression you can always keep unfolding them in such a way that they "meet" again.

This property is formally called confluence.

More formally: define

$$T \rightarrow_\tau T'$$

If $T'$ is the result of a repeated number of unfoldings of $T$. We have the following Theorem:

Suppose $$T_1\ {}_\tau\!\leftarrow T\rightarrow_\tau T_2$$

There exists $T_3$ such that $$T_1\rightarrow_\tau T_3\ {}_\tau\!\leftarrow T_2$$

The proof is a bit subtle. I'll just try and convince you using your own example: $$T = \mu\alpha\beta. 1 + \alpha\times\beta$$

The reductions you outlined contain a slight mistake, the correct "$\alpha$-reduction" is:

$$T\rightarrow_\tau \mu\beta.1 + T\times \beta\qquad (1)$$

and not $T\rightarrow_\tau \mu\alpha\beta.1 + (\mu\beta.1+\alpha\times\beta)\times\beta$ As you suggest.

The $\beta$-unfolding is:

$$T\rightarrow_\tau \mu\alpha.1+\alpha\times(\mu\beta.1+\alpha\times\beta)\qquad (2)$$

Let's show both of these lead to the same term. Take $U(\alpha)=\mu\beta.1+\alpha\times\beta$. We have $$T\rightarrow_\tau \mu\alpha.1+\alpha\times U(\alpha)$$ By the above reduction. Set $T_1=\mu\alpha.1 +\alpha\times U(\alpha)$. On the other hand $$T\rightarrow_\tau 1+ T\times U(T)\qquad (3)$$

by composing (1) with a $\beta$-unfolding. Composing the second reduction with an $\alpha$-reduction gives $$1 + T_1\times U(T_1)$$

But since $T\rightarrow_\tau T_1$, we can replace $T$ by $T_1$ in (3) to get identical terms.

• Aha! I guess even my first reduction example was also mistaken. Perhaps it should have been: μα.1+α -> 1+(μα.1+α) -> 1+(1+(μα.1+α))? Thankyou for a very helpful answer. May 29, 2014 at 20:20
• By the way, are there any programs which can help a learner explore terms like these? May 29, 2014 at 20:25
• Yes, your first example was mistaken, and the version above is correct. I'm afraid I don't know much about exploring such terms, but you might want to try an equational logic programing environment like Maude or maybe $\lambda$-prolog...
– cody
May 29, 2014 at 21:09
• The mode system of Mercury is also based on this formalism, sort of. Jun 12, 2014 at 0:03