the semantics of logics is based on valuations that map variables to values, while programming languages cannot store complex values atomically. they have a pointer semantics where complex data is stored on the heap, ...
详细信息
ISBN:
(纸本)9783031765537;9783031765544
the semantics of logics is based on valuations that map variables to values, while programming languages cannot store complex values atomically. they have a pointer semantics where complex data is stored on the heap, linked with pointers. the standard approach to bridge the semantic gap between algebraic specifications and executable programs is to translate algebraic data types, recursive definitions and programs to functional code with immutable data types. Since functional programs are often less efficient than C programs due to the lack (or limited use) of mutation and the requirement of using garbage collection, we develop a different approach in this paper that is based on always mutating data structures but keeping different ones disjoint. the approach generates efficient C programs from the specifications, which have a pointer semantics and explicitly allocate and free memory on the heap. Formal specifications are given for the semantics of a core source and target language that allow to demonstrate the main transformations necessary and prove their correctness. the approach has been implemented for the full language and produces working C code.
Finite maps or finite relations between infinite sets do not even form a category, since the necessary identities are not finite. We show relation-algebraic extensions of semigroupoids where the operations that would ...
详细信息
Finite maps or finite relations between infinite sets do not even form a category, since the necessary identities are not finite. We show relation-algebraic extensions of semigroupoids where the operations that would produce infinite results have been replaced with variants that preserve finiteness, but still satisfy useful algebraic laws. the resulting theories allow calculational reasoning in the relation-algebraic style with only minor sacrifices;our emphasis on generality even provides some concepts in theories where they had not been available before. the semigroupoid theories presented in this paper also can directly guide library interface design and thus be used for principled relation-algebraicprogramming;an example implementation in Haskell allows manipulating finite binary relations as data in a point-free relation-algebraicprogramming style that integrates naturally withthe current Haskell collection types. this approach enables seamless integration of relation-algebraic formulations to provide elegant solutions of problems that, with different data organisation, are awkward to tackle. (C) 2007 Elsevier Inc. All rights reserved.
We present an algebraic embedding of Neighbourhood logic (NL) into the framework of semirings which yields various simplifications. For example, some of the NL axioms can be dropped, since they are theorems in our fra...
详细信息
We present an algebraic embedding of Neighbourhood logic (NL) into the framework of semirings which yields various simplifications. For example, some of the NL axioms can be dropped, since they are theorems in our framework, and Galois connections produce properties for free. A further simplification is achieved, since the semiring methods used are easy and fairly standard. Moreover, this embedding allows us to reuse knowledge from Neighbourhood logic in other areas of Computer Science. Since in its original axiomatisation the logic cannot handle intervals of infinite length and therefore not fully model and specify reactive and hybrid systems, using lazy semirings we introduce an extension of NL to intervals of finite and infinite length. Furthermore, we discuss connections between the (extended) logic and other application areas, like Allen's thirteen relations between intervals, the branching time temporal logic CTL* and hybrid systems. (C) 2007 Elsevier Inc. All rights reserved.
We explore the power of relational semantics and equational reasoning in the style of Kleene algebra for analyzing programs with mutable, statically scoped local variables. We provide (i) a fully compositional relatio...
详细信息
We explore the power of relational semantics and equational reasoning in the style of Kleene algebra for analyzing programs with mutable, statically scoped local variables. We provide (i) a fully compositional relational semantics for a first-order programming language with constructs for local variable declaration and destructive update;and (ii) an equational proof system based on Kleene algebra with tests for proving the equivalence of programs in this language. We show that the proof system is sound and complete relative to the underlying equational theory without local variables. We illustrate the use of the system with several examples. (C) 2007 Elsevier Inc. All rights reserved.
the theory of cut-free sequent proofs has been used to motivate and justify the design of a number of logicprogramming languages. Two such languages, lambda Prolog and its linear logic refinement, Lolli [15], provide...
详细信息
the theory of cut-free sequent proofs has been used to motivate and justify the design of a number of logicprogramming languages. Two such languages, lambda Prolog and its linear logic refinement, Lolli [15], provide for various forms of abstraction (modules, abstract data types, and higher-order programming) but lack primitives for concurrency. the logicprogramming language, LO (Linear Objects) [2] provides some primitives for concurrency but lacks abstraction mechanisms. In this paper we present Forum, a logicprogramming presentation of all of linear logicthat modularly extends lambda Prolog, Lolli, and LO. Forum, therefore, allows specifications to incorporate both abstractions and concurrency. To illustrate the new expressive strengths of Forum, we specify in it a sequent calculus proof system and the operational semantics of a programming language that incorporates references and concurrency. We also show that the meta theory of linear logic can be used to prove properties of the object-languages specified in Forum.
In this paper, we propose a three-valued completion semantics for abductive logic programs, which solves some problems associated withthe Console et al. two-valued completion semantics. the semantics is a generalizat...
详细信息
In this paper, we propose a three-valued completion semantics for abductive logic programs, which solves some problems associated withthe Console et al. two-valued completion semantics. the semantics is a generalization of Kunen's completion semantics for general logic programs, which is known to correspond very well to a class of effective proof procedures for general logic programs. Secondly, we propose a proof procedure for abductive logic programs, which is a generalization of a proof procedure for general logic programs based on constructive negation. this proof procedure is sound and complete with respect to the proposed semantics. By generalizing a number of results on general logic programs to the class of abductive logic programs, we present further evidence for the idea that limited forms of abduction can be added quite naturally to general logic programs.
We investigate the use of multilattices as the set of truth-values underlying a general fuzzy logicprogramming framework. On the one hand, some theoretical results about ideals of a multilattice are presented in orde...
详细信息
We investigate the use of multilattices as the set of truth-values underlying a general fuzzy logicprogramming framework. On the one hand, some theoretical results about ideals of a multilattice are presented in order to provide an ideal-based semantics;on the other hand, a restricted semantics, in which interpretations assign elements of a multilattice to each propositional symbol, is presented and analysed. (C) 2006 Elsevier B.V. All rights reserved.
We investigate the modularity behavior of termination and confluence properties of (join) conditional term rewriting systems. We give counterexamples showing that the properties weak termination, weak innermost termin...
详细信息
We investigate the modularity behavior of termination and confluence properties of (join) conditional term rewriting systems. We give counterexamples showing that the properties weak termination, weak innermost termination and (strong) innermost termination are not preserved in general under signature extensions. then we develop sufficient conditions for the preservation of these properties under signature extensions, and more generally, for their modularity in the disjoint union case. this leads to new criteria for modularity of termination and completeness generalizing known results for unconditional systems. Finally, combining our analysis with recent related results on the preservation of semi-completeness, we show how to cover the (non-disjoint) case of combined conditional rewrite systems with shared constructors too.
Data distribution algebras are an abstract notion for the description of parallel programs. their dynamic execution can be optimized if they are shapely. In this paper we describe a shape analysis which allows compile...
详细信息
Data distribution algebras are an abstract notion for the description of parallel programs. their dynamic execution can be optimized if they are shapely. In this paper we describe a shape analysis which allows compile-time shapeliness-tests. It operates on the structure of algebraic data types and works for arbitrary functional programs rather than only shapely ones. Besides a first-order calculus we also propose a higher-order version which can handle higher-order functions as well. (C) 2000 Elsevier Science B.V. All rights reserved.
暂无评论