5
$\begingroup$

In Atkey & McBride ICFP 2013, they extend a simple type theory with guarded recursion indexed by clock variables $\triangleright^k$ and a clock quantification $\forall k. A$ that conveniently commutes with a great deal of connectives, most notably for this question

$$\forall k. A + B \cong (\forall k. A) + (\forall k. B)$$

This has been extended to dependent type theory, for instance Bizjak & Møgelberg MSCS 2020 and Sterling & Harper LICS 2018. Sterling & Harper's type theory supports the extension of the above to sigma-types (I think Bizjak & Møgelberg's does as well but I couldn't find it explicitly in the paper):

$$\forall k. \sum_{x:A} B \cong \sum_{x:\forall k. A} (\forall k. B[xk/x])$$

My first question is if the models in BM/HS accommodate a proof-irrelevant universe of propositions where

$$\forall k. \exists{(x:A)} \phi \cong \exists {(x:\forall k. A)} (\forall k. \phi[xk/x])$$

The reason I ask is that my intuitive model of these guarded dependent type theories is that within a context with a single clock variable $k$, a type $A$ can be interpreted in the topos of trees, i.e., a presheaf on $\omega$. Next, the clock quantification $\forall k. A$ can be interpreted as the set of $\omega$-chains, i.e., for each $i \in \omega$, an element $x_i : A_i$ that commutes with all projections $p_i(x_{i+1}) = x_i$. Finally a proposition $\phi$ would be a presheaf where every set $\phi_i$ is a subset of $1$.

It makes sense to me that in this model the $\Sigma$-type/coproduct would commute with taking the $\omega$-chain as the chain has to commute with projections, so you cannot "change from inl to inr", however, it seems false that an existential quantifier would! The example I have in mind is the weak bisimulation relation $\approx$ (valued in propositions) on the lift monad $L^k A \cong A + \triangleright^k (L^k A)$ from Møgelberg & Paviotti LICS '16. The proposition would be

$$\exists (x: L^k A) (\eta v) \approx x \wedge x \approx \Omega$$

where $v:A$ is anything and $\Omega$ is the "diverging" element. In my intuitive model,

$$\forall k. \exists (x: L^k A) (\eta v) \approx x \wedge x \approx \Omega$$

is true because for each step-index $i\in\omega$, We can take $x = x_i = \delta^{i+1}(\eta v)$ which is similar to $v$ by definition and similar to $\Omega$ by "time out". However the trick is that we are picking a different $x$ depending on the step index, so the switched version:

$$\exists (x: \forall k. L^k A) \forall k. (\eta v) \approx x k \wedge x k \approx \Omega$$

fails to allow this proof because we cannot assemble the $x_i$ into an $\omega$-chain. I think this proposition is false under that interpretation because anything that is similar to $\eta v$ must terminate at finite index, and so any $\omega$-chain of $x$s that satisfies $(\eta v) \approx x k$ will eventually be terminating and so eventually $x k \approx \Omega$ will be false.

So my second question is, if the clock quantifiers do commute with existential quantification then where did I go wrong in my intuitive reasoning above? And if they don't commute is there a variation on these models where they do?

$\endgroup$
2
  • $\begingroup$ I don't know, but I've emailed @JonathanSterling about it... $\endgroup$ Jul 18 at 10:01
  • $\begingroup$ Quick question : in your definition of weak bisimulation, do you not mean to existentially quantify over A rather than LA? $\endgroup$ Jul 18 at 10:18

2 Answers 2

4
$\begingroup$

Let me first say that I did not look carefully at the second part of your question, nor your sketch of why the clock quantifier should commute with propositional existential quantification.

I will restrict my comments to the question about clock quantification and the topos-logic's existential-quantification of both the Bizjak-Møgelberg and Sterling-Harper topoi. (Note that the latter is the open subtopos of the former under the proposition $\exists k : K. \top$). My comments should not be understood as pertaining to a notion of 'propositional truncation' for the PER model of Sterling and Harper; in PERs, there is not really a canonical notion of truncation (there are several possibilities that are quite inadequate in different ways), so let me really restrict my comments to the topos.

