A transformation system for concurrent processes

Program transformation techniques have been extensively studied in the framework of functional and logic languages, where they were applied mainly to obtain more efficient and readable programs. All these works are based on the Unfold/Fold program transformation method developed by Burstall and Darlington in the context of their recursive equational language. The use of Unfold/Fold based transformations for concurrent languages is a relevant issue that has not yet received an adequate attention. In this paper we define a transformation methodology for CCS. We give a set of general rules which are a specialization of classical program transformation rules, such as Fold and Unfold. Moreover, we define the general form of other rules, “oriented” to the goal of a transformation strategy, and we give conditions for the correctness of these rules. We prove that a strategy using the general rules and a set of goal oriented rules is sound, i.e. it transforms CCS programs into equivalent ones. We show an example of application of our method. We define a strategy to transform, if possible, a full CCS program into an equivalent program whose semantics is a finite transition system. We show that, by means of our methodology, we are able to a find finite representations for a class of CCS programs which is larger than the ones handled by the other existing methods. Our transformational approach can be seen as unifying in a common framework a set of different techniques of program analysis. A further advantage of our approach is that it is based only on syntactic transformations, thus it does not requires any semantic information. Received: 24 April 1997 / 19 November 1997     

Instant replay debugging of concurrent logic programs

One problem with debugging (committed choice) concurrent logic programs is that their behaviour may be non-deterministic, in that successive executions of the same program may produce different results. We describe a scheme, based on the ‘Instant Replay’ scheme developed for more conventional parallel languages, that allows us to reproduce the execution behaviour of a concurrent logic program on subsequent executions, so that the execution may be examined for debugging purposes. The properties of concurrent logic programming languages allow us to simplify our scheme greatly. We have demonstrated our scheme with KLIC, and KL1 on the PIM multiprocessors, but it can also be applied to other committed choice concurrent logic programming languages.     

Reproducible execution of SR programs

Reproducing the execution of a concurrent program is important in debugging and testing. It requires that, regardless of the actual order in which processes may execute, the reproduced execution is identical, with respect to the order in which certain activities occur, to a previously recorded execution. This paper presents a solution to the reproducibility problem for programs written in the SR concurrent programming language. Our solution transforms an arbitrary SR program into one for recording an event sequence and one for replaying from an event sequence. SR provides a rich collection of synchronization mechanisms, including rendezvous, asynchronous message passing, remote procedure call, and dynamic process creation. SR language features allow: flexible invocation servicing (e.g. use of invocation parameters in selecting an invocation to service in message passing or rendezvous); dynamically created processes and resource (module) instances; dynamic communication paths between processes; and dynamic distribution of programs across multiple machines. Because of these features, adaptations of previous solutions to the reproducibility problem for other languages and notations do not work for SR. Our solution handles all the above features. It results in a naturally distributed control algorithm for programs that are distributed. This paper also describes the implementations of our transformation tools. Copyright © 1999 John Wiley & Sons, Ltd.     

Abstract interpretation of logic programs using magic transformations

In dataflow analysis of logic programs, information must be propagated according to the control strategy of the language under consideration. However, for languages with top-down control flow, naive top-down dataflow analyses may have problems guaranteeing completeness and/or termination. What is required in the dataflow analysis is a bottom-up fixpoint computation, guided by the (possibly top-down) control strategy of the language. This paper describes the application of the magic templates algorithm, originally devised as a technique for efficient bottom-up computation of logic programs, to dataflow analysis of logic programs. It turns out that a direct application of the magic templates algorithm can result in an undesirable loss in precision, because connections between “calling patterns” and the corresponding “success patterns” may be lost. We show how the original magic templates algorithm can be modified to avoid this problem, and prove that the resulting analysis algorithm is at least as precise as any other abstract interpretation that uses the same abstract domain and abstract operations.     

Programming in a wide spectrum language: a collection of examples

The paper exemplifies programming in a wide spectrum language by presenting styles which range from non-operative specifications—using abstract types and tools from predicate logic as well as set theory—over recursive functions, to procedural program with variables. Besides a number of basic types, we develop an interpreter for parts of the language itself, an algorithm for applying transformation rules to program representations, a text editor, and a simulation of Backus' functional programming language.     

Category-based modularisation for equational logic programming

