Towards a Higher-Order Mathematical Operational Semantics

2025-05-06 0 0 528.94KB 37 页 10玖币

侵权投诉

arXiv:2210.13387v2 [cs.LO] 26 Oct 2022

Towards a Higher-Order Mathematical Operational

Semantics

SERGEY GONCHAROV, Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

STEFAN MILIUS∗,Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

LUTZ SCHRÖDER†,Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

STELIOS TSAMPAS‡,Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

HENNING URBAT§,Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Compositionality proofs in higher-order languages are notoriously involved, and general semantic frame-

works guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin’s bialgebraic ab-

stract GSOS framework, which has been successfully applied to obtain oﬀ-the-shelf compositionality results

for ﬁrst-order languages, so far does not apply to higher-order languages. In the present work, we develop a

theory of abstract GSOS speciﬁcations for higher-order languages, in eﬀect 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 speciﬁed in this way and discuss

how compositionality of the SKI calculus and the 𝜆-calculus w.r.t. a strong variant of Abramsky’s applicative

bisimilarity are obtained as instances.

Additional Key Words and Phrases: Abstract GSOS, Categorical semantics, Higher-order reasoning

1 INTRODUCTION

Turi and Plotkin’s framework of mathematical operational semantics [Turi and Plotkin 1997] elu-

cidates the operational semantics of programming languages, and guarantees compositionality of

programming language semantics in all cases that it covers. In this framework, operational seman-

tics are presented as distributive laws, varying in complexity, of a monad over a comonad in a

suitable category. An important example is that of GSOS laws, i.e. natural transformations of type

𝜚𝑋:Σ(𝑋×𝐵𝑋 ) → 𝐵Σ★𝑋, (1.1)

with functors Σ, 𝐵 :C→Crespectively specifying the syntax and behaviour of the system at hand.

The idea is that a GSOS law represents a set of inductive transition rules that specify how programs

are run. For example, the choice of C=Set and 𝐵=(P𝜔)𝐿, where P𝜔is the ﬁnite powerset

functor and 𝐿a set of transition labels, leads to the well-known GSOS rule format for specifying

labelled transition systems [Bloom et al. 1995]. In fact, Turi and Plotkin show that GSOS laws of a

(polynomial) endofunctor Σ:Set →Set over (P𝜔)𝐿correspond precisely to GSOS speciﬁcations

with term constructors given by Σand terms emitting labels from 𝐿. For that reason, Turi and

Plotkin’s framework is often referred to simply as abstract GSOS.

∗Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – project number 470467389

†Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – project number 419850228

‡Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – project number 419850228

§Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – project number 470467389

Authors’ addresses: Sergey Goncharov, Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany, sergey.

goncharov@fau.de; Stefan Milius, Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany, stefan.milius@fau.de;

Lutz Schröder, Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany, lutz.schroeder@fau.de; Stelios Tsampas,

Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany, stelios.tsampas@fau.de; Henning Urbat, Friedrich-

Alexander-Universität Erlangen-Nürnberg, Germany, henning.urbat@fau.de.

1:2 Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat

The semantic interpretation of GSOS laws is conveniently presented in a bialgebraic setting (cf.

Section 2.2): Every GSOS law 𝜚(1.1) canonically induces a bialgebra

Σ(𝜇Σ)𝜄

−→ 𝜇Σ𝛾

−−→ 𝐵(𝜇Σ)

on the object 𝜇Σof programs freely generated by the syntax functor Σ, where the algebra structure 𝜄

inductively constructs programs and the coalgebra structure 𝛾describes their one-step behaviour

according to the given law 𝜚. The above bialgebra is thus the operational model of 𝜚. Dually, its

denotational model is a bialgebra

Σ(𝜈𝐵)𝛼

−−→ 𝜈𝐵 𝜏

−−→ 𝐵(𝜈𝐵),

which extends the ﬁnal coalgebra 𝜈𝐵 of the behaviour functor 𝐵(to be thought of as the do-

main of abstract program behaviours). Both the operational and the denotational model can be

characterized by universal properties, namely as the initial 𝜚-bialgebra and the ﬁnal 𝜚-bialgebra.

This immediately entails a key feature of abstract GSOS: The semantics is automatically composi-

tional, in that behavioural equivalence (e.g. bisimilarity) of programs is a congruence with respect

to the operations of the language. The bialgebraic framework has been used widely to establish

