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: community: our work

Topic: Stelios Tsampas (and HO-GSOS)

Stelios Tsampas (Feb 16 2024 at 16:23):

Hello y'all. I'm starting this conversation to introduce you to my ongoing work on Higher-Order Mathematical Operational Semantics or Higher-Order Abstract GSOS (HO-GSOS). HO-GSOS is a categorical framework (I will explain shortly what I mean by "framework") of higher-order languages. The development of HO-GSOS and its theory takes place mainly in FAU Erlangen, the key contributors being (apart from myself) @Sergey Goncharov , @Henning Urbat , Stefan Milius and Lutz Schröder. I will break this post in three parts:

1) What do I mean by a framework and why I care.
2) Background and brief description of HO-GSOS.
3) Completed and ongoing work.

1) The "formal reasoning" branch of programming language theory often features works fitting a certain trope: an operational semantics is given, a certain question pertaining to program behavior is posed and said question is answered via a complex and laborious proof. Sometimes the question is rather specific, other times it is an instance of a general problem; in the latter case, the given operational semantics serves as a "representative" language, and the argumentation is presented, again, as an instance of a vaguely generic method that one can hope to apply to other instances. There are other variations of this trope, e.g. there can be two or more languages instead of one, but the idea remains the same.

Up to this point, formal reasoning for PL has resisted efforts towards systematically organizing reasoning methods under a common mathematical roof. I find this problematic, not only because I prefer elegant and unifying theories to ad-hoc methods, but mainly because it exposes formal proofs to expected scaling issues: i) one has to constantly reinvent the wheel, ii) the proofs are brittle w.r.t. to the parameters of the problem and iii) proofs scale badly w.r.t. the size of the language, making them extremely hard to apply to real-world languages.

Stelios Tsampas (Feb 16 2024 at 16:23):

The above outlines the key features of a potential "framework for programming languages" (borrowing ideas from the intro of Peio Borthelle, @Tom Hirschowitz and Ambroise Lafont [1]; Tom is in fact working towards systematizing formal reasoning, you should check out his work!):

a. It should be based on a well-defined, mathematical notion of a programming language.
b. It should provide abstract reasoning principles and methods (such as
abstract versions of Howe's method and logical relations), without the need to
set up complex machinery.
c. In terms of usability and efficiency, the above should be broad, generic and scalable, being able to model common programming paradigms and real-world programming languages.

Back in 1997, Turi and Plotkin [2] introduced Abstract GSOS, a theory that could legitimately claim a. and, to a limited degree, b. and c. of the above points.

Next up, a brief intro to (higher-order) abstract GSOS.

[1] A Cellular Howe Theorem, LICS 2020
[2] Towards a Mathematical Operational Semantics, LICS 1997

Stelios Tsampas (Feb 16 2024 at 16:23):

2) In the original abstract GSOS, (first-order) operational semantics are modelled by GSOS laws, i.e. natural transformations of the form

$\Sigma(X \times BX) \to B\Sigma^{\star}X~~(1)$,

where $\Sigma, B : \mathbb{C} \to \mathbb{C}$ are endofunctors in some distributive category $\mathbb{C}$. Functor $\Sigma$ can be understood as an algebraic signature in the standard way and $B X$ as the type of "structured successors of programs from X". This framework was significant and powerful for two main reasons:

• Turi and Plotkin made the beautiful observation that the standard (i.e. concrete, first-order) GSOS specifications over a signature $\Sigma : \mathbf{Set} \to \mathbf{Set}$ are in a bijective correspondence with GSOS laws of $\Sigma$ over $BX = (\mathcal{P}X)^{A}$ for some set $A$. More generally, this mathematical formalization of operational semantics as natural transformations is not just conveniently rigorous, it is also very precise and natural. This enabled people to meaningfully study systems at a high level of abstraction.
• Naturality captures the intuitive fact that the behavior of complex terms is determined only by the behavior of their subterms, and not the subterms' internal structure. Formally, naturality is in fact the critical cog ensuring that bisimilarity is compatible with the operations of the language (i.e. bisimilarity is a congruence), a key well-behavedness property.

