7
$\begingroup$

In "Types and Programming Languages", Pierce gives a translation from recursive types ($\mu$ types) to types expressed as regular trees: possibly infinite trees, but with finitely many distinct subtrees.

I'm wondering, is the converse true? Can every regular tree type be expressed using the $\mu$ fixpoint notation? It seems obvious that this can be done if you have mutually recursive types: you have a type for each subtree of the regular tree type. But can it be done with singly recursive types?

$\endgroup$
3
  • 2
    $\begingroup$ You can reduce mutable recursion to a single recursion, see Bekic's Theorem, see e.g. Section 10.1 of Winskel's book The Formal Semantics of Programming Languages. $\endgroup$ May 22, 2019 at 21:54
  • $\begingroup$ @MartinBerger Perfect, just what I was looking for! $\endgroup$ May 23, 2019 at 0:55
  • $\begingroup$ @MartinBerger If you write that as an answer I'll accept it $\endgroup$ May 23, 2019 at 0:55

1 Answer 1

7
$\begingroup$

You can reduce mutual recursion to a single recursion, see Bekic's Theorem, see e.g. Section 10.1 of Winskel's (1), where Bekic is worked out for programs rather than types. Note however that the details depend on the exact nature of the formal system in question. See A. Bauer's answer in (2) for the case of types.


  1. G. Winskel, The Formal Semantics of Programming Languages.

  2. CSTheory Stackexchange, Can Isorecursive types capture mutually recursive data types?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.