In this case, I do not expect the clock quantifier to distribute over the existential quantifier for arbitrary families of presheaves $A$ and predicates $\phi$. This would seem to need that $K$ is projective, but I do not see why that should be the case. In particular, unraveling the Kripke-Joyal semantics of $\forall k. \exists x. \phi k x$, it might be that there is no single $x$ that works for all clocks.

In particular, if we consider either the Bizjak-Møgelberg or Sterling-Harper topos, the following proposition holds: $\forall k. \exists n. \rhd^n_k \bot$. This corresponds to the fact that the Bizjak-Møgelberg topos classifies indexed families of filters on $\omega$ --- where the component of the generic generic family of filters at a given index $k$ is the predicate $\{n\mid \rhd^n_k \bot\}$. If the discussed commutation law held in general, it thus would imply $K\cong \bot$. This example was suggested by Max New.

On the other hand, if $A$ and $\phi$ are both clock-irrelevant, in the sense that $Ak \cong Ak'$ and modulo this isomorphism we have $\phi k = \phi k'$ and moreover it holds that $\exists k : K.\top$, then it does follow that the clock quantifier commutes with the existential quantification. Thus in the Sterling-Harper topos under these assumptions, it follows that the commutation law you ask for would hold in the special case of clock-irrelevant types and predicates. I do not believe it holds globally in the Bizjak-Møgelberg topos, but I haven't checked carefully.

Remark. Note that the reason the clock quantifier commuted with coproducts is that K is connected in the "multiplexed topos of trees" models of Bizjak-Møgelberg and Sterling-Harper. This property is also used, covertly(?), by Kristensen, Møgelberg and Vezzosi to do induction for HITs underneath a clock quantifier...

$\endgroup$
8
  • $\begingroup$ Just to confirm: in these topos models the clock quantification does commute with Sigma types? $\endgroup$
    – Max New
    Jul 18 at 11:31
  • 1
    $\begingroup$ In fact, in MLTT for any type $K$ and families $k:K \vdash Ak$ and $k:K, x:Ak \vdash Bkx$ the sigma type commutation law that you described holds. $\endgroup$ Jul 18 at 11:49
  • $\begingroup$ Oh I see, if you interpret the clock quantification as just a Pi type this is essentially a form of axiom of choice, and commuting with Sigma types is the usual “incorrect” rendering of AC. $\endgroup$
    – Max New
    Jul 18 at 12:05
  • $\begingroup$ That's right! Btw, I think that if A and \phi are both clock irrelevant, then it might in fact be possible to commute the existential under certain circumstances. Let me compute a bit more, and I'll update my answer. $\endgroup$ Jul 18 at 12:09
  • 1
    $\begingroup$ "Axiom of clockable choice"? $\endgroup$
    – Max New
    Jul 18 at 13:32
2
$\begingroup$

This question sounds related to Transfinite Iris, which proposes to change the Iris model from Nat-indexed propositions to Ordinal-indexed propositions to have "later" commute with existentials.

$\endgroup$
2
  • $\begingroup$ I think the question is a bit different; it is not about whether the later modality commutes with existentials, but whether the clock quantifier commutes with existentials. $\endgroup$ Jul 18 at 11:27
  • $\begingroup$ I think they are related, but gasche misstated the motivation in Transfinite Iris. In transfinite Iris, they wanted existentials to commute with the meaning, which was defined as |= Phi = forall i. Phi i, i.e., the proposition is “true at every step index”. Their motivation is to make a model where |= exists x. Phi is equivalent to exists x |= Phi, which is my intuitive reading of the commutativity of existentials with clock quantification. $\endgroup$
    – Max New
    Jul 18 at 12:12

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.