WEAK µ-EQUALITY IS DECIDABLE

arXiv:1102.0155v1 [cs.LO] 1 Feb 2011

WIL DEKKERS, RADBOUD UNIVERSITY, NIJMEGEN, THE NETHERLANDS

Abstract
In this paper we consider the set TTµ of µ-types, an extension of the set TT
of simple types freely generated from a set A of atomic types and the type
constructor → , by a new operator µ, to explicitly denote solutions of recursive
equations like A =µ A → β. We show that this so-called weak µ-equality for
µ-types is decidable by defining a derivation system for weak µ-equality based
on standard reduction for µ-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 α-equivalence classes of µ-types and one for
decidability of =µ/α for µ-types themselves. Both proofs are straightfroward
and elementary.
Introduction
In Cardone and Coppo[1] a proof method is given to show decidability of weak
µ-equality, using standard reduction and a special purpose proof system. It
turned out recently that their treatment of α-conversion was not completely
correct. Nethertheless their result is correct and in Endrullis, Grabmayer,
Klop and van Oostrom[2] three proofs for the decidability are given. Two of
the given proofs are inspired by the Cardone-Coppo proof strategy. The third
proof uses the theory of regular languages and is totally different. This paper
is based on the first two proofs of Endrullis et al. These proofs are ingenuous
but they are also technical and intricate. Our aim is to give simpler and more
straightforward proofs.
In their first proof Endrullis et al. work with µ-types themselves, not with
α-equivalence classes of µ-types. The proof constructs a decision procedure
for equality of types based on standard reduction for types. In that proof they
need the theory of α-avoiding developed by van Oostrom[3]. In the second
proof they work with α-equivalence classes and the corresponding reduction
relation →µ for classes and they show the decidability of =µ . Our proof is
more or less the other way round. Based on the first proof of Endrullis et
al. of decidabiliy of equality for types we give a proof of decidability of =µ
for classes of types and then from that proof we derive a first order proof of
decidability of equality for types where the theory of α-avoiding is not needed.
Both proofs are straightforward and elementary.
So in our first proof TTµ is he set of α-equivalence classes of types and A, B
stand for classes of types. We start by defining a set TTµ′ , containing TTµ , of
so-called annotated ( classes of ) µ-types and a reduction →µ′ : TTµ′ → TTµ′ that
is closely related with standard reduction on TTµ . Then we define a derivation
1

2

WIL DEKKERS, RADBOUD UNIVERSITY, NIJMEGEN, THE NETHERLANDS

system ⊢µ′ for equality of elements of TTµ′ such that for A, B ∈ TTµ one has
⊢µ′ A = B ⇔ A and B have a common standard reduct.
We show for a ∈ TTµ′ that SC(a) ≡ {b ∈ TTµ′ |a →∗µ′ b} is bounded as a function
in a and also that for a = b occurring in a derivation tree for ⊢µ′ A = B we have
a ∈ SC(A) and b ∈ SC(B). So the number of nodes occurring in a derivation
tree for ⊢µ′ A = B is bounded as a function in A, B. So ⊢µ′ A = B is decidable
and hence A =µ B is decidable, because of the fact that
A =µ B ⇔ A and B have a common standard reduct.
Then in part 2 from this result we derive easily that =µ/α on types themselves
can be decided by first order means via a decision procedure for =µ/α on types.

