# 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. – Pseudonym Jun 12 '14 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. – user2023370 May 29 '14 at 20:20
• By the way, are there any programs which can help a learner explore terms like these? – user2023370 May 29 '14 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 '14 at 21:09
• The mode system of Mercury is also based on this formalism, sort of. – Pseudonym Jun 12 '14 at 0:03