NESTED GUARDED HORN CLAUSES

1990 ◽  
Vol 01 (03) ◽  
pp. 249-263 ◽  
Author(s):  
MORENO FALASCHI ◽  
MAURIZIO GABBRIELLI ◽  
GIORGIO LEVI ◽  
MASAKI MURAKAMI
Keyword(s):  
Logic Programming ◽  
Operational Semantics ◽  
Horn Clauses ◽  
Fixpoint Semantics ◽  
New Feature ◽  
Definition Of

This paper defines a new concurrent logic language, Nested Guarded Horn Clauses (NGHC). The main new feature of the language is its concept of guard. In fact, an NGHC clause has several layers of (standard) guards. This syntactic innovation allows the definition of a complete (i.e. always applicable) set of unfolding rules and therefore of an unfolding semantics which is equivalent, with respect to the success set, to the operational semantics. A fixpoint semantics is also defined in the classic logic programming style and is proved equivalent to the unfolding one. Since it is possible to embed Flat GHC into NGHC, our method can be used to give a fixpoint semantics to FGHC as well.

scholarly journals From Interpreter to Logic Engine by Defunctionalization

2003 ◽  
Vol 10 (25) ◽  
Author(s):  
Dariusz Biernacki ◽  
Olivier Danvy
Keyword(s):  
Logic Programming ◽  
Programming Language ◽  
Operational Semantics ◽  
Lambda Calculus ◽  
Transition System ◽  
Abstract Machine ◽  
Logic Programming Language ◽  
Delimited Continuations ◽  
Simple Logic ◽  
Control Operators

Starting from a continuation-based interpreter for a simple logic programming language, propositional Prolog with cut, we derive the corresponding logic engine in the form of an abstract machine. The derivation originates in previous work (our article at PPDP 2003) where it was applied to the lambda-calculus. The key transformation here is Reynolds's defunctionalization that transforms a tail-recursive, continuation-passing interpreter into a transition system, i.e., an abstract machine. Similar denotational and operational semantics were studied by de Bruin and de Vink in previous work (their article at TAPSOFT 1989), and we compare their study with our derivation. Additionally, we present a direct-style interpreter of propositional Prolog expressed with control operators for delimited continuations.<br /><br />Superseded by BRICS-RS-04-5.

A specification logic for concurrent object-oriented programming

1999 ◽  
Vol 9 (3) ◽  
pp. 253-286 ◽  
Author(s):  
G. DELZANNO ◽  
D. GALMICHE ◽  
M. MARTELLI
Keyword(s):  
Logic Programming ◽  
Programming Languages ◽  
Linear Logic ◽  
Operational Semantics ◽  
Object Oriented ◽  
Object Oriented Programming ◽  
Higher Order Logic ◽  
Specification Logic ◽  
Theoretic Characterization

This paper focuses on the use of linear logic as a specification language for the operational semantics of advanced concepts of programming such as concurrency and object-orientation. Our approach is based on a refinement of linear logic sequent calculi based on the proof-theoretic characterization of logic programming. A well-founded combination of higher-order logic programming and linear logic will be used to give an accurate encoding of the traditional features of concurrent object-oriented programming languages, whose corner-stone is the notion of encapsulation.

scholarly journals Constraint functional logic programming over finite domains

2007 ◽  
Vol 7 (5) ◽  
pp. 537-582 ◽  
Author(s):  
ANTONIO J. FERNÁNDEZ ◽  
TERESA HORTALÁ-GONZÁLEZ ◽  
FERNANDO SÁENZ-PÉREZ ◽  
RAFAEL DEL VADO-VÍRSEDA
Keyword(s):  
Logic Programming ◽  
Operational Semantics ◽  
Point Of View ◽  
Finite Domain ◽  
Lazy Evaluation ◽  
Functional Logic Programming ◽  
Functional Logic ◽  
Finite Domains ◽  
Higher Order Functions ◽  
Domain Constraints