further correspondences and obtain compositionality results [Bartels 2004;Fiore and Staton 2006;

Goncharov et al. 2022;Klin and Sassone 2008;Miculan and Peressotti 2016].

As a ﬁrst step towards extending their framework to languages with variable binding, such as

the 𝜋-calculus [Milner et al. 1992] and the 𝜆-calculus, Fiore, Plotkin and Turi [1999] use the theory

of presheaves to establish an abstract categorical foundation of syntax with variable binding, and

develop a theory of capture-avoiding substitution in this abstract setting. Based on these foun-

dations, the semantics of ﬁrst-order languages with variable binding, more precisely that of the

𝜋-calculus and value-passing CCS [Milner 1989], is formulated in terms of GSOS laws on cate-

gories of presheaves [Fiore and Turi 2001].

However, the question of the mathematical operational semantics of the 𝜆-calculus, or generally

that of higher-order languages, still remains a well-known issue in the literature (see e.g. the in-

troductory paragraph by Hirschowitz and Lafont [2022]). Indeed, in order to give the semantics of

a higher-order language in terms of some sort of a distributive law of a syntax functor over some

choice of a behaviour functor, one needs to overcome a number of fundamental problems. For in-

stance, for a generic set 𝑋of programs, the most obvious set of “higher-order behaviours over 𝑋”

would be 𝑋𝑋, the set of functions 𝑓:𝑋→𝑋that expect an input program in 𝑋and produce a new

program. Of course, the assignment 𝑋↦→ 𝑋𝑋is not functorial in 𝑋but bifunctorial; more precisely,

the bifunctor 𝐵(𝑋 , 𝑌 )=𝑌𝑋:Setop ×Set →Set is of mixed variance. Working with mixed-variance

bifunctors as a basis for higher-order behaviour makes the situation substantially more complex

in comparison to Turi and Plotkin’s original setting. In particular, natural transformations alone

will no longer suﬃce as the technical basis of a framework involving mixed-variance functors, and

it is not a priori clear what the right notion of coalgebra for a mixed-variance functor should be.

In this paper, we address these issues, with a view to obtaining a general congruence result.

Contributions. We develop a theory of abstract GSOS for higher-order languages, essentially

extending Turi and Plotkin’s original framework. We model higher-order behaviours abstractly in

terms of syntax endofunctors of the form Σ=𝑉+Σ′:C→C, for a choice of an object 𝑉∈Cto be

thought of as an object of variables, and behaviour bifunctors 𝐵:Cop ×C→C. The key concept

introduced in our paper is that of a 𝑉-pointed higher-order GSOS law: a family of morphisms

𝜚𝑋,𝑌 :Σ(𝑗𝑋 ×𝐵(𝑗𝑋 , 𝑌 )) → 𝐵(𝑗𝑋, Σ★(𝑗𝑋 +𝑌)),

dinatural in 𝑋∈𝑉/Cand natural in 𝑌∈C, with 𝑗:𝑉/C→Cdenoting the forgetful functor from

the coslice category 𝑉/Cto C. We show how each 𝑉-pointed higher-order GSOS law inductively

Towards a Higher-Order Mathematical Operational Semantics 1:3

determines an operational semantics given by a morphism

𝛾:𝜇Σ→𝐵(𝜇Σ, 𝜇Σ)

where 𝜇Σis initial algebra for the syntax endofunctor Σ:C→C. In fact, much in analogy to

the ﬁrst-order case, we introduce a notion of higher-order bialgebra for the given law 𝜚, and show

that 𝛾extends to the initial such bialgebra.

From a coalgebraic standpoint, the operational semantics 𝛾:𝜇Σ→𝐵(𝜇Σ, 𝜇Σ)is a coalgebra for

the restricted endofunctor 𝐵(𝜇Σ,--):C→C. Our semantic domain of choice is the ﬁnal 𝐵(𝜇Σ,--)-

coalgebra (𝑍 , 𝜁 ), the object of behaviours determined by the functor 𝐵(𝜇Σ,--). We obtain a mor-

phism coit𝛾:𝜇Σ→𝑍by coinductively extending 𝛾; that is, we take the unique coalgebra mor-

phism into the ﬁnal coalgebra:

𝜇Σ𝐵(𝜇Σ, 𝜇Σ)

𝑍 𝐵(𝜇Σ, 𝑍 )

