

CAUTION: This email originated from outside the organisation. Do not click links or open attachments unless you recognise the sender and know the content is safe.


Dear Sergey,

On behalf of the Programme Committee of CALCO 2025, we are happy to inform you that your early idea contribution 11

From Abstract Higher-Order GSOS to Abstract Big-Step Semantics, Abstractly (Early ideas)

has been accepted for presentation at CALCO 2025.

The reviews for your submission are attached below. Please take the reviewer comments into account when preparing the final version. More details regarding the final version will follow shortly.

We look forward to seeing you in Glasgow!

Best regards,
Corina and Alexander.

SUBMISSION: 11
TITLE: From Abstract Higher-Order GSOS to Abstract Big-Step Semantics, Abstractly (Early ideas)


----------------------- REVIEW 1 ---------------------
SUBMISSION: 11
TITLE: From Abstract Higher-Order GSOS to Abstract Big-Step Semantics, Abstractly (Early ideas)
AUTHORS: Sergey Goncharov, Pouya Partow and Stelios Tsampas

----------- Overall evaluation -----------
SCORE: 2 (accept)
----- TEXT:
This "early idea" abstract on abstract big-step semantics through abstract higher-order GSOS (AHOGSOS) is well in scope of CALCO.
I see no reason to reject it.

That said, I am not an expert on GSOS and I failed to understand the technical content of this abstract.  I made an honest attempt, and my comments below could be seen as a proof-of-work.

The failure to communicate might be due to the lack of space the authors had for the presentation, but I also see some essential shortcoming.  Half a page, that is 25% of the total available space of 2 pages, is spent on the example of combinatory logic (CL), but then the example is not connected to the abstract framework it was intended to illustrate.

Very concretely, the functors Σ and B should be instantiated to CL, and then also the refinement of them presented in the "separability" part.

The question is whether then there is enough space remaining for all of the content of the abstract.  If I had to make the choice, I would put the counterexample (l55ff) into a technical report and link to it from the abstract.  This counterexample takes around 15% of the total space, and these 15% could be used instead to connect the abstract framework to the CL example.

Details
=======

Small-step and big-step semantic for CL are well-presented, but then AHOGSOS is introduced, CL is not connected to its formalism.  The question is, why do you prepare the reader by a concrete example just to drop it once you go to the abstract mathematics?

From the level of difficulty, I think when you sit down an implement big-step operational semantics for CL, you quickly converge to the presentation you call xCL where you form "closures" for underapplied uses of K and S.  In contrast, an abstract framework for SOS is not something that suggests itself.

Concretely, I am missing answers for the following questions:
1. Category C, what do its objects and morphisms denote?
2. What is the signature functor Σ for the case of xCL?
3. What is the behavior functor B?
4. Likewise what are then Σᵥ, Σ_c, D and T?

My guesses:
1. The objects of C are representing sets of terms, morphisms functions.
2. Σ is the "non-recursive" presentation of the language of xCL, e.g.
   ```haskell
   data Σ X = I | K | S | K' X | S' X | S'' X X | App X X
   ```
3. Here I am lost with my current background knowledge, as I would expect now some relation specifying the operational semantics, but B targets C.

Reading Turi and Plotkin [4], I might get some more clues.
There, B is the "successor" functor for the operational semantics, producing for a set X of terms the collection B X of terms reachable by a single operational step.  This collection B is organized by the labels a ∈ A on the rules of the operational semantics.
The "abstract GSOS" simply speaks of ρX : Σ(X × BX) → B(TX) which comes close to the presentation here assuming that the set TX of terms over X is Σ^⋆X.
Somehow fact that the labels in xCL are also terms materializes in a B : Cᵒᵖ × C → C, but it is not clear to me which of the positions of B are for the labels and which for the lhss.
Guessing that X is for the lhss in accordance with paper [4], I do not understand why B(X,Y) becomes contravariant in X when in [4] it was covariant.

So, if the xCL example shall be of any use in this abstract, B needs to spelled out for xCL.



----------------------- REVIEW 2 ---------------------
SUBMISSION: 11
TITLE: From Abstract Higher-Order GSOS to Abstract Big-Step Semantics, Abstractly (Early ideas)
AUTHORS: Sergey Goncharov, Pouya Partow and Stelios Tsampas

----------- Overall evaluation -----------
SCORE: 1 (weak accept)
----- TEXT:
A categorical approach to relate big-step and small-step operational semantics in terms of higher-order GSOS is outlined.

Though well-motivated in principle in a presentation it would seem advantageous to first see the workings of moving between the two operational semantics types on the rule level before diving into the categorical details.  In particular, it seems that some of the issues that still have to be solved - the strong separation condition - are best explained with conditions on rules.



----------------------- REVIEW 3 ---------------------
SUBMISSION: 11
TITLE: From Abstract Higher-Order GSOS to Abstract Big-Step Semantics, Abstractly (Early ideas)
AUTHORS: Sergey Goncharov, Pouya Partow and Stelios Tsampas

----------- Overall evaluation -----------
SCORE: 2 (accept)
----- TEXT:
The paper outlines an approach for relating small-step and big-step
operational semantics in an abstract categorical setting. The authors
build on the existing theory of abstract higher-order GSOS where the
small-step semantics can be specified categorically. This is extended
to a separated higher-order GSOS, separating the the syntax into value
constructors and computation constructors. In this setting one can
define a multistep semantics as least fixpoint and abstract the
big-step semantics as a natural transformation from computation
constructors applied to values to a monad of results.

The authors observe that separability alone is not enough to prove the
fundamental equivalence between small-step and big-step semantics and
identify a stronger condition, which abstracts the idea of suitably
constraining the shape of rule conclusions based on the premises, as a
potential way to remedy this issue.

The theme is surely of interest for CALCO. The authors did a good job
in sythesizing in a limit space the main ideas of their work. For a
non-expert (like me) the technical details are difficult to grasp from
the short summary, but I do not see this as a problem. Rather, I think
this can be a quite interesting and valuable addition to CALCO's program.


