اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدA fully-abstract semantics of lambda-mu in the pi-calculus
235
0
0.0
(
0
)
تأليف
Steffen van Bakel
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
We study the lambda-mu-calculus, extended with explicit substitution, and define a compositional output-based interpretation into a variant of the pi-calculus with pairing that preserves single-step explicit head reduction with respect to weak bisimilarity. We define four notions of weak equivalence for lambda-mu -- one based on weak reduction, two modelling weak head-reduction and weak explicit head reduction (all considering terms without weak head-normal form equivalent as well), and one based on weak approximation -- and show they all coincide. We will then show full abstraction results for our interpretation for the weak equivalences with respect to weak bisimilarity on processes.
قيم البحث
اقرأ أيضاً
We define sound and adequate denotational and operational semantics for the stochastic lambda calculus. These two semantic approaches build on previous work that used similar techniques to reason about higher-order probabilistic programs, but for the
first time admit an adequacy theorem relating the operational and denotational views. This resolves the main issue left open in (Bacci et al. 2018).
This paper provides a fully abstract semantics for value-passing CCS for trees (VCCTS). The operational semantics is given both in terms of a reduction semantics and in terms of a labelled transition semantics. The labelled transition semantics is no
n-sequential, allowing more than one action occurring simultaneously. We develop the theory of behavioral equivalence by introducing both weak barbed congruence and weak bisimilarity. In particular, we show that weak barbed congruence coincides with weak bisimilarity on image-finite processes. This is the first such result for a concurrent model with tree structures. Distributed systems can be naturally modeled by means of this graph-based system, and some examples are given to illustrate this.
We define a semantics for Milners pi-calculus, with three main novelties. First, it provides a fully-abstract model for fair testing equivalence, whereas previous semantics covered variants of bisimilarity and the may and must testing equivalences. S
econd, it is based on reduction semantics, whereas previous semantics were based on labelled transition systems. Finally, it has a strong game semantical flavor in the sense of Hyland-Ong and Nickau. Indeed, our model may both be viewed as an innocent presheaf semantics and as a concurrent game semantics.
We present Hypersequent Classical Processes (HCP), a revised interpretation of the Proofs as Processes correspondence between linear logic and the {pi}-calculus initially proposed by Abramsky [1994], and later developed by Bellin and Scott [1994], Ca
ires and Pfenning [2010], and Wadler [2014], among others. HCP mends the discrepancies between linear logic and the syntax and observable semantics of parallel composition in the {pi}-calculus, by conservatively extending linear logic to hyperenvironments (collections of environments, inspired by the hypersequents by Avron [1991]). Separation of environments in hyperenvironments is internalised by $otimes$ and corresponds to parallel process behaviour. Thanks to this property, for the first time we are able to extract a labelled transition system (lts) semantics from proof rewritings. Leveraging the information on parallelism at the level of types, we obtain a logical reconstruction of the delayed actions that Merro and Sangiorgi [2004] formulated to model non-blocking I/O in the {pi}-calculus. We define a denotational semantics for processes based on Brzozowski derivatives, and uncover that non-interference in HCP corresponds to Fubinis theorem of double antiderivation. Having an lts allows us to validate HCP using the standard toolbox of behavioural theory. We instantiate bisimilarity and barbed congruence for HCP, and obtain a full abstraction result: bisimilarity, denotational equivalence, and barbed congruence coincide.
We develop a categorical compositional distributional semantics for Lambek Calculus with a Relevant Modality, which has a limited version of the contraction and permutation rules. The categorical part of the semantics is a monoidal biclosed category
with a coalgebra modality as defined on Differential Categories. We instantiate this category to finite dimensional vector spaces and linear maps via quantisation functors and work with three concrete interpretations of the coalgebra modality. We apply the model to construct categorical and concrete semantic interpretations for the motivating example of this extended calculus: the derivation of a phrase with a parasitic gap. The effectiveness of the concrete interpretations are evaluated via a disambiguation task, on an extension of a sentence disambiguation dataset to parasitic gap phrases, using BERT, Word2Vec, and FastText vectors and Relational tensors
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
