<p><span class="math-container">$\mu$</span> denotes <em>least</em> fixed points, so <span class="math-container">$\mu t. t$</span> should be <span class="math-container">$\bot$</span>, the initial/empty type (and <span class="math-container">$\nu t. t$</span> should be <span class="math-container">$\top$</span>, the terminal/unit type).</p>

CC BY-SA 4.0
2024-09-27T17:31:17.467Z
2024-09-27T17:31:17.467Z
Naïm Favier
<p>The type equation <span class="math-container">$t = t$</span> does not restrict <span class="math-container">$t$</span> in any way. All types <span class="math-container">$t$</span> satisfy that equation. So, the least fixpoint is the least possible type <span class="math-container">$t$</span>, that is, <span class="math-container">$\bot$</span>, and the greatest fixpoint is the greatest possible type, that is, <span class="math-container">$\top$</span>.</p>

CC BY-SA 4.0
2024-10-07T08:41:03.213Z
2024-10-07T08:41:03.213Z
winitzki
<p>In the paper:</p>
<p><em>David B. MacQueen, Gordon D. Plotkin, Ravi Sethi: An Ideal Model for Recursive Polymorphic Types. Inf. Control. 71(1/2): 95-130 (1986).</em></p>
<p>the authors give a domain theoretic model for a large class of recursive types. More specifically, a large class of &quot;well-behaved&quot; types is defined (the so-called <em>contractive</em> ones) and their meaning is defined through the Banach fixpoint theorem.</p>
<p>As it turns out, a particularly simple recursive type that is not contractive, is the  <span class="math-container">$\mu t.t$</span> one (which corresponds to the recursive type definition <span class="math-container">$t=t$</span>). I was wondering, from a domain theoretic point of view, what should the meaning of this type be? One could say that its meaning is the trivial type (in the terminology of the above paper, the set that contains only the <span class="math-container">$\perp$</span> element). Alternatively, one could say that  the meaning of the equation is the whole space of all possible values (denoted by <strong>V</strong> in the above paper). This second choice could be justified because the equation <span class="math-container">$t=t$</span> does not impose any restriction on the elements that satisfy it. Which of the two choices is the correct one?</p>

<type-theory><denotational-semantics>
The meaning of the recursive type μt.t
LaR
# The meaning of the recursive type μt.t

(Asked by: username_0 on 2024-09-27)

In the paper:

*David B. MacQueen, Gordon D. Plotkin, Ravi Sethi: An Ideal Model for Recursive Polymorphic Types. Inf. Control. 71(1/2): 95-130 (1986).*

the authors give a domain theoretic model for a large class of recursive types. More specifically, a large class of "well-behaved" types is defined (the so-called *contractive* ones) and their meaning is defined through the Banach fixpoint theorem.

As it turns out, a particularly simple recursive type that is not contractive, is the $\mu t.t$ one (which corresponds to the recursive type definition $t=t$). I was wondering, from a domain theoretic point of view, what should the meaning of this type be? One could say that its meaning is the trivial type (in the terminology of the above paper, the set that contains only the $\perp$ element). Alternatively, one could say that the meaning of the equation is the whole space of all possible values (denoted by **V** in the above paper). This second choice could be justified because the equation $t=t$ does not impose any restriction on the elements that satisfy it. Which of the two choices is the correct one?

**Tags:** type-theory, denotational-semantics


---

## 2 answers

### Answer by username_1 on 2024-09-27. Score: 5 | Accepted answer

$\mu$ denotes *least* fixed points, so $\mu t. t$ should be $\bot$, the initial/empty type (and $\nu t. t$ should be $\top$, the terminal/unit type).


---

### Answer by username_2 on 2024-10-07. Score: 1

The type equation $t = t$ does not restrict $t$ in any way. All types $t$ satisfy that equation. So, the least fixpoint is the least possible type $t$, that is, $\bot$, and the greatest fixpoint is the greatest possible type, that is, $\top$.


---

