patternMinor
Unrolling multi-variable mu (μ) expressions in type theory
Viewed 0 times
multitheoryunrollingexpressionstypevariable
Problem
Unrolling an iso-recursive μ-type expression such as, say, one isomorphic to natural numbers:
using
by three steps, for example, gives:
If I instead have a polymorphic list, such as:
is there a necessary relative order to the expansion of λ and μ? Say I instantiate α to T:
Can we instead unroll μ before applying the λ at an arbitrary step?
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:
I could start with a few unrolls with β:
...starting with α instead looks more complicated:
...or maybe α-β alternation could work, say starting with β:
...or starting with α:
Where does it all end? I can't imagine they end up equivalent. Is there a standard approach?
μα.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+αβI could start with a few unrolls with β:
μα.μβ.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?
Solution
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.
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.
Context
StackExchange Computer Science Q#26031, answer score: 5
Revisions (0)
No revisions yet.