𝛾

coit𝛾𝐵(𝜇Σ,coit𝛾)

𝜁

Importantly, and in sharp contrast to ﬁrst-order abstract GSOS, the ﬁnal coalgebra (𝑍, 𝜁 )generally

does not extend to a ﬁnal higher-order bialgebra; in fact, a ﬁnal bialgebra usually fails to exist (see

Example 4.21). As a consequence, it turns out that proving compositionality in our higher-order

setting is more challenging, requiring entirely diﬀerent techniques and additional assumptions on

the base category Cand the functors Σand 𝐵.

Speciﬁcally, we investigate higher-order GSOS laws in a regular category C. As our main com-

positionality result, we show that the kernel pair of coit𝛾:𝜇Σ→𝑍(which under mild conditions

is equivalent to bisimilarity) is a congruence. We demonstrate the expressiveness of higher-order

GSOS laws by modelling two important examples of higher-order systems. We draw our ﬁrst ex-

ample, the SKI combinator calculus [Curry 1930], from the world of combinatory logic, which we

represent using a higher-order GSOS law on the category of sets. For our second example we

move on to a category of presheaves, on which we model the call-by-name and the call-by-value

𝜆-calculus. In all of these examples, we show how the induced semantics corresponds to strong

variants of applicative bisimilarity [Abramsky 1990]. We note that in the case of the call-by-value

𝜆-calculus, our coalgebraic version of applicative bisimilarity is nonstandard as it allows applica-

tion of functions to arbitrary closed terms, not just values.

While our framework lays the foundations towards a higher-order mathematical operational

semantics in the style of abstract GSOS, let us mention two of its current limitations and important

directions for future work. First, our compositionality result is about a rather ﬁne-grained notion of

program equivalence, viz. coalgebraic behavioural equivalence, and our ultimate goal is to reason

about weak coalgebraic bisimilarity, e.g. standard applicative bisimilarity for 𝜆-calculi. Second, we

presently do not incorporate eﬀects such as states to our setting. See Section 6 for more details.

Organization. In Section 2 we provide a brief introduction to the core categorical concepts that

are used throughout this paper. Moving on, in Section 3 we discuss examples from combinatory

logic and present a basic rule format for higher-order languages that illustrates the principles

behind our approach. Section 4 is where we deﬁne our notion of pointed higher-order GSOS law

and prove our main compositionality result (Theorem 4.12). In Section 5 we implement the call-

by-name and call-by-value 𝜆-calculus in our abstract framework. We conclude the paper with

a summary of the contributions and a brief discussion on potential avenues for future work in

Section 6.

1:4 Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat

Related work. Formal reasoning on higher-order languages is a long-standing research topic

(e.g. [Abramsky 1990;Abramsky and Ong 1993;Scott 1970]). The series of workshops on Higher

Order Operational Techniques in Semantics [Gordon and Pitts 1999] played an important role in es-

tablishing the so called operational methods for higher-order reasoning. The two most important

such methods are logical relations [Dreyer et al. 2011;O’Hearn and Riecke 1995;Statman 1985;Tait

1967] and Howe’s method [Howe 1989,1996], both of which remain in use to date. Other signiﬁcant

contributions towards reasoning on higher-order languages were made by Sangiorgi [1994,1996]

and Lassen [2005]. While GSOS-style frameworks ensure compositionality for free by mere adher-

ence to given rule formats, both logical relations and Howe’s method instead have the character

of robust but inherently complex methods whose instantiation requires considerable eﬀort.

Recently, notable progress has been made towards generalizing Howe’s method [Borthelle et al.

2020;Hirschowitz and Lafont 2022], based on previous work on familial monads and operational

semantics [Hirschowitz 2019]. According to the authors, their approach departs from Turi and

Plotkin’s bialgebraic framework exactly because the bialgebraic framework did not cover higher-

order languages at the time. Dal Lago et al. [2017] give a general account of congruence proofs, and

speciﬁcally Howe’s method, for applicative bisimilarity for 𝜆-calculi with algebraic eﬀects, based

on the theory of relators. Hermida et al. [2014] present a foundational account of logical relations

as structure-preserving relations in a reﬂexive graph category.

Rule formats like the GSOS format [Bloom et al. 1995] have been very useful for guaranteeing

congruence of bisimilarity at a high level of generality. However, rule formats for higher-order