1. A decision procedure for weak µ-equality via α-equivalence classes
of types
1.1. Definition (Of TTµ and →µ ). (i) Let A = A∞ be an infinite set of type atoms
α, β, γ · · · considered as type variables for the purpose of binding and substitution.The
set of µ-types, notation TTµ , is defined as follows. TTµ = α | A1 → A2 | µα.A1 .
(ii) On TTµ we define the notion of α-reduction and α-conversion via the contraction
rule
µα.A 7→α µα′ .A[α := α′ ], provided α′ ∈
/ FV(A).
The relation →α is the least compatible relation containing 7→α and =α is the least
congruence containing 7→α .
(iii) Define on TTµ a notion of µ-reduction via the contraction rule 7→µ
µβ.A1 7→µ A1 [β := µβ.A1 ]
The relation →µ ⊆ TTµ × TTµ is the compatible closure of 7→µ . That is
A1 →µ B1 ⇒ µβ.A1 →µ µβ.B1 ;
A1 →µ A′1 ⇒ (A1 → A2 ) →µ (A′1 → A2 );
A2 →µ A′2 ⇒ (A1 → A2 ) →µ (A1 → A′2 ).
(iv) →∗µ denotes zero or more →µ steps and =µ is the least congruence containing
7→µ .
(v) In this first part we work with α-equivalence classes of types and we asume that
all bound and free variables are different. Especially in µα1 ...µαn .A all αi are different.
1.2. Definition. Let [A] denote the α-equivalence class of A and let TT[µ] denote the set
of α-equivalence classes. →µ and =µ can easily be lifted to relations →[µ] and =[µ] on
TT[µ] . In part 2 of this paper we will consider TTµ , →µ and =µ but in this part 1 we
work with TT[µ] , →[µ] and =[µ] and we simply write TTµ , →µ and =µ . Also we write
A for [A].
1.3. Definition. [Of standard reduction →∗st ]
(a) A →∗st A
(b) If A1 [β := µβ.A1 ] →∗st B, then the composition µβ.A1 → A1 [β := µβ.A1 ] →∗st B is a
standard reduction.

WEAK µ-EQUALITY IS DECIDABLE

3

(c) If A1 →∗st B1 , then the induced reduction µβ.A1 →∗st µβ.B1 is a standard reduction.
(d) If A1 →∗st A′1 and A2 →∗st A′2 , then each reduction (A1 → A2 ) →∗µ (A′1 → A′2 )
generated by interleaving is a standard reduction.
1.4. Example. (i) Let A ≡ µαµβ.α. Then A →µ µβ1 .A →µ µβ1 µβ2 .A →µ · · · is a
standard reduction.
(ii) Let B ≡ µα.α → α. Then B →µ (B → B) →µ (B → B) → B →µ · · · is a standard
reduction.
(iii) Let C ≡ µαµβµγ.α. Then C →µ µαµγ.α →µ µγ1 (µαµγ.α) is not a standard
reduction.
1.5. Remark. We have the well known facts.
(i) The relation →µ is Church Rosser (CR);
(ii) If A →∗µ B then there is a standard reduction A →∗st B.
We illustrate (ii) in the above remark by an example.
1.6. Example. Let A = µαµβ.C[α, β]. Here C[., .] is a so-called context. The variables
α and β can occur several times in it. Now let B = µα.C[α, µβ.C]. Then
A →µ B = µα.C[α, µβ.C[α, β]] →µ C[B, µβ.C[B, β]].
We can make this two-step reduction into a standard reduction as follows.
A →µ µβ.C[A, β] →µ C[A, µβ.C[A, β]]
and now reduce each occurrence of A to B, from left to right.
Let for the moment A ↓ B denote that A and B have a common standard reduct. Our
aim is to show that A =µ B is decidable. By (ii) of the above remark we are ready if we
show that A ↓ B is decidable. However a direct proof of that is not so easy because in
general a type A may have infinitely many standard reducts as is shown by (i) and (ii)
of Example 1.4.
We remedy the two problems given by the example by changing the notion of standard
reduction (and also the set of types) roughly as follows. In clause (c) of the notion of
standard reduction we add the condition β ∈ F V (A1 ). Then the number of µβi as in (i) of
the example is bounded . Moreover clause (d) is changed into (A1 → A2 ) → Ai i = 1, 2
to remedy the problem shown in (ii).
This is formalised as follows.
1.7. Definition (Of the set of annotated types TTµ′ ). (i) The set of annotated types TTµ′
is defined by TTµ′ ≡ {(µα1 ).....(µαn )A | A ∈ TTµ , αi ∈ F V (A), αi 6= αj if i 6= j},
(ii) We consider the annotated types modulo α-equivalence as follows
/ FV(A) ∪ BV(A)). And implicitly
(µα1 ).....(µαn )A ≡ (µα′1 ).....(µα′n )A[αi := α′i ] (α′i ∈
′
′
αi 6= αj if i 6= j},
1.8. Remark. (i) In Endrullis et al.[2] a set AnnTer(µ) is defined by AnnTer(µ) =
{(µα1 ).....(µαn )A | A ∈ TTµ }. So they don’t have the conditions αi ∈ F V (A) and αi 6= αj
if i 6= j. Moreover they don’t work modulo α-conversion.
(ii) The intuition for (µα1 ).....(µαn )A is that it stands for µα1 .....µαn .A ∈ TTµ where
the µαi at the root are frozen. This will become clear in Definition 1.10.
(iii) Note that TTµ ⊂ TTµ′ .