Although modularisation is basic to modern computing, it has been little studied for logic-based programming. We treat modularisation for equational logic programming using the institution of category-based equational logic in three different ways: (1) to provide a generic satisfaction condition for equational logics; (2) to give a category-based semantics for queries and their solutions; and (3) as an abstract definition of compilation from one (equational) logic programming language to another. Regarding (2), we study soundness and completeness for equational logic programming queries and their solutions. This can be understood as ordinary soundness and completeness in a suitable “non-logical” institution. Soundness holds for all module imports, but completeness only holds for conservative module imports. Category-based equational signatures are seen as modules, and morphisms of such signatures as module imports. Regarding (3), completeness corresponds to compiler correctness. The results of this research applies to languages based on a wide class of equational logic systems, including Horn clause logic, with or without equality; all variants of order and many sorted equational logic, including working modulo a set of axioms; constraint logic programming over arbitrary user-defined data types; and any combination of the above. Most importantly, due to the abstraction level, this research gives the possibility to have semantics and to study modularisation for equational logic programming developed over non-conventional structures. Received April 15, 1994/April 12, 1995     

The Least Fixpoint Transformation for Disjunctive Logic Programs

The paradigm of disjunctive logic programming(DLP)enhances greatly the expressive power of normal logic programming(NLP)and many(declarative)semantics have been defined for DLP to cope with various problems of knowledge representation in artificial intelligence.However,the expressive ability of the semantics and the soundness of program transformations for DLP have been rarely explored.This paper defines an immediate consequence operatro T^GP for each disjunctive program and shows that T^GP has the least and computable fixpoint Lft(P),Lft is,in fact,a program transformation for DLP,which transforms all disjunctive programs into negative programs.It is shown that Lft preserves many key semantics,including the disjunctive stable models,well-founded model,disjunctive argunent semantics DAS,three-valued models,ect.Thic means that every disjunctive program P has a unique canonical form Lft(P)with respect to these semantics.As a result,the work in this paper provides a unifying framework for studying the expressive ability of various semantics for DLP On the other hand,the computing of the above semantics for negative programs is ust a trivial task,therefore,Lft(P)is also an optimization method for DLP.Another application of Lft is to derive some interesting semantic results for DLP.     

Relating logic programs via program maps

This paper presents a mathematical theory underlying a systematic method for constructingProlog programs calledstepwise enhancement. Stepwise enhancement dictates building a program starting with askeleton program which constitutes the basic control flow for the problem to be solved, and adding extra computations to the skeleton program by using well-understood programming techniques. Each extra computation can be developed independently, and the separate enhancements combined to produce the final program. While intuition and motivation have focused onProlog, the methods are applicable to logic programming languages more generally. The central concept in our mathematical theory for stepwise enhancement is that of a program map between two logic programs. Our definition of a program map from an enhancement to its skeleton guarantees the lifting of computations, the essence of the enhancement methodology. In this paper, we give definitions of program map and extensions, show that the definitions preserve the property of computations lifting, give examples of extensions and programming techniques which generate them, and point to directions for future work.     

线性递归Da taL og 程序优化算法

提出了线性齐次ＤａｔａＬｏｇ逻辑程序的概念,并为该类程序设计了一个优化的求解算法。在此基础上提出了求解一般线性ＤａｔａＬｏｇ程序的优化算法,该算法利用带有的约束条件的递归调用方法,将线性ＤａｔａＬｏｇ程序求解问题变换成齐次程序的求解问题。算法简单,易于实现,可应用于任何线性ＤａｔａＬｏｇ程序的求解。     

A domain-specific language for regular sets of strings and trees

We propose a novel high level programming notation, called FIDO, that we have designed to concisely express regular sets of strings or trees. In particular, it can be viewed as a domain-specific language for the expression of finite state automata on large alphabets (of sometimes astronomical size). FIDO is based on a combination of mathematical logic and programming language concepts. This combination shares no similarities with usual logic programming languages. FIDO compiles into finite state string or tree automata, so there is no concept of run-time. It has already been applied to a variety of problems of considerable complexity and practical interest. We motivate the need for a language like FIDO, and discuss our design and its implementation. Also, we briefly discuss design criteria for domain-specific languages that we have learned from the work with FIDO. We show how recursive data types, unification, implicit coercions, and subtyping can be merged with a variation of predicate logic, called the Monadic Second-order Logic (M2L) on trees. FIDO is translated first into pure M2L via suitable encodings, and finally into finite state automata through the MONA tool     

Linear programs in a simple reversible language