languages have been scarce. An important example is that of Bernstein’s promoted tyft/tyxt rule

format [Bernstein 1998;Mousavi and Reniers 2007], which has similarities to our presentation of

combinatory logic in Section 3, but it is unclear whether or not the format has any categorical

representation. The rule format of Howe [1996] was presented in the context of Howe’s method.

A variant of Howe’s format was recently developed by Hirschowitz and Lafont [2022].

2 PRELIMINARIES

2.1 Category Theory

We assume familiarity with basic notions from category theory such as limits and colimits, func-

tors, natural transformations, and monads. For the convenience of the reader, we review some

terminology and notation used in the paper.

Products and coproducts. Given objects 𝑋1, 𝑋2in a category C, we write 𝑋1×𝑋2for their product,

with projections fst:𝑋1×𝑋2→𝑋1and snd:𝑋1×𝑋2→𝑋2. For a pair of morphisms 𝑓𝑖:𝑌→𝑋𝑖,

𝑖=1,2, we let h𝑓1, 𝑓2i:𝑌→𝑋1×𝑋2denote the unique induced morphism. Dually, we write 𝑋1+𝑋2

for the coproduct, with injections inl:𝑋1→𝑋1+𝑋2and inr :𝑋2→𝑋1+𝑋2, and [𝑔1, 𝑔2]:𝑋1+𝑋2→

𝑌for the copairing of morphisms 𝑔𝑖:𝑋𝑖→𝑌,𝑖=1,2.

Dinatural transformations. Given functors 𝐹 , 𝐺 :Cop ×C→D, a dinatural transformation from

𝐹to 𝐺is a family of morphisms 𝜎𝑋:𝐹(𝑋 , 𝑋 ) → 𝐺(𝑋 , 𝑋 )(𝑋∈C) such that for every morphism

𝑓:𝑋→𝑌of C, the hexagon below commutes:

𝐹(𝑋 , 𝑋 )𝐺(𝑋, 𝑋 )

𝐹(𝑌 , 𝑋 )𝐺(𝑋, 𝑌 )

𝐹(𝑌 , 𝑌 )𝐺(𝑌 , 𝑌 )

𝜎𝑋

𝐺(𝑋,𝑓 )𝐹(𝑓 ,𝑋 )

𝐹(𝑋,𝑓 )𝜎𝑌

𝐺(𝑓 ,𝑌 )

Towards a Higher-Order Mathematical Operational Semantics 1:5

Regular categories. A category is regular if (1) it has ﬁnite limits, (2) for every morphism 𝑓:𝐴→

𝐵, the kernel pair 𝑝1, 𝑝2:𝐸→𝐴of 𝑓has a coequalizer, and (3) regular epimorphisms are sta-

ble under pullback. In a regular category, every morphism 𝑓:𝐴→𝐵admits a factorization

𝐴𝑒

−−→ 𝐶𝑚

−−→ 𝐵into a regular epimorphism 𝑒followed by a monomorphism 𝑚: Take 𝑒to be the

coequalizer of the kernel pair of 𝑓, and 𝑚the unique factorizing morphism. Indeed the main pur-

pose of regular categories is to provide a notion of image factorization of morphisms that relates to

kernels of morphisms in a similar way as in set theory. Examples of regular categories include the

category Set of sets and functions, every presheaf category SetC, and every category of algebras

over a signature (see below). In all these cases, regular epimorphisms and monomorphisms are

precisely the (componentwise) surjective and injective morphisms, respectively.

Algebras. Given an endofunctor 𝐹on a category C, an 𝐹-algebra is a pair (𝐴, 𝑎)of an object 𝐴

(the carrier of the algebra) and a morphism 𝑎:𝐹𝐴 →𝐴(its structure). A morphism from (𝐴, 𝑎)

to an 𝐹-algebra (𝐵, 𝑏)is a morphism ℎ:𝐴→𝐵of Csuch that ℎ·𝑎=𝑏·𝐹ℎ. Algebras for 𝐹and

their morphisms form a category Alg(𝐹), and an initial 𝐹-algebra is simply an initial object in that

category. We denote the initial 𝐹-algebra by 𝜇𝐹 if it exists, and its structure by 𝜄:𝐹(𝜇𝐹 ) → 𝜇𝐹 .

