<p>Pataraia's fixed point theorem gives a constructive proof of the fact that if you have a monotone function $f$ on a DCPO, then it has a least fixed point. I've frequently used this fixed point theorem to construct logical relations for proving properties about dependent type theories. </p>

<p>The idea is that you can view a syntactic type system as a pair $(U, \phi)$ of a partial equivalence relation (or PER) $U$, representing the codes of types, and an interpretation function $\phi : U \to \mathrm{PER}$, sending each type code to its interpretation. Semantic type systems can be equipped with a domain structure, by saying that $(U', \phi') \sqsubseteq (U, \phi)$ just when $U' \subseteq U$, and for every type $A \in |U'|$, we have that $\phi(A) = \phi'(A)$. The empty type system is the obvious bottom element, and joins exist in the obvious way. Then a logical relation can be constructed as a fixed point of a monotone map with respect to this ordering. </p>

<p>However, this semantic definition also bears a strong relationship to inductive-recursive definitions, where the set $U$ and the interpretation $\phi$ are defined simultaneously. (Unsurprisingly, since generalizing universe constructions was  the prime motivation for the invention of induction-recursion.) </p>

<p>Has anyone looked at the relation between the two? It's not obvious to me, since the proof of Pataraia's theorem, while constructive, is rather impredicative (it seems to rely essentially upon the powerset operation). So:</p>

<ol>
<li>Can Pataraia's theorem be used to prove  the soundness of the full induction-recursion schema?</li>
<li>To what extent can induction-recursion be used to prove the converse? (I assume it won't go all the way, but maybe I'm wrong!) </li>
</ol>

CC BY-SA 3.0
2017-06-27T19:25:33.627Z
Doesn't your setup require powersets as well? That is, you say that you have functions $\phi : U \to \mathrm{PER}$. Their codomain seems to involve powersets.
Andrej Bauer
CC BY-SA 3.0
2017-06-27T19:26:43.607Z
Are you asking whether the particular instance of induction-recursion is related to Pataraia's theorem, or whether *general* induction-recursion is related to Pataraia's theorem?
Andrej Bauer
CC BY-SA 3.0
2017-06-28T08:57:22.183Z
@AndrejBauer That's part of the question! My proof via P's theorem uses powersets, since $\phi$ has a large codomain. However, you can  alternatively define the logical relation with large induction-recursion (where you define a type and a family of sets simultaneously). This is borderline impredicative, and I'm wondering if (a) P's theorem is enough to interpret the full large IR schema, and (b) how much of P's theorem large IR can prove.
Neel Krishnaswami
CC BY-SA 3.0
2017-06-29T09:58:22.730Z
Large? PERs form a set.
Andrej Bauer
CC BY-SA 3.0
2017-06-29T11:07:14.693Z
From a type theorist's pov -- if you try to define it in Agda, the $\phi$-component's recursive definition is entwined with the inductive definition of $U$. This is dubbed "large induction-recursion", since the output of $\phi$ is a set at the same level as $U$. Proper Scandinavian type theorists assert that this is predicative, but I don't know of any fixed point theorem weaker than Pataraia's theorem which will let me interpret this, and the only proof of Pataraia's theorem I know is impredicative.
Neel Krishnaswami
CC BY-SA 3.0
2017-06-29T16:17:20.743Z
By the way, why Pataraia's theorem and not simply Tarski's theorem? PERs form a complete lattice. Also, the impredicativity of these theorems lies not in their proofs, but in their *formulations*: *if* we have a complete lattice *then* every monotone map on it has a fixed point. The proof itself just uses the assumption that something is a complete lattice. So I don't see how to even state Tarski's fixed-point theorem in a predicative setting. Hmm, the CZF people must have done it.
Andrej Bauer
CC BY-SA 3.0
2017-06-29T16:26:53.463Z
There we go: https://arxiv.org/pdf/1301.2793.pdf
Andrej Bauer
CC BY-SA 3.0
2017-06-30T09:34:15.983Z
PERs form a lattice, sure, but *type systems* (pairs $(U, \phi)$) only have domain structure.
Neel Krishnaswami
<lo.logic><pl.programming-languages><type-theory><dependent-type><fixed-points>
Relationship between Pataraia's theorem and inductive-recursive definitions?
Neel Krishnaswami
# Relationship between Pataraia's theorem and inductive-recursive definitions?

