Wyniki wyszukiwania - BazTech

1

Concurrency Semantics in Continuation-Passing Style

Todoran E. N., Papaspyrou N.

Fundamenta Informaticae

|

2017

|

Vol. 153, nr 1/2

125--146

EN

We present a denotational semantics designed in continuation-passing style (CPS) for an abstract language providing operators for nondeterministic choice, sequential and parallel composition, and a general mechanism of interaction between multisets of distributed actions. We show that the basic laws of concurrent systems are satisfied in this semantics. Next, by customizing the behavior of continuations we obtain denotational semantics for a couple of concurrent languages and a nature-inspired formalism. The languages discussed include Hoare's communicating sequential processes (CSP), and two formalisms based on multiparty interactions: a version of CSP extended with communication and synchronization on multiple channels, and a language similar to a process algebra for DNA computing introduced by Cardelli. We accomplish the semantic investigation in the mathematical framework of complete metric spaces.

2

A Theoretical Perspective of Coinductive Logic Programming

Ancona D., Dovier A.

Fundamenta Informaticae

|

2015

|

Vol. 140, nr 3/4

221--246

EN

In this paper we study the semantics of Coinductive Logic Programming and clarify its intrinsic computational limits, which prevent, in particular, the definition of a complete, computable, operational semantics. We propose a new operational semantics that allows a simple correctness result and the definition of a simple meta-interpreter. We compare, and prove the equivalence, with the operational semantics defined and used in other papers on this topic.

3

Stochastic Petri Box Calculus with Discrete Time

Tarasyuk I.V.

Fundamenta Informaticae

|

2007

|

Vol. 76, nr 1-2

189-218

EN

In the last decades, a number of stochastic enrichments of process algebras was constructed to allow one for specification of stochastic processes within the well-developed framework of algebraic calculi. In [], a continuous time stochastic extension of finite Petri box calculus (PBC) was proposed called sPBC. The algebra sPBC has interleaving semantics due to the properties of continuous time distributions. At the same time, PBC has step semantics, and it could be natural to propose its concurrent stochastic enrichment. We construct a discrete time stochastic extension dtsPBC of finite PBC. A step operational semantics is defined in terms of labeled transition systems based on action and inaction rules. A denotational semantics is defined in terms of a subclass of labeled discrete time stochastic Petri nets (LDTSPNs) called discrete time stochastic Petri boxes (dts-boxes). A consistency of both semantics is demonstrated. In addition, we define a variety of probabilistic equivalences that allow one to identify stochastic processes with similar behaviour which are differentiated by too strict notion of the semantic equivalence. The interrelations of all the introduced equivalences are investigated.

4

The Impact of seq on Free Theorems-Based Program Transformations

Johann P., Voigtländer J.

Fundamenta Informaticae

|

2006

|

Vol. 69, nr 1,2

63-102

EN

Parametric polymorphism constrains the behavior of pure functional programs in a way that allows the derivation of interesting theorems about them solely from their types, i.e., virtually for free. Unfortunately, standard parametricity results - including so-called free theorems - fail for nonstrict languages supporting a polymorphic strict evaluation primitive such as Haskell's seq. A folk theorem maintains that such results hold for a subset of Haskell corresponding to a Girard-Reynolds calculus with fixpoints and algebraic datatypes even when seq is present provided the relations which appear in their derivations are required to be bottom-reflecting and admissible. In this paper we show that this folklore is incorrect, but that parametricity results can be recovered in the presence of seq by restricting attention to left-closed, total, and admissible relations instead. The key novelty of our approach is the asymmetry introduced by left-closedness, which leads to ``inequational'' versions of standard parametricity results together with preconditions guaranteeing their validity even when seq is present. We use these results to derive criteria ensuring that both equational and inequational versions of short cut fusion and related program transformations based on free theorems hold in the presence of seq.

5

Full abstrctness of a metric semantics for action refinement

Hartog J.I. den, Vink E.P. de, Bakker J.W. de

Fundamenta Informaticae

|

1999

|

Vol. 40, Nr 4

335-382

EN

For a process language with action refinement and synchronization both an operational and a denotational semantics are given. The operational semantics is based on an SOS-style transition system specification involving syntactical refinement sequences. The denotational semantics is an interleaving model which uses semantical refinement `environments'. It identifies those statements which are equal under all refinements. The denotational model is shown to be fully abstract with respect to the operational one. The underlying metric machinery is exploited to obtain this full abstractness result. Usually, action refinement is treated either in a model with some form of true concurrency, or, when an interleaving model is applied, by assuming that the refining statements are atomized. We argue that an interleaving model without such atomization is attractive as well.