Moreover, we write it 𝑎:(𝜇𝐹, 𝜄) → (𝐴, 𝑎)for the unique morphism from 𝜇𝐹 to the algebra (𝐴, 𝑎).

More generally, a free 𝐹-algebra on an object 𝑋of Cis an 𝐹-algebra (𝐹★𝑋, 𝜄𝑋)together with a

morphism 𝜂𝑋:𝑋→𝐹★𝑋of Csuch that for every algebra (𝐴, 𝑎)and every morphism ℎ:𝑋→𝐴

in C, there exists a unique 𝐹-algebra morphism ℎ★:(𝐹★𝑋, 𝜄𝑋) → (𝐴, 𝑎)such that ℎ=ℎ★·𝜂𝑋. As

usual, the universal property determines 𝐹★𝑋uniquely up to isomorphism. If free algebras exist

on every object, then their formation induces a monad 𝐹★:C→C, the free monad on 𝐹[Barr

1970]. For every 𝐹-algebra (𝐴, 𝑎), we obtain an Eilenberg-Moore algebra ˆ𝑎:𝐹★𝐴→𝐴as the free

extension of the identity morphism id𝐴:𝐴→𝐴.

The most familiar example of functor algebras are algebras over a signature. An algebraic signa-

ture consists of a set Σof operation symbols together with a map ar:Σ→Nassociating to every

operation symbol fits arity ar(f). Symbols of arity 0 are called constants. Every signature Σinduces

the polynomial set functor Ýf∈Σ(--)ar(f), which we denote by the same letter Σ. An algebra for the

functor Σthen is precisely an algebra for the signature Σ, i.e. a set 𝐴equipped with an operation

f𝐴:𝐴𝑛→𝐴for every 𝑛-ary operation symbol f∈Σ. Morphisms between Σ-algebras are maps

respecting the algebraic structure.

An equivalence relation ∼ ⊆ 𝐴×𝐴on a Σ-algebra 𝐴is called a congruence if, for every 𝑛-ary

operation symbol f∈Σand all elements 𝑎𝑖, 𝑏𝑖∈𝐴(𝑖=1, . . . , 𝑛), one has that

𝑎𝑖∼𝑏𝑖(𝑖=1, . . . , 𝑛)implies f𝐴(𝑎1, . . . , 𝑎𝑛) ∼ f𝐴(𝑏1, . . . , 𝑏𝑛).

Equivalently, there exists a morphism ℎ:𝐴→𝐵to some Σ-algebra 𝐵such that ∼equals the kernel

of ℎ, that is,

𝑎∼𝑏iﬀ ℎ(𝑎)=ℎ(𝑏).

Given a set 𝑋of variables, the free algebra Σ★𝑋is the Σ-algebra of terms generated by Σwith

variables from 𝑋. In particular, the free algebra on the empty set is the initial algebra 𝜇Σ; it is

formed by all closed terms of the signature. For every Σ-algebra (𝐴, 𝑎), the induced Eilenberg-

Moore algebra ˆ𝑎:Σ★𝐴→𝐴is given by the map evaluating terms over 𝐴in the algebra.

Coalgebras. Acoalgebra for an endofunctor 𝐹on Cis a pair (𝐶, 𝑐)of an object 𝐶(the carrier) and

a morphism 𝑐:𝐶→𝐹𝐶 (its structure). A morphism from an 𝐹-coalgebra (𝐶, 𝑐)to an 𝐹-coalgebra

(𝐷, 𝑑 )is a morphism ℎ:𝐶→𝐷of Csuch that 𝐹ℎ ·𝑐=𝑑·ℎ. Coalgebras for 𝐹and their mor-

phisms form a category Coalg(𝐹), and a ﬁnal 𝐹-coalgebra is a ﬁnal object in that category. If it

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

arXiv:2210.13387v2[cs.LO]26Oct20221TowardsaHigher-OrderMathematicalOperationalSemanticsSERGEYGONCHAROV,Friedrich-Alexander-UniversitätErlangen-Nürnberg,GermanySTEFANMILIUS∗,Friedrich-Alexander-UniversitätErlangen-Nürnberg,GermanyLUTZSCHRÖDER†,Friedrich-Alexander-UniversitätErlangen-Nürnberg,GermanyS...

展开>> 收起<<

Towards a Higher-Order Mathematical Operational Semantics.pdf

共37页,预览5页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Towards a Higher-Order Mathematical Operational Semantics

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: