Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: our papers

Topic: Towards a Higher-Order Mathematical Operational Semantics

Stelios Tsampas (Oct 26 2022 at 18:46):

I am happy to present the new paper I coauthored with my good friends and colleagues at Friedrich-Alexander-Universität Erlangen-Nürnberg called Towards a Higher-Order Mathematical Operational Semantics. Here's the abstract:

Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which has been successfully applied to obtain off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory of abstract GSOS specifications for higher-order languages, in effect transferring the core principles of Turi and Plotkin's framework to a higher-order setting. In our theory, the operational semantics of higher-order languages is represented by certain dinatural transformations that we term pointed higher-order GSOS laws. We give a general compositionality result that applies to all systems specified in this way and discuss how compositionality of the SKI calculus and the $\lambda$-calculus w.r.t. a strong variant of Abramsky's applicative bisimilarity are obtained as instances.

This work is especially meaningful for me, as I have been "in the hunt" for the Turi-Plotkin style semantics of the $\lambda$-calculus (or any higher-order language for that reason) for more than two years. At long last, the hunt is over. I bet @Christian Williams, who was part of the effort in the first year, will be interested in the outcome as well. Shoutout also to my friend @anuyts!

To give you an idea of what this is about, in 1999 Turi and Plotkin figured out that the operational semantics of certain classes of first-order systems are in an one-to-one correspondence with natural transformations of the form

$$\rho \colon \Sigma(X \times BX) \Rightarrow B\Sigma^{\star}X,$$

for a choice of a "syntax" endofunctor/signature $\Sigma \colon \mathbb{C} \to \mathbb{C}$ and a "behavior" functor $B \colon \mathbb{C} \to \mathbb{C}$ in some sensible category $\mathbb{C}$. For example, for $\mathbb{C} = \mathbf{Set}$ and $B = \mathcal{P}_{\omega}$ (the finite powerset functor), natural transformations like the above correspond bijectively to the so-called GSOS specifications.

This is a really nice framework as one gets compositionality for free for entire classes of systems. It does, however, have one very important issue: it doesn't support higher-order languages like the $\lambda$-calculus. Well, not any more :wink:.