4

WIL DEKKERS, RADBOUD UNIVERSITY, NIJMEGEN, THE NETHERLANDS

1.9. Notation. (i) We denote (µα1 ).....(µαn )A simply as (µα1 ...αn )A and mostly we
write (µ~
α)A.
(ii) a, b, c....denote elements of TTµ′ and as before A, B, C.... stand for elements of TTµ .
(iii) If α
~ is a sequence of (different) type variables then α
~ ↾a denotes the sequence that
arises from α
~ by omitting the variables that do not occur freely in a. Similarly for α
~ ↾a∩b.
(µ~
α)✷A stands for (µ(~
α↾A))A.
α)✷S = {(µ~
α)✷a | a ∈ S}.
If S ⊆ TTµ′ then (µ~
(iv) If S ⊂ TTµ′ then |S| stands for the number of elements of S.
(v) {~
α} stands for the set of variables occurring in α
~ . When we write {α1 , ..., αn } we
always assume αi 6= αj for i 6= j.
1.10. Definition. (0f →µ′ : TTµ′ → TTµ′ and SC(a))
(i) The reduction relation →µ′ : TTµ′ → TTµ′ is defined as follows.
αβ)A1 if β ∈ F V ((A1 );
(µ~
α)µβ.A1 →µ′ (µ~
α)A1 [β := µβ.A1 ];
(µ~
α)µβ.A1 →µ′ (µ~
α)✷Ai i = 1, 2;
(µ~
α)(A1 → A2 ) →µ′ (µ~
(ii) SC(a) = {b ∈ TTµ′ | a →∗µ′ b}.
1.11. Remark. (i) Note that →µ′ is not compatible with µ or →. So for example we do
not have µαµβ.A1 →µ′ µα.A1 [β := µβ.A1 ].
(ii) Now the outline of the decidability proof is as follows.
–We define a derivation system ⊢µ′ a = b for types a, b ∈ TTµ′ , closely connected with the
reduction relation →µ′ and we show for A, B ∈ TTµ :
⊢µ′ A = B ⇔ A and B have a common standard reduct.
Hence we have A =µ B ⇔ ⊢µ′ A = B.
– We note that for all nodes c = d occurring in a derivation tree for ⊢µ′ a = b we have
c ∈ SC(a) and d ∈ SC(b.
– We show that |SC(a)| is bounded as a function in a. Hence the number of different
nodes in a derivation tree for ⊢µ′ a = b is bounded as a function in a, b.
– We conclude that ⊢µ′ a = b is decidable and hence so is A =µ B.
We start by defining the derivation system ⊢µ′ a = b for a, b ∈ TTµ′ . We give the
definition via representatives, types instead of α-equivalence classes of types, and we
show that it is invariant under α-conversion. Hence this defines in fact a relation on the
set of α-equivalence classes.

WEAK µ-EQUALITY IS DECIDABLE

5

1.12. Definition. (Of ⊢µ′ a = b for a, b ∈ TTµ′ )
(axiom)

a=b

if a =α b

(left µ-step)

~
(µ~
α)A1 [γ := µγ.A1 ] = (µβ)B
~
(µ~
α)µγ.A1 = (µβ)B

(right µ-step)

~ 1 [δ := µδ.B1 ]
(µ~
α)A = (µβ)B
~
(µ~
α)A = (µβ)µδ.B
1

(µ-freezing)

~
(µ~
αγ)A1 = (µβδ)B
1
~
(µ~
α)µγ.A1 = (µβ)µδ.B1

{~
α} ⊆ FV(A1 → A2 )
~ ⊆ FV(B1 → B2 )
(decomposition) {β}
(µα~1 )A1 = (µβ~1 )B1

α
~ ↾Ai = α~i = αi1 · · · αim
~ i = β~i = βi · · · βi
β↾B
m
1
(µα~2 )A2 = (µβ~2 )B2
~ 1 → B2
(µ~
α)A1 → A2 = (µβ)B

Note that in the above definition A, B stand for types, not α-equivalence classes of
types and =α on TTµ′ is given by
/ FV(A).
A =α A′ ⇒ (µα1 ).....(µαn )A′ =α (µα′1 ).....(µα′n )A′ [αi := α′i ] (α′i ∈
Note also that in the rule (µ-freezing) implicitly γ ∈ FV(A1 ), δ ∈ FV(B1 ) and in rule
(decomposition) {α~i } ⊆ FV(Ai ), {β~i } ⊆ FV(Bi ).
In a decision procedure of ⊢µ′ a = b in fact these rules are used upside down. That
explains the names of the rules.
1.13. Lemma. Let a =α a′ , b =α b′ . Then
⊢µ′ a = b ⇒ ⊢µ′ a′ = b′ .
Proof. By an easy induction on the definition of ⊢µ′ a = b.
So Definition 1.12 defines in fact a relation on the set of α-equivalence classes. We
denote that relation also by ⊢µ′ .
1.14. Lemma. (i) FV(µβ.A1 ) = FV(A1 [β := µβ.A1 ]) = FV((µβ)A1 ).
(ii) A →∗µ B ⇒ FV(A) = FV(B).
(iii) a →∗µ′ b ⇒ FV(b) ⊆ FV(a).
~
~
~
α)A = (µβ)B
⇒ |{~
α}| = |{β}|,
FV((µ~
α)A) = FV((µβ)B)
(iv) ⊢µ′ (µ~
For easier use in the following we rewrite Definition 1.12 for α-equivalence classes as
follows.

6

WIL DEKKERS, RADBOUD UNIVERSITY, NIJMEGEN, THE NETHERLANDS

1.15. Definition. (Of ⊢µ′ a = b for α-equivalence classes a, b.)
(axiom)

a=a

(left µ-step)

(µ~
α)A1 [β := µβ.A1 ] = (µ~
α)B
(µ~
α)µβ.A1 = (µ~
α)B

(right µ-step)

(µ~
α)A = (µ~
α)B1 [β := µβ.B1 ]
(µ~
α)A = (µ~
α)µβ.B1

(µ-freezing)

(µ~
αβ)A1 = (µ~
αβ)B1
(µ~
α)µβ.A1 = (µ~
α)µβ.B1

{~
α} ⊆ FV(A1 → A2 ) α
~ ↾A1 = α~1 , α
~ ↾A2 = α~2
(µα~1 )A1 = (µα~1 )B1 (µα~2 )A2 = (µα~2 )B2
(decomposition)
(µ~
α)A1 → A2 = (µ~
α)B1 → B2
The following is an example of a derivation of ⊢µ′ a = b. We reason backwards, so we
write down a = b and using the rules upside down we hope to finish with only axioms.
1.16. Example.
µαβγ.((µδ.α) → γ) =
⇓
(µα)µβγ.((µδ.α) → γ) =
⇓
(µα)µγ.((µδ.α) → γ) =
⇓
(µα)((µδ.α) → µγ.((µδ.α) → γ)) =
⇓
(µα)(µδ.α) = (µα)α
left µ−step ⇓
(µα)α = (µα)α

µαβ.(α → (µγ.α → γ))
µ−freezing
(µα)µβ.(α → (µγ.α → γ))
left and right µ−step
(µα)(α → (µγ.α → γ))
left µ−step
(µα)(α → (µγ.α → γ))
decomposition
(µα)µγ.((µδ.α) → γ) = (µα)(µγ.α → γ)
⇓ µ − freezing
(µαγ)((µδ.α) → γ) = (µαγ)(α → γ)
⇓ decomposition
(µα)µδ.α = (µα)α
(µγ)γ = (µγ)γ
⇓ left µ−step
(µα)α = (µα)α

1.17. Remark. Let A = µαβγ.((µδα) → γ) and B = µαβ.(α → (µγ.α → γ)). In the
example above we gave a proof of ⊢µ′ A = B. In fact one could try other proofs. For
example one could start with a left µ-step and a right µ-step. Then one encounters at
some stage again a node A = B. So one could go on for ever and the result would be an

WEAK µ-EQUALITY IS DECIDABLE

7

infinite tree. But of course one should stop developing the sub branch at that node.
In general if in a derivation of ⊢µ′ a = b we arrive at a node c = d that we encountered
already higher up in the branch from the root to that node then we stop at that node.
Further on we will show that the number of nodes in the resulting tree is bounded as a
function of a, b.
But first we will show in the next proposition that ⊢µ′ A = B iff A and B have a common
standard reduct.
1.18. Proposition. The following two assertions are equivalent
α)A = (µ~
α)B;
(i) ⊢µ′ (µ~
(ii) A and B have a common standard reduct.
α)A = (µ~
α)B.
Proof. (i)⇒(ii). By induction on the derivation of ⊢µ′ (µ~
(axiom)

(µ~
α)A = (µ~
α)A. This is clearly ok.

(left µ-step)

(µ~
α)A1 [β := µβ.A1 ] = (µ~
α)B
(µ~
α)µβ.A1 = (µ~
α)B

By the induction hypothsis A1 [β := µβ.A1 ] and B have a common standard reduct,
hence the same holds for µβ.A1 and B by (b) of Definition 1.3.
(right µ-step) Similarly.
(µ-freezing)

(µ~
αβ)A1 = (µ~
αβ)B1
(µ~
α)µβ.A1 = (µ~
α)µβ.B1

By the induction hypothesis A1 and B1 have a common standard reduct, hence the same
holds for µβ.A1 and µβ.B1 .
{~
α} ⊆ FV(A1 → A2 ) α
~ ↾A1 = α~1 , α
~ ↾A2 = α~2
(µα~1 )A1 = (µα~1 )B1 (µα~2 )A2 = (µα~2 )B2
(decomposition)
(µ~
α)A1 → A2 = (µ~
α)B1 → B2
By the induction hypothesis A1 and B1 have a common standard reduct and the same
holds for A2 and B2 . So it also holds for A1 → A2 and B1 → B2 .
(ii)⇒ (i). By induction on the definition of A →∗st C and B →∗st C in Definition 1.3.
Case (a) for both A and B.
α)A = (µ~
α)A by axiom.
Then B = A and we have ⊢µ′ (µ~
Case (b) for A (and similarly for B).
α)µβ.A1 = (µ~
α)B by (left
α)A1 [β := µβ.A1 ] = (µ~
α)B and we get ⊢µ′ (µ~
We have ⊢µ′ (µ~
µ-step).
Case (c) for A an for B.
Now A = µβ.A1 and B = µβ.B1 , A1 →∗st C1 ←∗st B1 and therefore
µβ.A1 →∗st µβ.C1 ←∗st µβ.B1 .

8

WIL DEKKERS, RADBOUD UNIVERSITY, NIJMEGEN, THE NETHERLANDS

Note that FV(A1 ) = FV(B1 ) by Lemma 1.14(ii) We distinguish two subcases
Subcase (c1 ) β ∈ FV(A1 ) ∩ FV(B1 ).
αβ)A1 = (µ~
αβ)B1 and hence by (µ-freezing)
By the induction hypothesis we have ⊢µ′ (µ~
α)µβ.A1 = (µ~
α)µβ.B1 .
⊢µ′ (µ~
Subcase (c2 ) β ∈
/ FV(A1 ), β ∈
/ FV(B1 ).
α)A1 = (µ~
α).B1 , hence we get by (left
Now we have by the induction hypothesis ⊢µ′ (µ~
α)µβ.A1 = (µ~
α)µβ.B1 .
µ-step) and (right µ-step) ⊢µ′ (µ~
Case (d) for A and for B. Now we have A1 →∗st C1 ←∗st B1 , A2 →∗st C2 ←∗st B2
and hence A = A1 → A2 →∗st C1 → C2 ←∗st B1 → B2 . Note that by Lemma 1.14(ii)
we have FV(Ai ) = FV(Bi ) and FV(A1 → A2 ) = FV(B1 → B2 ). Let {~
α} ⊆ FV(A1 →
~ ↾ Ai , i = 1, 2. Then
A2 ) so that (µ~
α)A1 → A2 , (µ~
α)B1 → B2 ∈ TTµ′ . Define α~i = α
(µα~i )Ai , (µα~i )Bi ∈ TTµ′ and by the induction hypothesis, two times, we have ⊢µ′ (µα~1 )A1 =
(µα~1 )B1 , ⊢µ′ (µα~2 )A2 = (µα~2 )B2 .
Now we have treated all cases. If we have Case (c) for A and Case (a) for B then in fact
we have Case (c) for both A and B. If we have Case (d) for A and Case (a) for B then
in fact we have Case (d) for both A and B. Finally Case (c) for A and Case (d) for B
(or vice versa) cannot occur at the same time.
Now we will finish the proof of decidability of =µ by showing that the number of
different nodes c = d occurring in a derivation tree of ⊢µ′ a = b is bounded as a function
in a, b.
Note that for all these nodes c = d we have c ∈ SC(a), d ∈ SC(b). (See Definition 1.10)
We start by showing that |SC(a)| is bounded as a function in a.
~
~
1.19. Lemma. (µ~
α)✷((µβ)✷a)
= (µ~
αβ)✷a.
Proof. Immediate. Note that by the variable convention α
~ and β~ have no variables in
common.
1.20. Lemma. SC(α) = {α};
SC(µβ.A1 ) = {µβ.A1 } ∪ (µβ)✷SC(A1 ) ∪ SC(A1 [β := µβ.A1 ]);
SC(A1 → A2 ) = {A1 → A2 } ∪ SC(A1 ) ∪ SC(A2 );
SC((µ~
α)A) = (µ~
α)✷SC(A).
Proof. By induction on the structure of a ∈ TTµ′ , using the preceding lemma. Note that
the second clause also holds for β ∈
/ FV(A1 ) because then (µβ)✷SC(A1 ) = SC(A1 ) =
SC(A1 [β := µβ.A1 ]) by Lemma 1.14(iii).
Now SC([A1 [β := µβ.A1 ]) could be intricate but we will show in Lemma 1.22 that we
have in fact SC(µβ.A1 ) ⊆ {µβ.A1 } ∪ (µβ)✷SC(A1 ) ∪ SC(A1 )[β := µβ.A1 ].
1.21. Lemma. If A[β := B] →∗µ′ b then we have either
(i) This reduction is A[β := B] →∗µ′ B →∗µ′ b
(ii) This reduction is a [β := B] instance of A →∗µ′ a (So b = a[β := B]).
Proof. By induction on the length of the reduction A[β := B] →∗µ′ b.
If the length is zero then we have (ii). Else we have A[β := B] →∗µ′ b′ →µ′ b. The
induction hypothesis for A[β := B] →∗µ′ b′ gives that we have either (i) or (ii) as follows

WEAK µ-EQUALITY IS DECIDABLE

9

(i) A[β := B] →∗µ′ B →∗µ′ b′ Then we have also case (i) for A[β := B] →∗µ′ b.
(ii) The reduction A[β := B] →∗µ′ b′ is a [β := B] instance of A →∗µ′ a′ . So b′ = a′ [β := B]
We distinguish subcases for a′ as follows.
(iia) a′ = β. Then we have Case (i) (for A[β := B] →∗µ′ b).
(iib) a′ = α 6= β or a′ = (µα).α. These cases cannot occur because then b′ = a′ is in nf.
(iic) a′ = (µ~
α)µγ.A′ with β ∈
/ {~
α, γ}.
In this case (µ~
α) at the root is very innocent. It is frozen and occurs in the same way
at the root in all types occurring in the proof in this part (iic). Therefore for simplicity
we assume {~
α} = ∅. Now b′ = µγ.A′ [β := B]. We distinguish two subcases.
(iic1) µγ.A′ [β := B] →µ′ (µγ).(A′ [β := B]) (∗)
Then γ ∈ FV(A′ [β := B]), hence also γ ∈ FV(A′ ), because γ ∈
/ FV(B) by the variable
′
′
convention. So (∗) is a [β := B] instance of µγ.A →µ (µγ).A′ . In total we have that
A[β := B] →∗µ′ B ′ →µ′ b is an instance of A →∗µ′ µγ.A′ →µ′ (µγ).A′ and we are in Case
(ii).
(iic2) b′ = µγ.A′ [β := B] →µ′ A′ [β := B][γ := µγ.A′ [β := B]] = b.
By the substitution lemma we get b′ = µγ.A′ [β := B] →µ′ A′ [γ := µγ.A′ ][β := B] = b.
Now we have that A[β := B] →∗µ′ a′ [β := B] →µ′ a[β := B] is an instance of A →∗µ′ a′ =
µγ.A′ →µ′ a = A′ [γ := µγ.A′ ] and we are in Case (ii).
α)✷(Ai [β :=
(iid) a′ = (µ~
α)(A1 → A2 ). Then b′ = (µ~
α)(A1 [β := B] → A2 [β := B]) →µ′ (µ~
′
′
α)✷Ai . Now we are in case (ii) again.
B]) = b and a →µ (µ~
1.22. Lemma. SC(µβ.A1 ) ⊆ {µβ.A1 } ∪ (µβ)✷SC(A1 ) ∪ SC(A1 )[β := µβ.A1 ].
Proof. Let µβ.A1 →∗µ′ b be a reduction path of minimal length.
If the length is zero then b = µβ.A1 . Now let the length be bigger then zero. We
distinguish two cases.
Case (i) µβ.A1 →µ′ (µβ).A1 →∗µ′ b
Now β ∈ FV(A1 ) and b ∈ SC((µβ).A1 ) = (µβ)✷SC(A1 ).
Case(ii) µβ.A1 →µ′ A1 [β := µβ.A1 ] →∗µ′ b.
We distinguish two subcases according to Lemma 1.21
(iia) µβ.A1 →µ′ A1 [β := µβ.A1 ] →∗µ′ µβ.A1 →∗µ′ b. This cannot occur because it is not a
reduction of minimal length.
(iib) A1 [β := µβ.A1 ] →∗µ′ b is a [β := µβ.A1 ] instance of A1 →∗µ′ a. Now a ∈ SC(A1 )
hence b = a[β := µβ.A1 ] ∈ SC(A1 )[β := µβ.A1 ].

10

WIL DEKKERS, RADBOUD UNIVERSITY, NIJMEGEN, THE NETHERLANDS

1.23. Definition.
l(α)
l(A1 → A2 )
l(µβ.A1 )
l((µ~
α).A)

=
=
=
=

1;
1 + l(A1 ) + l(A2 );
1 + l(A1 );
l(A).

1.24. Lemma. |SC((µ~
α)A)| = |SC(A)| ≤ 3l(A) .
Proof. By Lemmas 1.20 and 1.22.
1.25. Lemma. Let n = n((µ~
α)A = (µ~
α)B) be the number of different nodes in a complete
α)A = (µ~
α)B. Then
derivation treee for ⊢µ′ (µ~
l(A)+l(B) )

n ≤ 3(3

.

Proof. Easy. Note that each node in the derivation tree has at most three daughters.
α)A = (µ~
α)B is decidable.
1.26. Corollary. (i) ⊢µ′ (µ~
(ii) ⊢µ′ A = B is decidable.
1.27. Corollary. A =µ B is decidable.
Proof. By Remark 1.5 and Proposition 1.18.

2. A decision procedure of weak µ-equality for types themselves
In this subsection we work with the µ-types themselves instead of their α-equivalence
classes. On this set of types →µ/α is the reduction relation on the set of types TTµ
generated by →µ and →α . We show that the relation =µ/α on TTµ is decidable via the
first order decision procedure of Definition 1.12 for types.
2.1. Definition. →µ/α is the reduction relation on the set of types TTµ generated by
→µ and →α .
=µ/α is the transitive, symmetric, reflexive closure of →µ/α . →∗µ/α denotes zero or more
→µ/α steps.
We will show
A =µ/α B ⇔ ⊢µ′ A = B.
where ⊢µ′ derives equations between types in TTµ′ , as given in Definition 1.12 and moreover that this relation is decidable.
From now on α-quivalence classes in TTµ and TTµ′ are denoted by [A] and [a]. =[µ] stands
for equality on the set of α-equivalence classes [A] and ⊢[µ′ ] denotes the derivation system
of Definition 1.15 for classes [a] where a ∈ TTµ′ .
2.2. Lemma. ⊢µ′ a = b ⇔ ⊢[µ′ ] [a] = [b] and both derivations can be done by the ”same”
steps. Equivalently they have the same length.
Proof. Immediate
2.3. Lemma. A =µ/α B ⇔ [A] =[µ] [B].
Proof. Immediate
Combining Remark 1.5, Proposition 1.18 and Lemmas 2.2 and 2.3 we get

WEAK µ-EQUALITY IS DECIDABLE

11

2.4. Corollary. A =µ/α B ⇔ ⊢µ′ A = B.
Finally by Lemma 2.2 we have that ⊢µ′ A = B is decidable. In fact there is a bijection
from the derivation tree for ⊢µ′ A = B on the derivation tree for ⊢[µ′ ] [A] = [B]. So we
have the following
2.5. Theorem. A =µ/α B is decidable via the first order decision procedure ⊢µ′ A = B.
2.6. Remark. In this part 2 we do not have Lemma 1.22 for types. It only holds modulo
α-equivalence.
References
[1] Felice Cardone and Mario Coppo. Decidability Properties of Recursive
Types. In C. Blundo and C. Laneve, editors, ICTCS 2003 volume 2841 of
LNCS, pages 242-255. Springer, 2003.
[2]Jörg Endrullis, Clemens Grabmayer, Jan Willem Klop, Vincent van Oostrom. On equal µ-terms. 2011. Free university Amsterdam.
[3] V. van Oostrom. FD à la Melliès. February 1997. Free University Amsterdam.

