Operational and goal-independent denotational semantics for Prolog with cut

In this paper we propose an operational and a denotational semantics for Prolog. We deal with the control rules of Prolog and the cut operator. Our denotational semantics provides a goal-independent semantics. This means that the behaviour of a goal in a program is defined as the evaluation of the goal in the denotation (semantics) of the program. We show how our denotational semantics can be specialised into a computed answer semantics and into a call pattern semantics. Our work provides a basis for a precise abstract interpretation of Prolog programs.     

On Modeling Coordination via Asynchronous Communication and Enhanced Matching

The paper proposes a theoretical study of a coordination language embodying Linda's asynchronous communication primitive with a refined matching mechanism based on pairs composed of attribute names associated with their values. Computations in this language are described by means of an operational semantics, reporting the whole traces of executions. The non-compositionality of this intuitive operational semantics motivates the design of a compositional and fully abstract denotational semantics, which is then exploited for studying program equivalence in this setting.     

Non-deterministic data types: models and implementations

Summary The model theoretic basis for (abstract) data types is generalized from algebras to multi-algebr as in order to cope with non-deterministic operations. A programming oriented definition and a model theoretic criterion (called simulation) for implementation of data types are given. To justify the criterion w.r.t. the definition, an abstract framework linking denotational semantics of programming languages and model theory of data types is set up. A set of constraints on a programming language semantics are derived which guarantee that simulation implies implementation. It is argued that any language supporting data abstraction does fulfill these constraints. As an example a simple but expressive language L is defined and it is formally proved that L does conform to these restrictions.     

Full Abstraction for a Shared-Variable Parallel Language

We give a new denotational semantics for a shared-variable parallel programming language and prove full abstraction: the semantics gives identical meanings to commands if and only if they induce the same behavior in all program contexts. The meaning of a command is a set of “transition traces,” which record the ways in which a command may interact with and be affected by its environment. We show how to modify the semantics to incorporate new program constructs, to allow for different levels of granularity or atomicity, and to model fair infinite computation, in each case achieving full abstraction with respect to an appropriate notion of program behavior.     

Sequential algorithms on concrete data structures

We provide a sequential denotational semantics for sequential programming languages, based on a new notion of sequential algorithm on the Kahn-Plotkin concrete data structures. Intuitively an algorithm may be seen either as a concrete object—a “program” in a simple output-driven language — or as an abstract object — the pair of a sequential function and of a computation strategy for it. The concrete and abstract presentations are equivalent, as shown by a representation theorem. The algorithms form a cartesian closed category with straightforward solutions to recursive domain equations. Hence they may replace functions in the denotational semantics of any sequential language. An applicative programming language based on sequential algorithms is presented in a companion paper.     

Can LCF be topped? Flat lattice models of typed λ-calculus

Plotkin ((1977) Theoret. Comput. Sci. 5: 223–256) examines the denotational semantics of PCF (essentially typed λ-calculus with arithmetic and looping). The standard Scott semantics V is computationally adequate but not fully abstract; with the addition of some parallel facilities, it becomes fully abstract, and with the addition of an existential operator, denotationally universal. We consider carrying out the same program for , the Scott models built from flat lattices rather than flat cpo's. Surprisingly, no computable extension of PCF can be denotationally universal; perfectly reasonable semantic values such as supremum and Plotkin's “parallel or” cannot be definable. There is an unenlightening fully abstract extension _A (approx), based on Gödel numbering and syntactic analysis. Unfortunately, this is the best we can do; operators defined by PCF-style rules cannot give a fully abstract language. (There is a natural and desirable property, operational extensionality, which prevents full abstraction with respect to .) However, we show that Plotkin's program can be carried out for a nonconfluent evaluator.     

Denotational semantics of a para-functional programming language

Apara-functional programming language is a functional language that has been extended with special annotations that provide an extra degree of control over parallel evaluation. Of most interest are annotations that allow one to express the dynamic mapping of a program onto a known multiprocessor topology. Since it is quite desirable to provide a precise semantics for any programming language, in this paper adenotational semantics is given for a simple para-functional programming language with mapping annotations. A precise meaning is given not only to the normalfunctional behavior of the program (i.e., the answer), but also to theoperational notion of where (i.e., on what processor) expressions are evaluated. The latter semantics is accomplished through an abstract entity called anexecution tree.This research was supported in part by the National Science Foundation under Grants DCR-8403304 and DCR-8451415, and the Department of Energy under Grant DE-FG02-86ER25012.     

The semantics of the combination of atomized statements and parallel choice