@Tom Hirschowitz I know that you been following similar, yet diverging paths for what is essentially the same overarching problem and so I am inviting you to read this paper. I did the same w.r.t. your papers on the topic (e.g. https://arxiv.org/abs/2103.16833).

The paper is now available on arXiv (https://arxiv.org/abs/2210.13387).

Christian Williams (Oct 26 2022 at 18:55):

Wow! This looks great Stelios. I look forward to reading.

Stelios Tsampas (Oct 26 2022 at 19:00):

Absolutely! Sharpen up your presheaf skills :rolling_on_the_floor_laughing:.

Stelios Tsampas (Oct 26 2022 at 20:02):

@Nathanael Arkor might also be interested. And we're thinking of looking into your Algebraic models of simple type theories to possibly take our approach to the world of typed languages.

Tom Hirschowitz (Oct 27 2022 at 07:21):

Stelios Tsampas said:

Tom Hirschowitz I know that you been following similar, yet diverging paths for what is essentially the same overarching problem and so I am inviting you to read this paper. I did the same w.r.t. your papers on the topic (e.g. https://arxiv.org/abs/2103.16833).

Probably not a big surprise to you, but I've already read most of it :innocent:
And indeed I noticed that you've read my paper with @Ambroise, including our variant of Howe's format.
One puzzling question is: your proof does not look like an abstract form of Howe's method, so does it reveal that Howe's method is in fact not necessary for proving congruence in the higher-order case? Or does it only work because you deal with strong bisimilarity, which makes things easier?

Stelios Tsampas (Oct 27 2022 at 08:50):

Tom Hirschowitz said:

Stelios Tsampas said:

Tom Hirschowitz I know that you been following similar, yet diverging paths for what is essentially the same overarching problem and so I am inviting you to read this paper. I did the same w.r.t. your papers on the topic (e.g. https://arxiv.org/abs/2103.16833).

Probably not a big surprise to you, but I've already read most of it :innocent:
And indeed I noticed that you've read my paper with Ambroise, including our variant of Howe's format.
One puzzling question is: your proof does not look like an abstract form of Howe's method, so does it reveal that Howe's method is in fact not necessary for proving congruence in the higher-order case? Or does it only work because you deal with strong bisimilarity, which makes things easier?

Long story short no, the coequalizer method seems to get stuck when dealing with the standard, "weak" applicative bisimilarity as opposed to our strong version. Yet it's not the end of the world.

The issue is that the coequalizer represents the quotient of an equivalence relation, which in this case is the least equivalence relation that is closed under the operations of the language. Howe's closure is notably not transitive (nor symmetric, but that's besides the point), only left-closed on the choice of $\sim$, due to the unsound-ness of transitivity with weak bisimilarity (right? :face_with_raised_eyebrow:).

Right now that's OK. Strong applicative bisimilarity/coalgebraic bisimilarity is in my opinion the more fundamental equivalence and the abstract format perfectly allows one to express languages that make non-trivial decisions based on the $\beta$-reductions (or whatever similar invisible transition) of subterms. And that's true in the original framework.

In any case, in order to prove congruence of weaker equivalences for certain subclasses of HO GSOS laws, a categorical form of Howe's method looks, at the moment, almost inevitable.

Tom Hirschowitz (Oct 27 2022 at 09:07):

I'm having trouble following, sorry. I agree that Howe's closure is not transitive, but what do you mean by "left-closed on the choice of $\sim$"?

Regarding which of strong and weak bisimilarity is most fundamental, I'd argue that weak bisimilarity is, because iirc it agrees with contextual equivalence. What makes you prefer the strong variant?

Stelios Tsampas (Oct 27 2022 at 09:10):

Tom Hirschowitz said:

I'm having trouble following, sorry. I agree that Howe's closure is not transitive, but what do you mean by "left-closed on the choice of $\sim$"?

Regarding which of strong and weak bisimilarity is most fundamental, I'd argue that weak bisimilarity is, because iirc it agrees with contextual equivalence. What makes you prefer the strong variant?

For the first part: say you have ${\sim} \subseteq \Lambda \times \Lambda$ and denote $~{\hat\sim}~ \Lambda \times \Lambda$ its Howe's closure. Then if $a \mathbin{\hat\sim} b$ and $b \sim c$, we can conclude that $a \mathbin{\hat\sim} c$.

Stelios Tsampas (Oct 27 2022 at 09:25):

For the second part... I should give it up :joy:. I can't argue with the fundamental equivalence being the one that coincides with contextual equivalence. What I should say instead is that it's coalgebraically the more fundamental relation, insofar coalgebraic bisimilarity is the fundamental program equivalence when dealing with coalgebras. The basic, if you will.

Also, generally speaking, what if I add to the $\lambda$-calculus a context $\texttt{f}$ such that

$$\frac{p \to p'}{\texttt{f}(p) \not\to}$$

Shouldn't that be considered a flavor of the $\lambda$-calculus? Yet, clearly, standard applicative bisimilarity is not a congruence and contextual equivalence would be something strictly finer.

Stelios Tsampas (Oct 27 2022 at 09:30):

Again, probably one more reason why in PL theory the "fundamental" program equivalence is contextual equivalence.

Tom Hirschowitz (Oct 27 2022 at 09:34):

Stelios Tsampas said:

Then if $a \mathbin{\hat\sim} b$ and $b \sim c$, we can conclude that $a \mathbin{\hat\sim} c$.

Oh, ok, sure. I'm not sure I get the overall point though. I agree Howe's closure isn't transitive, and isn't closed by action of $\sim$ on the left. But its transitive closure agrees with $\sim$, right? So Howe's closure is only an intermediate step in the proof. Oh, was this meant to explain how your method differs from Howe's? If so, yes, I was already convinced of this, even though I couldn't have pinpointed it so specifically.

Tom Hirschowitz (Oct 27 2022 at 09:39):

Stelios Tsampas said:

For the second part... I should give it up :joy:. I can't argue with the fundamental equivalence being the one that coincides with contextual equivalence. What I should say instead is that it's coalgebraically the more fundamental relation, insofar coalgebraic bisimilarity is the fundamental program equivalence when dealing with coalgebras. The basic, if you will.

Also, generally speaking, what if I add to the $\lambda$-calculus a context $\texttt{f}$ such that

$$\frac{p \to p'}{\texttt{f}(p) \not\to}$$

Shouldn't that be considered a flavor of the $\lambda$-calculus? Yet, clearly, standard applicative bisimilarity is not a congruence and contextual equivalence would be something strictly finer.

I fully agree that applicative bisimilarity is not always the right equivalence. There are illustrative examples in Koutavas et al. And I'm very interested in generalising our approach to normal-form and environmental bisimulation. Although for now I'm rather trying to generalise it to cover more concrete instances of applicative bisimilarity... :rowboat:

Stelios Tsampas (Oct 27 2022 at 09:42):

Tom Hirschowitz said:

Stelios Tsampas said:

Then if $a \mathbin{\hat\sim} b$ and $b \sim c$, we can conclude that $a \mathbin{\hat\sim} c$.

Oh, ok, sure. I'm not sure I get the overall point though. I agree Howe's closure isn't transitive, and isn't closed by action of $\sim$ on the left. But its transitive closure agrees with $\sim$, right? So Howe's closure is only an intermediate step in the proof. Oh, was this meant to explain how your method differs from Howe's? If so, yes, I was already convinced of this, even though I couldn't have pinpointed it so specifically.

Yes, I just wanted to illustrate the difference. The point is that if one would try to replicate our method for weak bisimilarity, for instance after obtaining the "weak" transition system $\gamma^{\star} \colon \Lambda \to B(\Lambda,\Lambda)$, then one would probably not be able to induce a coalgebra structure $\Lambda_{\sim} \to B(\Lambda_{\sim},\Lambda_{\sim})$ (where $\Lambda_{\sim}$ is our coequalizer) using universal properties.

Stelios Tsampas (Oct 27 2022 at 09:45):

By the way, we have sketched a (rough) plan to implement Howe's method using relation lifting techniques. The mixed variance of $B$ makes things significantly more complicated though...

Stelios Tsampas (Oct 27 2022 at 09:50):

Tom Hirschowitz said:

I fully agree that applicative bisimilarity is not always the right equivalence. There are illustrative examples in Koutavas et al. And I'm very interested in generalising our approach to normal-form and environmental bisimulation. Although for now I'm rather trying to generalise it to cover more concrete instances of applicative bisimilarity... :rowboat:

That is very interesting. I'm very curious as to how you'll be able to do environmental bisimilarity in your framework. In this instance, I believe not doing things coalgebraically is an advantage! I, for once, am not sure how environmental bisimilarity can be achieved coalgebraically. On the other hand, normal form looks feasible.

Stelios Tsampas (Oct 27 2022 at 09:53):

Which instances of applicative bisimilarity are you trying to cover, if I may ask?

Tom Hirschowitz (Oct 27 2022 at 10:07):

Sure: Gordon's sort of cbv PCF, Biernacki and Lenglet's presentation of $\lambda$-calculus with delimited contituations (and sequels...). More ambitious: $\lambda$-calculus with algebraic effects, as in Gavazzo et al, Lenglet and Schmitt's higher-order process calculi (here the proof is in fact quite different, and subtle...). But I'd welcome other ideas!

Stelios Tsampas (Oct 27 2022 at 10:17):

I have no ideas at the moment :pensive: . The $\lambda$-calculus with effects is something that interests me greatly. I'm also happy to see that people are still interested in process-calculi-like program equivalences (just like in Gordon's and Lenglet and Schmitt's work), where coalgebraic bisimilarity seems to be relevant without the need for refinement, as opposed to Abramsky's standard applicative bisiimlarity.

Stelios Tsampas (Oct 27 2022 at 10:18):

All of those will be a good test for your framework w.r.t. its adaptability :).

Stelios Tsampas (Nov 10 2022 at 23:48):

This was accepted at POPL, thing is the submission still has the old title "Higher-Order Abstract GSOS". This should be fixed soon.