6
$\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$
  • 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$ – Martin Berger May 22 at 21:54
  • $\begingroup$ @MartinBerger Perfect, just what I was looking for! $\endgroup$ – jmite May 23 at 0:55
  • $\begingroup$ @MartinBerger If you write that as an answer I'll accept it $\endgroup$ – jmite May 23 at 0:55
6
$\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, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.