The above facts drew me to this framework, which I studied quite intently, eventually producing relevant work on secure compilers and weak bisimilarity with @Christian Williams among others.

By far the biggest problem with abstract GSOS was its inadequacy to model higher-order languages like the $\lambda$-calculus. At some point, @Christian Williams and I tried to do just that, to extend the framework, to fit the $\lambda$-calculus to abstract GSOS, but we (like others before us) failed. However, the Erlangen group gave it another go in 2022 and a few good ideas later, HO-GSOS was born [3].

Stelios Tsampas (Feb 16 2024 at 16:24):

Briefly, under the HO-GSOS framework, a higher-order operational semantics now consists of i) an endofunctor $\Sigma : \mathbb{C} \to \mathbb{C}$, modelling syntax as before, ii) a bifunctor $B : \mathbb{C}^{\mathrm{op}} \times \mathbb{C} \to \mathbb{C}$, where $B(X,Y)$ represents the "structured successors of programs in $Y$, potentially accepting programs in $X$ as inputs", and iii) a family of maps

$\Sigma(X \times B(X,Y)) \to B(X, \Sigma^{\star}(X + Y))~~(2)$,

natural in $Y$ and dinatural in $X$. Generalizing from natural to dinatural transformations is a rather standard idea. The challenging part was showing that (2) faithfully models actual higher-order systems (doing so for the $\lambda$-calculus was one of the highlights of [3]) and that bisimilarity is still a congruence. These facts meant that the fundamental advantages of abstract GSOS do indeed carry over to our higher-order setting; they also served as a green light for further research, to find out how powerful HO-GSOS really is.

In the next post (arriving later today or tomorrow), I will summarize our latest developments on HO-GSOS [4,5,6]; in particular, I will argue that one can implement common reasoning methods at the level of generality of HO-GSOS, and how this solves important efficiency considerations, as well as exposing their language-specific parts.

In the meantime, I hope you find this interesting and fun ;). If you have any questions (e.g. exactly how (1) and (2) model operational semantics) or other remarks, fire away.

[3] Towards a Higher-Order Mathematical Operational Semantics, POPL 2023
[4] Weak Similarity in Higher-Order Mathematical Operational Semantics, LICS 2023
[5] Logical Predicates in Higher-Order Mathematical Operational Semantics, FoSSaCS 2024
[6] Bialgebraic Reasoning on Higher-Order Program Equivalence, arXiv

Stelios Tsampas (Feb 16 2024 at 17:34):

Let me add that the HO-GSOS programme falls within the applied category theory area.

Stelios Tsampas (Feb 17 2024 at 00:12):

3) Right, the reasoning methods on operational semantics. I will focus on logical relations, probably the most popular method out there. So what are logical relations? Most people who work with logical relations don't bother answering this question; a humorous take is that nobody knows what they are, but they know how to spot one (see the intro of [7] for a similar take). Just to be clear, people have given formal definitions of the qualifier "logical" used in "logical relation" before (Plotkin, Tait, Dal Lago, Gavazzo, @Jon Sterling and many more), the joke mostly applies to logical relations as a proof method, which is presented demonstratively rather than as a formal, generic argument, as it should. Reasoning with logical relations looks like this:

Say an operational semantics (SOS rules) of a typed language is given, and one wants to construct a (type-indexed) relation $R_{\tau} \subseteq \mu\Sigma_{\tau} \times \mu\Sigma_{\tau}$ for $\mu\Sigma$ the initial algebra (the type-indexed family of program terms) of an endofunctor $\Sigma$, such that $R_{\tau}(a,b)$ implies that $a$ and $b$ are contextually, or observationally, equivalent (another interesting fact to prove would be the so-called fundamental lemma, namely that $R$ is reflexive). In most cases, one can come up with a certain "candidate" type-indexed relation, say $\square$, which has the following characteristic property on programs in the "function" type $\tau_{1} \to \tau_{2}$:

$\square_{\tau_{1} \to \tau_{2}}(a,b)$ if for all $d,e : \tau_{1}$ such that $\square_{\tau_{1}}(d,e)$, then $\square_{\tau_{2}}(a(d),b(e))$,

Stelios Tsampas (Feb 17 2024 at 00:12):

where $a(d),b(e) : \tau_{2}$ stands for something like application in the $\lambda$-calculus. In other words, "related inputs are mapped to related outputs". Now, $\square$ is only useful if it is a congruence, i.e. compatible with the operations of the language (this suffices to show both that $\square$ implies contextual equivalence and that $\square$ is reflexive). Proving congruence is a laborious and error-prone task. The logical relations proof method thus consists of two parts:

a. Coming up with the logical relation, which is non-trivial.
b. Proving that it is a congruence, which is tough.

Let's see how category theory and HO-GSOS helps doing our job easier. In HO-GSOS, the rules induce a coalgebra, the so-called operational model, on the initial algebra $\mu\Sigma$ of endofunctor $\Sigma$ by induction (we're in a typed setting so the following map is type-indexed accordingly):

$\gamma_{\tau} : \mu\Sigma \to B_{\tau}(\mu\Sigma,\mu\Sigma)$

Stelios Tsampas (Feb 17 2024 at 00:13):

A very nice insight of our recent work [5,6] was that logical predicates/relations amount to Hermida-Jacobs invariants/bisimulations for higher-order programs. In our case, a relation $R$ is logical if the following is true:

$R_{\tau} \leq \gamma_{\tau}^{\star}[\overline{B}_{\tau}(R,R)]~(3)$,

where $\gamma_{\tau}^{*}$ is the preimage of $\gamma_{\tau}$ and overline $\overline{B}$ is a (bifunctorial) relation lifting. Indeed, instantiating (3) to the $\lambda$-calculus gives the expected notion. Worth noting is that so far I'm only making use of standard, well-known notions: coalgebras and relation liftings, simply extended to a bifunctorial setting. Now, as it turns out, there's a generic fixed-point construction on the complete lattice of relations in $\mu\Sigma$ that allows one to automatically get the "candidate" (step-indexed) logical relation which, modulo a simple condition that can be verified by inspecting the rules, is automatically a cogruence. Let's compare a. and b. earlier to the situation in HO-GSOS:

a. The logical relation is given as a generic construction.
b. Proving that it is a congruence is a matter of a simple condition.

Stelios Tsampas (Feb 17 2024 at 00:20):

I will stop here for now. Hopefully this series of posts ignited your interest enough to read the HO-GSOS papers [3,4,5,6], which are all available online on arXiv, including the one on Howe's method [4] which, conceptually, works similarly to [5] and [6].

[3] Towards a Higher-Order Mathematical Operational Semantics, Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, Henning Urbat, POPL 2023, available online.
[4] Weak Similarity in Higher-Order Mathematical Operational Semantics, Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, Henning Urbat, LICS 2023, available online
[5] Logical Predicates in Higher-Order Mathematical Operational Semantics, Sergey Goncharov, Alessio Santamaria, Lutz Schröder, Stelios Tsampas, Henning Urbat, FoSSaCS 2024, available online
[6] Bialgebraic Reasoning on Higher-Order Program Equivalence, Sergey Goncharov, Stefan Milius, Stelios Tsampas, Henning Urbat, available online

Stelios Tsampas (Feb 17 2024 at 00:26):

On the short term, we plan to work on call-by-(push)-value languages (which the framework supports but doesn't give ideal congruence results out-of-the-box), which I'm sure @Max New would be interested in, and doing polymorphic languages like System F (so far we've only covered recursive types).