Very simple reversible programming languages can be useful for the study of reversible transformations. For this purpose we define simple reversible language (SRL), a very simple reversible language, and analyse its properties. The language SRL is similar to the “loop” languages that have been used by several authors to characterise the set of primitive recursive functions. There are, however, important differences: SRL has domain instead of and only reversible programs can be written in SRL. The reversibility of linear homogeneous SRL programs is related to the fact that the corresponding set of matrices has the algebraic structure of a group. We show that such programs implement exactly the linear transformations corresponding to the group of integer positive modular matrices, while in ESRL, an extended version of SRL, the set of transformations that can be implemented by linear homogeneous programs corresponds exactly to the group of integer modular matrices.     

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.     

Rule-based coordination of logic programs

Shared Prolog (SP) is a parallel symbolic language in which coordination issues are clearly separated from computation issues. SP combines concurrency and communication based on a shared dataspace coordination model with sequential symbolic computation based on logic programming. We demonstrate how a rule-based coordination language can be used for expressing a number of different parallel computing schemata, reusing and reorganizing existing sequential programs.     

Program transformation through meta-shifting

A program transformation strategy called meta-shifting is developed for control optimization of programs written in languages with control freedom. The strategy involves writing a specialized evaluator for each program (segment) with specific control. It is applied to an equational language to derive a general method to transform one program into another, which simulates (approximately) normal order evaluation of the original program, under interpreters with arbitrary evaluation order.     

A residualizing semantics for the partial evaluation of functional logic programs

Recent proposals for multi-paradigm declarative programming combine the most important features of functional, logic and concurrent programming into a single framework. The operational semantics of these languages is usually based on a combination of narrowing and residuation. In this paper, we introduce a non-standard, residualizing semantics for multi-paradigm declarative programs and prove its equivalence with a standard operational semantics. Our residualizing semantics is particularly relevant within the area of program transformation where it is useful, e.g., to perform computations during partial evaluation. Thus, the proof of equivalence is a crucial result to demonstrate the correctness of (existing) partial evaluation schemes.     

Negation as Failure. Completeness of the Query Evaluation Process for horn clause programs with recursive definitions

An extension of the class of logic programs for which the Negation as Failure rule is equivalent to the Closed World Assumption is presented. This extension includes programs on infinite domains and with recursive definitions. For this class of programs with ground (positive or negative) queries the Query Evaluation Process is complete. A characterization of this class of programs is given, and a decision algorithm, which recognizes a subclass of these programs, is presented. The algorithm is based on showing the correspondence between a program and a primitive recursive function. Work partially supported by Esprit Project 530 (Epsilon).     

命令式语言的化学语义

化学计算模型是基于化学反应和计算之间比喻的并行计算模型,其内在的并行性及不确定性可以有效的消除与计算逻辑本身无关的人为顺序性,但是难于描述特定的控制机制.高阶化学编程语言是对传统化学计算模型的扩展和泛化,可以描述传统的控制机制和定义新的控制机制.通过从简单命令式语言到高阶化学语言的转换,给出了命令式语言的一种化学语义描述,为结合命令式编程和化学编程提供了一种可能.     

Verification of object-oriented programs: A transformational approach

We show that verification of object-oriented programs by means of the assertional method can be achieved in a simple way by exploiting a syntax-directed transformation from object-oriented programs to recursive programs. This transformation suggests natural proofs rules and its correctness helps us to establish soundness and relative completeness of the proposed proof system. One of the difficulties is how to properly deal in the assertion language with the instance variables and aliasing. The discussed programming language supports arrays, instance variables, failures and recursive methods with parameters. We also explain how the transformational approach can be extended to deal with other features of object-oriented programming, like classes, inheritance, subtyping and dynamic binding.     

A type system for logic programs

A theory for a type system for logic programs is developed which addressesthe question of well-typing, type inference, and compile-time and run-time type checking. A type is a recursively enumerable set of ground atoms, which is tuple-distributive. The association of a type to a program is intended to mean that only ground atoms that are elements of the type may be derived from the program. A declarative definition of well-typed programs is formulated, based on an intuitive approach related to the fixpoint semantics of logic programs. Whether a program is well typed is undecidable in general. We define a restricted class of types, called regular types, for which type checking is decidable. Regular unary logic programs are proposed as a specification language for regular types. An algorithm for type-checking a logic program with respect to a regular type definition is described, and its complexity is analyzed. Finally, the practicality of the type system is discussed, and some examples are shown. The type system has been implemented in FCP for FCP and is incorporated in the Logix system.