-
The Mays and Musts of Concurrent Strategies
Authors:
Simon Castellan,
Pierre Clairambault,
Glynn Winskel
Abstract:
Concurrent strategies based on event structures are examined from the viewpoint of 'may' and 'must' testing in traditional process calculi. In their pure form concurrent strategies fail to expose the deadlocks and divergences that can arise in their composition. This motivates an extension of the bicategory of concurrent strategies to treat the 'may' and 'must' behaviour of strategies under testin…
▽ More
Concurrent strategies based on event structures are examined from the viewpoint of 'may' and 'must' testing in traditional process calculi. In their pure form concurrent strategies fail to expose the deadlocks and divergences that can arise in their composition. This motivates an extension of the bicategory of concurrent strategies to treat the 'may' and 'must' behaviour of strategies under testing. One extension adjoins neutral moves to strategies but in so doing loses identities w.r.t. composition. This in turn motivates another extension in which concurrent strategies are accompanied by stopping configurations; the ensuing stopping strategies inherit the structure of a bicategory from that of strategies. The technical developments converge in providing characterisations of the 'may' and 'must' equivalences and preorders on strategies.
△ Less
Submitted 24 August, 2021;
originally announced August 2021.
-
Assessing perceived organizational leadership styles through twitter text mining
Authors:
A. La Bella,
A. Fronzetti Colladon,
E. Battistoni,
S. Castellan,
M. Francucci
Abstract:
We propose a text classification tool based on support vector machines for the assessment of organizational leadership styles, as appearing to Twitter users. We collected Twitter data over 51 days, related to the first 30 Italian organizations in the 2015 ranking of Forbes Global 2000-out of which we selected the five with the most relevant volumes of tweets. We analyzed the communication of the c…
▽ More
We propose a text classification tool based on support vector machines for the assessment of organizational leadership styles, as appearing to Twitter users. We collected Twitter data over 51 days, related to the first 30 Italian organizations in the 2015 ranking of Forbes Global 2000-out of which we selected the five with the most relevant volumes of tweets. We analyzed the communication of the company leaders, together with the dialogue among the stakeholders of each company, to understand the association with perceived leadership styles and dimensions. To assess leadership profiles, we referred to the 10-factor model developed by Barchiesi and La Bella in 2007. We maintain the distinctiveness of the approach we propose, as it allows a rapid assessment of the perceived leadership capabilities of an enterprise, as they emerge from its social media interactions. It can also be used to show how companies respond and manage their communication when specific events take place, and to assess their stakeholder's reactions.
△ Less
Submitted 24 May, 2021;
originally announced May 2021.
-
Disentangling Parallelism and Interference in Game Semantics
Authors:
Simon Castellan,
Pierre Clairambault
Abstract:
Game semantics is a denotational semantics presenting compositionally the computational behaviour of various kinds of effectful programs. One of its celebrated achievement is to have obtained full abstraction results for programming languages with a variety of computational effects, in a single framework. This is known as the semantic cube or Abramsky's cube, which for sequential deterministic pro…
▽ More
Game semantics is a denotational semantics presenting compositionally the computational behaviour of various kinds of effectful programs. One of its celebrated achievement is to have obtained full abstraction results for programming languages with a variety of computational effects, in a single framework. This is known as the semantic cube or Abramsky's cube, which for sequential deterministic programs establishes a correspondence between certain conditions on strategies (''innocence'', ''well-bracketing'', ''visibility'') and the absence of matching computational effects. Outside of the sequential deterministic realm, there are still a wealth of game semantics-based full abstraction results; but they no longer fit in a unified canvas. In particular, Ghica and Murawski's fully abstract model for shared state concurrency (IA) does not have a matching notion of pure parallel program-we say that parallelism and interference (i.e. state plus semaphores) are entangled. In this paper we construct a causal version of Ghica and Murawski's model, also fully abstract for IA. We provide compositional conditions parallel innocence and sequentiality, respectively banning interference and parallelism, and leading to four full abstraction results. To our knowledge, this is the first extension of Abramsky's semantic cube programme beyond the sequential deterministic world.
△ Less
Submitted 17 September, 2024; v1 submitted 29 March, 2021;
originally announced March 2021.
-
Game Semantics: Easy as Pi
Authors:
Nobuko Yoshida,
Simon Castellan,
Léo Stefanesco
Abstract:
Game semantics has proven to be a robust method to give compositional semantics for a variety of higher-order programming languages. However, due to the complexity of most game models, game semantics has remained unapproachable for non-experts.
In this paper, we aim at making game semantics more accessible by viewing it as a syntactic translation into a session typed pi-calculus, referred to as…
▽ More
Game semantics has proven to be a robust method to give compositional semantics for a variety of higher-order programming languages. However, due to the complexity of most game models, game semantics has remained unapproachable for non-experts.
In this paper, we aim at making game semantics more accessible by viewing it as a syntactic translation into a session typed pi-calculus, referred to as metalanguage, followed by a semantics interpretation of the metalanguage into a particular game model. The syntactic translation can be defined for a wide range of programming languages without knowledge of the particular game model used. Simple reasoning on the model (soundness, and adequacy) can be done at the level of the metalanguage, escaping tedious technical proofs usually found in game semantics. We call this methodology programming game semantics.
We design a metalanguage (PiDiLL) inspired from Differential Linear Logic (DiLL), which is concise but expressive enough to support features required by concurrent game semantics. We then demonstrate our methodology by yielding the first causal, non-angelic and interactive game model of CML, a higher-order call-by-value language with shared memory concurrency. We translate CML into PiDiLL and show that the translation is adequate. We give a causal and non-angelic game semantics model using event structures, which supports a simple semantics interpretation of PiDiLL. Combining both of these results, we obtain the first interactive model of a concurrent language of this expressivity which is adequate with respect to the standard weak bisimulation, and fully abstract for the contextual equivalence on second-order terms.
We have implemented a prototype which can explore the generated causal object from a subset of OCaml.
△ Less
Submitted 10 November, 2020;
originally announced November 2020.
-
Categories with Families: Unityped, Simply Typed, and Dependently Typed
Authors:
Simon Castellan,
Pierre Clairambault,
Peter Dybjer
Abstract:
We show how the categorical logic of untyped, simply typed and dependently typed lambda calculus can be structured around the notion of category with family (cwf). To this end we introduce subcategories of simply typed cwfs (scwfs), where types do not depend on variables, and unityped cwfs (ucwfs), where there is only one type. We prove several equivalence and biequivalence theorems between cwf-ba…
▽ More
We show how the categorical logic of untyped, simply typed and dependently typed lambda calculus can be structured around the notion of category with family (cwf). To this end we introduce subcategories of simply typed cwfs (scwfs), where types do not depend on variables, and unityped cwfs (ucwfs), where there is only one type. We prove several equivalence and biequivalence theorems between cwf-based notions and basic notions of categorical logic, such as cartesian operads, Lawvere theories, categories with finite products and limits, cartesian closed categories, and locally cartesian closed categories. Some of these theorems depend on the restrictions of contextuality (in the sense of Cartmell) or democracy (used by Clairambault and Dybjer for their biequivalence theorems). Some theorems are equivalences between notions with strict preservation of chosen structure. Others are biequivalences between notions where properties are only preserved up to isomorphism. In addition to this we discuss various constructions of initial ucwfs, scwfs, and cwfs with extra structure.
△ Less
Submitted 7 July, 2020; v1 submitted 1 April, 2019;
originally announced April 2019.
-
Games and Strategies as Event Structures
Authors:
Simon Castellan,
Pierre Clairambault,
Silvain Rideau,
Glynn Winskel
Abstract:
In 2011, Rideau and Winskel introduced concurrent games and strategies as event structures, generalizing prior work on causal formulations of games. In this paper we give a detailed, self-contained and slightly-updated account of the results of Rideau and Winskel: a notion of pre-strategy based on event structures; a characterisation of those pre-strategies (deemed strategies) which are preserved…
▽ More
In 2011, Rideau and Winskel introduced concurrent games and strategies as event structures, generalizing prior work on causal formulations of games. In this paper we give a detailed, self-contained and slightly-updated account of the results of Rideau and Winskel: a notion of pre-strategy based on event structures; a characterisation of those pre-strategies (deemed strategies) which are preserved by composition with a copycat strategy; and the construction of a bicategory of these strategies. Furthermore, we prove that the corresponding category has a compact closed structure, and hence forms the basis for the semantics of concurrent higher-order computation.
△ Less
Submitted 27 September, 2017; v1 submitted 15 April, 2016;
originally announced April 2016.
-
Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version)
Authors:
Simon Castellan,
Pierre Clairambault,
Peter Dybjer
Abstract:
We show that a version of Martin-Löf type theory with an extensional identity type former I, a unit type N1 , Sigma-types, Pi-types, and a base type is a free category with families (supporting these type formers) both in a 1- and a 2-categorical sense. It follows that the underlying category of contexts is a free locally cartesian closed category in a 2-categorical sense because of a previously p…
▽ More
We show that a version of Martin-Löf type theory with an extensional identity type former I, a unit type N1 , Sigma-types, Pi-types, and a base type is a free category with families (supporting these type formers) both in a 1- and a 2-categorical sense. It follows that the underlying category of contexts is a free locally cartesian closed category in a 2-categorical sense because of a previously proved biequivalence. We show that equality in this category is undecidable by reducing it to the undecidability of convertibility in combinatory logic. Essentially the same construction also shows a slightly strengthened form of the result that equality in extensional Martin-Löf type theory with one universe is undecidable.
△ Less
Submitted 28 November, 2017; v1 submitted 15 April, 2015;
originally announced April 2015.
-
Thin Games with Symmetry and Concurrent Hyland-Ong Games
Authors:
Simon Castellan,
Pierre Clairambault,
Glynn Winskel
Abstract:
We build a cartesian closed category, called Cho, based on event structures. It allows an interpretation of higher-order stateful concurrent programs that is refined and precise: on the one hand it is conservative with respect to standard Hyland-Ong games when interpreting purely functional programs as innocent strategies, while on the other hand it is much more expressive. The interpretation of p…
▽ More
We build a cartesian closed category, called Cho, based on event structures. It allows an interpretation of higher-order stateful concurrent programs that is refined and precise: on the one hand it is conservative with respect to standard Hyland-Ong games when interpreting purely functional programs as innocent strategies, while on the other hand it is much more expressive. The interpretation of programs constructs compositionally a representation of their execution that exhibits causal dependencies and remembers the points of non-deterministic branching.The construction is in two stages. First, we build a compact closed category Tcg. It is a variant of Rideau and Winskel's category CG, with the difference that games and strategies in Tcg are equipped with symmetry to express that certain events are essentially the same. This is analogous to the underlying category of AJM games enriching simple games with an equivalence relations on plays. Building on this category, we construct the cartesian closed category Cho as having as objects the standard arenas of Hyland-Ong games, with strategies, represented by certain events structures, playing on games with symmetry obtained as expanded forms of these arenas.To illustrate and give an operational light on these constructions, we interpret (a close variant of) Idealized Parallel Algol in Cho.
△ Less
Submitted 1 March, 2019; v1 submitted 26 September, 2014;
originally announced September 2014.