AbstractIn this paper, we present our proposal to Constraint Functional Logic Programming over Finite Domains (CFLP($\fd$)) with a lazy functional logic programming language which seamlessly embodies finite domain ($\fd$) constraints. This proposal increases the expressiveness and power of constraint logic programming over finite domains (CLP($\fd$)) by combining functional and relational notation, curried expressions, higher-order functions, patterns, partial applications, non-determinism, lazy evaluation, logical variables, types, domain variables, constraint composition, and finite domain constraints. We describe the syntax of the language, its type discipline, and its declarative and operational semantics. We also describe\toy(fd)$, an implementation forCFLP($\fd$), and a comparison of our approach with respect toCLP($\fd$) from a programming point of view, showing the new features we introduce. And, finally, we show a performance analysis which demonstrates that our implementation is competitive with respect to existingCLP($\fd$) systems and that clearly outperforms the closer approach toCFLP($\fd$).

scholarly journals Natural Quantum Operational Semantics with Predicates

2008 ◽  
Vol 18 (3) ◽  
pp. 341-359 ◽  
Author(s):  
Marek Sawerwain ◽  
Roman Gielerak
Keyword(s):  
Positive Operator ◽  
Operational Semantics ◽  
General Definition ◽  
Completely Positive Maps ◽  
Transition Systems ◽  
Positive Operator Valued Measures ◽  
Labelled Transition Systems ◽  
Positive Maps ◽  
Definition Of ◽  
Positive Operator Valued Measure

Natural Quantum Operational Semantics with PredicatesA general definition of a quantum predicate and quantum labelled transition systems for finite quantum computation systems is presented. The notion of a quantum predicate as a positive operator-valued measure is developed. The main results of this paper are a theorem about the existence of generalised predicates for quantum programs defined as completely positive maps and a theorem about the existence of a GSOS format for quantum labelled transition systems. The first theorem is a slight generalisation of D'Hondt and Panagaden's theorem about the quantum weakest precondition in terms of discrete support positive operator-valued measures.

scholarly journals ε-TPN: definition of a Time Petri Net formalism simulating the behaviour of the timed grafcets

2019 ◽  
Vol Volume 31 - 2019 - CARI 2018 ◽  
Author(s):  
Médésu Sogbohossou ◽  
Medesu Sogbohossou ◽  
Antoine Vianou ◽  
Nabil Gmati ◽  
Eric Badouel ◽  
...  
Keyword(s):  
Petri Nets ◽  
Control Systems ◽  
Timed Automata ◽  
Operational Semantics ◽  
Formal Modeling ◽  
Time Petri Nets ◽  
Time Petri Net ◽  
Finite State ◽  
Definition Of ◽  
Finite State Space

To allow a formal verification of timed GRAFCET models, many authors proposed to translate them into formal and well-reputed languages such as timed automata or Time Petri nets (TPN). Thus, the work presented in [Sogbohossou, Vianou, Formal modeling of grafcets with Time Petri nets, IEEE Transactions on Control Systems Technology, 23(5)(2015)] concerns the TPN formalism: the resulting TPN of the translation, called here ε-TPN, integrates some infinitesimal delays (ε) to simulate the synchronous semantics of the grafcet. The first goal of this paper is to specify a formal operational semantics for an ε-TPN to amend the previous one: especially, priority is introduced here between two defined categories of the ε-TPN transitions, in order to respect strictly the synchronous hypothesis. The second goal is to provide how to build the finite state space abstraction resulting from the new definitions. Afin de permettre la vérification formelle des grafcets temporisés, plusieurs auteurs ont proposé de les traduire dans des langages formels de réputation tels que les automates temporisés et les réseaux de Petri temporels (TPN). Ainsi, les travaux présentés dans [Sogbohossou, Vianou, Formal modeling of grafcets with Time Petri nets, IEEE Transactions on Control Systems Technology, 23(5)(2015)] concernent le formalisme des TPN: le réseau résultant de la traduction, dénommé ici ε-TPN, intègre des délais infinitésimaux (ε) pour simuler la sémantique synchrone du grafcet. Le premier objectif de cet article est de définir la sémantique opérationnelle d'un ε-TPN afin d'améliorer l'ancienne définition: spécifiquement, une priorité est introduite ici entre deux catégories de transitions définies pour ces réseaux, dans l'optique de respecter rigoureusement l'hypothèse synchrone. Le second but est de fournir une méthode de calcul de l'espace d'état fini qui découle des nouvelles définitions.

Sign in / Sign up

Export Citation Format

Share Document