In this paper we define a uniform language that is an extension of the language underlying the process algebraPA. One of the main extensions of this language overPA is given by so-called atomizing brackets. If we place these brackets around a statement then we treat this statement as an atomic action. Put differently, these brackets remove all interleaving points. We present a transition system for the language and derive its operational semantics. We show that there are several options for defining a transition system such that the resulting operational semantics is a conservative extension of the semantics forPA. We define a semantic domain and a denotational model for the language. Next we define a closure operator on the semantic domain and show how to use this closure operator to derive a fully abstract denotational semantics. Then the algebraic theory of the language is considered. We define a collection of axioms and a term rewrite system based on these axioms. Using this term rewrite system we are able to identify normal forms for the language. It is shown that these axioms capture the denotational equality. It follows that if two terms are provably equal then they have the same operational semantics. Finally, we show how to extend the axiomatization in order to axiomatize its operational equivalence.     

Three Inadequate Models

The connection between operational and denotational semantics is of longstanding interest in the study of programming languages. The emphasis has been on positive results, whether for adequacy or full abstraction. One normally considers the standard solution of an evident natural domain equation for the language; this is generally adequate but not fully abstract if one uses any of the usual categories of domains. One then tries other categories to get improved results. Here we restrict ourselves to a standard category of domains and show, for an untyped λ-calculus with arithmetic, that inadequate models exist if one considers non-standard solutions to the domain equation. One model is inadequate, simpliciter; a second is adequate but inadequate when the language is extended by a “parallel or” construct; the third is adequate in the latter sense, but in it the Y-combinator does not denote the least fixed point operator. We also consider whether it is possible to do better than the standard solution as regards full abstraction. Surprisingly this question only makes sense for solutions which are adequate for the extended language. For these the standard solution is indeed closest to full abstraction, justifying the use of non-standard categories. Received October 2000 / Accepted in revised form April 2001     

Distributed quantum programming

In this paper we explore the structure and applicability of the Distributed Measurement Calculus (DMC), an assembly language for distributed measurement-based quantum computations. We describe the formal language’s syntax and semantics, both operational and denotational, and state several properties that are crucial to the practical usability of our language, such as equivalence of our semantics, as well as compositionality and context-freeness of DMC programs. We show how to put these properties to use by constructing a composite program that implements distributed controlled operations, in the knowledge that the semantics of this program does not change under the various composition operations. Our formal model is the basis of a quantum virtual machine construction for distributed quantum computations, which we elaborate upon in the latter part of this work. This virtual machine embodies the formal semantics of DMC such that programming execution no longer needs to be analysed by hand. Far from a literal translation, it requires a substantial concretisation of the formal model at the level of data structures, naming conventions and abstraction mechanisms. At the same time we provide automatisation techniques for program specification where possible to obtain an expressive and user-friendly programming environment.     

动态模糊逻辑程序设计语言的指称语义

文献[8]借鉴Dijkstra的监督命令程序结构,给出了动态模糊逻辑程序设计语言的基本框架结构.在此基础上,进一步扩充和完善,并根据指称语义的原理和方法,用结构归纳法给出动态模糊逻辑程序设计语言的指称语义,主要包括:动态模糊程序设计语言的语义域、语义函数及其指称语义.最后给出了一个动态模糊程序设计语言的例子以观察程序的运行过程.     

A denotational semantics for Handel-C

We present a denotational semantics for a fully functional subset of the Handel-C hardware compilation language (Celoxica Ltd., Handel-C Language Reference Manual, v3.0, 2002, ), based on the concept of typed assertion traces. We motivate the choice of semantic domains by illustrating the complexities of the behaviour of the language, paying particular attention to the prialt (priority-alternation) construct of Handel-C. We then define the typed assertion traces over an abstract notion of actions, and demonstrate key properties of the key semantic operations on these. The denotational semantics is then given using traces with actions instantiated as state-transformers.     

A layered semantics for a parallel object-oriented language

We develop a denotational semantics for POOL, a parallel object-oriented programming language. The main contribution of this semantics is an accurate mathematical model of the most important concept in object-oriented programming: the object. This is achieved by structuring the semantics in layers working at three different levels: for statements, objects and programs. For each of these levels we define a specialized mathematical domain of processes, which we use to assign a meaning to each language construct. This is done in the mathematical framework of complete metric spaces. We also define operators that translate between these domains. At the program level we give a precise definition of the observable input/output behaviour of a particular program, which could be used at a later stage to decide the issue of full abstractness. We illustrate our semantic techniques by first applying them to a toy language similar to CSP.This paper describes work done in ESPRIT Basic Research Action 3020,Integration.     

函数式面向对象语言FOPL的指称语义

