6
$\begingroup$

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!)
|cite|improve this question
$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer Jun 27 '17 at 19:25
  • $\begingroup$ 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? $\endgroup$ – Andrej Bauer Jun 27 '17 at 19:26
  • $\begingroup$ @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. $\endgroup$ – Neel Krishnaswami Jun 28 '17 at 8:57
  • $\begingroup$ Large? PERs form a set. $\endgroup$ – Andrej Bauer Jun 29 '17 at 9:58
  • $\begingroup$ 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. $\endgroup$ – Neel Krishnaswami Jun 29 '17 at 11:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.