(Asked by: username_0 on 2017-06-27)

Pataraia's fixed point theorem gives a constructive proof of the fact that if you have a monotone function $f$ on a DCPO, then it has a least fixed point. I've frequently used this fixed point theorem to construct logical relations for proving properties about dependent type theories.

The idea is that you can view a syntactic type system as a pair $(U, \phi)$ of a partial equivalence relation (or PER) $U$, representing the codes of types, and an interpretation function $\phi : U \to \mathrm{PER}$, sending each type code to its interpretation. Semantic type systems can be equipped with a domain structure, by saying that $(U', \phi') \sqsubseteq (U, \phi)$ just when $U' \subseteq U$, and for every type $A \in |U'|$, we have that $\phi(A) = \phi'(A)$. The empty type system is the obvious bottom element, and joins exist in the obvious way. Then a logical relation can be constructed as a fixed point of a monotone map with respect to this ordering.

However, this semantic definition also bears a strong relationship to inductive-recursive definitions, where the set $U$ and the interpretation $\phi$ are defined simultaneously. (Unsurprisingly, since generalizing universe constructions was the prime motivation for the invention of induction-recursion.)

Has anyone looked at the relation between the two? It's not obvious to me, since the proof of Pataraia's theorem, while constructive, is rather impredicative (it seems to rely essentially upon the powerset operation). So:

1. Can Pataraia's theorem be used to prove the soundness of the full induction-recursion schema?
2. To what extent can induction-recursion be used to prove the converse? (I assume it won't go all the way, but maybe I'm wrong!)

**Tags:** lo.logic, pl.programming-languages, type-theory, dependent-type, fixed-points

> **Comments:**
> **username_1**: Doesn't your setup require powersets as well? That is, you say that you have functions $\phi : U \to \mathrm{PER}$. Their codomain seems to involve powersets.  
> **username_1**: Are you asking whether the particular instance of induction-recursion is related to Pataraia's theorem, or whether *general* induction-recursion is related to Pataraia's theorem?  
> **username_0**: @AndrejBauer That's part of the question! My proof via P's theorem uses powersets, since $\phi$ has a large codomain. However, you can  alternatively define the logical relation with large induction-recursion (where you define a type and a family of sets simultaneously). This is borderline impredicative, and I'm wondering if (a) P's theorem is enough to interpret the full large IR schema, and (b) how much of P's theorem large IR can prove.  
> **username_1**: Large? PERs form a set.  
> **username_0**: From a type theorist's pov -- if you try to define it in Agda, the $\phi$-component's recursive definition is entwined with the inductive definition of $U$. This is dubbed "large induction-recursion", since the output of $\phi$ is a set at the same level as $U$. Proper Scandinavian type theorists assert that this is predicative, but I don't know of any fixed point theorem weaker than Pataraia's theorem which will let me interpret this, and the only proof of Pataraia's theorem I know is impredicative.  
> **username_1**: By the way, why Pataraia's theorem and not simply Tarski's theorem? PERs form a complete lattice. Also, the impredicativity of these theorems lies not in their proofs, but in their *formulations*: *if* we have a complete lattice *then* every monotone map on it has a fixed point. The proof itself just uses the assumption that something is a complete lattice. So I don't see how to even state Tarski's fixed-point theorem in a predicative setting. Hmm, the CZF people must have done it.  
> **username_1**: There we go: https://arxiv.org/pdf/1301.2793.pdf  
> **username_0**: PERs form a lattice, sure, but *type systems* (pairs $(U, \phi)$) only have domain structure.  

---

## 0 answers