函数式面向对象程序设计语言ＦＯＰＬ是笔者设计并实现的一种合成语言，本文在一个全称的抽象域上描述了ＦＯＰＬ语言的指称语义。     

Semantics of plan revision in intelligent agents

In this paper, we give an operational and denotational semantics for a meta-language of the 3APL agent programming language. With this meta-language, various 3APL interpreters can be programmed. We prove equivalence of the operational and denotational semantics. Furthermore, we give an operational semantics for object-level 3APL. Using this semantics, we relate the 3APL meta-language to object-level 3APL by providing a specific interpreter, the semantics of which will prove to be equivalent to object-level 3APL.     

Circular expressions: elimination of static environments

Consider the connection between denotational semantics for a language with goto statements and flow diagrams for programs in such a language. The main point of interest is that the denotational semantics uses a recursively defined environment to give the meaning of labels, while a flow diagram merely has a jump to the appropriate program point. A simple reduction called “indirection elimination” strips away the environment from the denotational semantics and extracts an expression with cycles that is very close to the flow diagram of a program. The same idea applies to associating bodies with recursive procedures, or to any construct whose semantics is not wedded to the syntax. In addition to being a useful data structure and conceptual device, expressions with cycles are well defined mathematical objects—their semantics can be given by unfolding them into infinite structures that have been well studied. The practicality of the elimination of environments has been tested by constructing a trial implementation, which serves as the front end of a semantics directed compiler generator. The implementation takes a denotational semantics of a language and constructs a “black box” that maps programs in the language into an intermediate representation. The intermediate representation is a circular expression.     

A Partial Evaluator for A Parallel Lambda Language

This paper describes theoretical and practical aspects of a partial evaluator that treats a parallel lambda language.The parallel language presented is a combination of lambda calculus and message passing communication mechanism.This parallel language can be used to write a programming language‘s denotational semantics which extracts the paallelism in the program.From this denotational definition of the programming language,the partial evaluator can generate parallel compiler of the language by self-application. The key technique of partial evaluation is binding time analysis that determines in advance which parts of the source program can be evaluated during partial evaluation,and which parts cannot,A binding time analysis is described based upon type inference.A new type chcode in introduced into the type system,which denotes the type of those expressions containing residual channel operations.A well-formedness criterion is given which ensures that partial evaluation not only doesn‘t commit type errors but also doesn‘t change the sequence of channel operations.Before binding time analysis,channel analysis is used to analyze the communication relationship between send and receive processes.     

基于H-等价的算法识别技术研究

蕴涵在程序代码中的语义是程序语言词法和语法的抽象表达,构成了人脑思维与机器思维交互过程的中间变换。从指称语义出发,结合具体语言,用形式化的方法讨论了语义等价和H-等价(Herbrand等价)。H-等价的判定条件相对来说更容易得到满足,具有更广泛的可用性。结合具体算法给出了H-等价在算法识别方面的应用成果及其局限性。     

Magic-sets for localised analysis of Java bytecode

Static analyses based on denotational semantics can naturally model functional behaviours of the code in a compositional and completely context and flow sensitive way. But they only model the functional i.e., input/output behaviour of a program P, not enough if one needs P’s internal behaviours i.e., from the input to some internal program points. This is, however, a frequent requirement for a useful static analysis. In this paper, we overcome this limitation, for the case of mono-threaded Java bytecode, with a technique used up to now for logic programs only. Namely, we define a program transformation that adds new magic blocks of code to the program P, whose functional behaviours are the internal behaviours of P. We prove the transformation correct w.r.t. an operational semantics and define an equivalent denotational semantics, devised for abstract interpretation, whose denotations for the magic blocks are hence the internal behaviours of P. We implement our transformation and instantiate it with abstract domains modelling sharing of two variables, non-cyclicity of variables, nullness of variables, class initialisation information and size of the values bound to program variables. We get a static analyser for full mono-threaded Java bytecode that is faster and scales better than another operational pair-sharing analyser. It has the same speed but is more precise than a constraint-based nullness analyser. It makes a polyhedral size analysis of Java bytecode scale up to 1300 methods in a couple of minutes and a zone-based size analysis scale to still larger applications.     

语义转换--直接指称语义到接续指称语义

指称语义分为直接指称语义和接续指称语义，其中后一种语义描述的难度较大，给出了直接指称语义描述到接续指称语义描述的转换方法，这就使得这种语义转换的自动化成为可能．转换算法揭示了直接指称语义与接续指称语义之间的内在关系，同时也提供了写接续指称语义描述的有效方法．当需要检验同一种语言的直接指称语义描述和接续指称语义描述是否等价时，提供的技术是很有用的。