A lingua franca for concurrent logic programming

Two of the more important concurrent logic programming languages with nonflat guards are GHC and Parlog. They balance the requirements of having clean semantics and providing good control facilities rather differently, and their respective merits are compared and contrasted. Since concurrent logic programming would benefit from both, but neither language is able to express all the programs expressible in the other language, a lingua franca of these languages is defined and justified. A method is given for translating GHC and Parlog to and from it. The method preserves the arities and execution conditions of each clause. It enables a lingua franca implementation to support both languages transparently, and to provide a simple concurrent logic programming language suitable for programming in its own right     

Parallel programming with logic languages: A survey

Formal properties of logic languages are largely studied; however, their impact on the practice of software design and programming is currently minimal. In this paper we survey some interesting representatives of the family of logic languages aiming at comparing the different capabilities they offer for designing and programming parallel systems. The logic languages Prolog, Aurora, Flat Concurrent Prolog, Parlog, GHC, and DeltaProlog were chosen, because a suitable set of relevant examples has been published, mostly by the language designers themselves. A number of sample programs is used to expose and compare the languages with respect to their object oriented programming capabilities for multiprocess coordination, interprocess communication, and resource management. Special attention is devoted also to metaprogramming as well, seen as a useful technique for specifying and building the operating environments of the languages themselves. The paper ends with a discussion on positive and negative features found comparing these languages, and indicates some guidelines to be followed in the design of new logic languages.     

External sources of knowledge and value invention in logic programming

The issue of value invention in logic programming embraces many scenarios, such as logic programming with function symbols, object oriented logic languages, inter-operability with external sources of knowledge, or set unification. This work introduces a framework embedding value invention in a general context. The class of programs having a suitable (but, in general, not decidable) ‘finite grounding property’ is identified, and the class of ‘value invention restricted’ programs is introduced. Value invention restricted programs have the finite grounding property and can be decided in polynomial time. They are a very large polynomially decidable class having this property, when no assumption can be made about the nature of invented values (while this latter is the case in the specific literature about logic programming with function symbols). Relationships with existing formalisms are eventually discussed, and the implementation of a system supporting the class of such programs is described.     

DPOS: A metalanguage and programming environment for parallel processing

This paper describes and illustrates a structured programming metalanguage (DPOS) and graphical programming environment for generating and debugging high-level distributed MIMD parallel programs. DPOS introduces an innovative message-passing model and also recursive graphical definition of parallel process networks. It also provides programming and debugging at the meta language level that is portable across implementation languages. The initial development focus of DPOS is to provide a parallel development system for Lisp-based, symbolic and artificial intelligence programs as part of the MAYFLY parallel processing project. The DPOS environment also generates source code and provides a simulation system for graphical debugging and animation of the programs in graph form.     

Programming with non-determinism in deductive databases

While non-determinism has long been established as a key concept in logic pro-gramming, its importance in the context of deductive databases was recognized only recently. This paper provides an overview of recent results on this topic with the aim of providing an introduction to the theory and practice of non-determinism in deductive databases. In particular we (i) recall the main results linking non-deterministic constructs in database languages to the theory of data complexity and the expressibility hierarchy of query languages; (ii) provide a reasoned introduction to effective programming with non-deterministic constructs; (iii) compare the usage of non-deterministic constructs in languages such as LDL++ to that of traditional logic programming languages; (iv) discuss the link between the semantics of logic programs with non-deterministic constructs and the stable-model semantics of logic programs with negation.     

On goal-directed provability in classical logic

One of the key features of logic programming is the notion of goal-directed provability. In intuitionistic logic, the notion of uniform proof has been used as a proof-theoretic characterization of this property. Whilst the connections between intuitionistic logic and computation are well known, there is no reason per se why a similar notion cannot be given in classical logic. In this paper we show that there are two notions of goal-directed proof in classical logic, both of which are suitably weaker than that for intuitionistic logic. We show the completeness of this class of proofs for certain fragments, which thus form logic programming languages. As there are more possible variations on the notion of goal-directed provability in classical logic, there is a greater diversity of classical logic programming languages than intuitionistic ones. In particular, we show how logic programs may contain disjunctions in this setting. This provides a proof-theoretic basis for disjunctive logic programs, as well as characterising the “disjunctive” nature of answer substitutions for such programs in terms of the provability properties of the classical connectives Λ and Λ.     

Profiling prolog programs

Profilers play an important role in the development of efficient programs. Profiling techniques developed for traditional languages are inadequate for logic programming languages, for a number of reasons: first, the flow of control in logic programming languages, involving back-tracking and failure, is significantly more complex than in traditional languages; secondly, the time taken by a unification operation, the principal primitive operation of such languages, cannot be predicted statically because it depends on the size of the input; and finally, programs may change at run-time because clauses may be added or deleted using primitives such as assert and retract. This paper describes a simple profiler for Prolog. The ideas outlined here may be used either to implement a simple interactive profiler, or integrated into Prolog compilers.     

时序逻辑语言XYZ/E中指针的形式化表示与验证

指针是一种重要的数据类型,使用指针能使程序更加有效和优美.可是指针却以不易驾御而闻名,至今在时序逻辑语言中未见到对它的形式化工作.XYZ/E既是一个时序逻辑系统也是一个程序设计语言,它能表示普通高级语言中几乎所有的重要机制.本文主要讨论在时序逻辑语言XYZ/E中指针的形式化表示问题以及在结构化XYZ/SE程序中指针的验证问题.     

A view of programming languages as symbiosis of meaning and computations

Function and logic programming languages are understood as terms, resp. formulas, of a first order theory. This theory gives meaning to programs and allows reasoning about programs within full predicate logic possibly using quantifiers and induction. The operational semantics of programming languages is given by deductively restricted subtheories of the meaning theory in such a way that the computation sequences are in a one-to-one correspondence with proofs in subtheories. Moreover, meaning is invariant to computations as everything provable in a subtheory is required to be a theorem of the meaning theory. The questions of deadlocks and termination of programs are thus reduced to the proof-theoretical questions of existence of proofs in the subtheories.     

A Highly Dependable Computing Architecture for Safety-Critical Control Applications

More and more technical systems are supervised, controlled and regulated by programmable electronic systems. The dependability of the entire system depends heavily on the safety of the embedded software. But the technological trend to entrust software with tasks of growing complexity and safety relevance conflicts with the lacking acceptance of rigorous proofs of software safety. Based on an international standard for higher level programming languages for programmable logic controllers (PLC, IEC 1131-3), a mathematically based method for validating the behavioral correctness and the functional safety of graphical designs of safety-critical control applications is introduced. The design elements taken from a domain specific module library are proven correct and safe only once. The functional correctness and satisfaction of safety requirements of new application graphical programs can then be shown effectively by reference to the proven properties of the library components used. This approach is part of an comprehensive computing architecture for safety-critical control programs which is presented in a survey.     

The Branching-Time Transformation Technique for Chain Datalog Programs

The branching-time transformation technique has proven to be an efficient approach for implementing functional programming languages. In this paper we demonstrate that such a technique can also be defined for logic programming languages. More specifically, we first introduce Branching Datalog, a language that can be considered as the basis for branching-temporal deductive databases. We then present a transformation algorithm from Chain Datalog programs to the class of unary Branching Datalog programs with at most one IDB atom in the body of each clause. In this way, we obtain a novel implementation approach for Chain Datalog, shedding at the same time new light on the power of branching-time logic programming.     

If Prolog is the Answer, What is the Question? or What it Takes to Support AI Programming Paradigms

Knowledge programming, which makes use of the explicit representation and interpretation of knowledge to create intelligent programs, requires specialized languages and tools to help programmers. Prolog, an implementation of a logic programing language, provides some of these tools; it and other languages have been argued to be the "best" way to do such knowledge programming. This paper raises questions which suggest that any single paradigm of programming (e.g., logic programming or object-oriented programming) benefits by being integrated in a single environment with other paradigms of programming. Integration of these paradigms with each other, and within a flexible, user-friendly computing environment is also necessary. Such an environment must provide source level debugging and monitoring facilities, analysis and performance tuning tools, and an extended set of user communication programs.     

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.     

Evaluation of the Effectiveness of Prolog for a CAD Application

Fifth-generation computers will probably be based on logic programming languages like Prolog rather than on Fortran-type languages. Are such languages suitable to 3-D CAD applications?     

Bounded quantifications for iteration and concurrency in logic programming

The only means for repetition in most logic programming languages, including Prolog, is recursion. Definite iteration is introduced in logic programming languages through the bounded quantification construct. Firstly, it is claimed that this construct is often, though not always, more natural than recursion for expressing relations that involve repetition. In particular, programs involving arrays and similar data structures are significantly simplified. Secondly, it is argued that bounded quantifications should be efficiently implementable on sequential computers and have a high potential for running in parallel, particularly on computers supporting the SPMD model of computation. Bounded quantifications are compared with related constructs from other languages, including the definite loops of imperative languages and the array comprehensions of recent functional languages.     

Logical approximation for program analysis

The abstract interpretation of programs relates the exact semantics of a programming language to a finite approximation of those semantics. In this article, we describe an approach to abstract interpretation that is based in logic and logic programming. Our approach consists of faithfully representing a transition system within logic and then manipulating this initial specification to create a logical approximation of the original specification. The objective is to derive a logical approximation that can be interpreted as a terminating forward-chaining logic program; this ensures that the approximation is finite and that, furthermore, an appropriate logic programming interpreter can implement the derived approximation. We are particularly interested in the specification of the operational semantics of programming languages in ordered logic, a technique we call substructural operational semantics (SSOS). We show that manifestly sound control flow and alias analyses can be derived as logical approximations of the substructural operational semantics of relevant languages.     

Relating the implementation techniques of functional and functional logic languages

Functional logic languages are declarative programming languages that integrate the programming paradigms of functional and logic languages within a single framework. They are extensions of functional languages with principles derived from logic programmingNarrowing, the evaluation mechanism of functional logic languages, can be defined as a generalization ofreduction, the evaluation mechanism of purely functional languages. The unidirectional pattern matching, which is used for parameter passing in functional languages, is simply replaced by the bidirectionalunification known from logic programming languages. We show in this paper, how to extend a reduction machine, that has been designed for the evaluation of purely functional programs to a machine that performs narrowing. The necessary extensions concern the realization of unification and backtracking, for which we fall back upon the methods of Warren’s Prolog engine.²¹⁾ The narrowing machine embodies an optimized treatment of deterministic computations. A complete specification of the reduction and the narrowing machine and of the translation of a sample language into abstract machine code is given. Comparative results of a C-implementation of the reduction and the narrowing machine show that the time overhead of the more complex narrowing evaluation is, in general, less than 10% of the reduction evaluation.     

基于HTML语言的跨平台界面设计

描述了如何利用HTML超文本标识语言为终端用户创建基于表单的图形化界面。在这里HTML语言仅用于描述用户界面的的外观，程序的编程可以用许多种编程语言或脚本语言。     

基于HTML语言的用户界面设计

描述了如何利用HTML超文本标记语言为终端用户创建基于表单的图形化界面。在这里HTML语言仅用于描述用户界面的外观 ,程序的编制可以用许多种编程语言或脚本语言。     

一种用于指针程序的形状分析方法

指针程序的分析一直是研究热点。本文提出一种基于形状图逻辑的形状分析方法,其中形状分析采用形状图来表达程序中指针的指向和相等关系,并用形状图逻辑来进行推理。形状图逻辑是一种把形状图看成有关指针的断言,并在此基础上对Hoare逻辑进行扩展而得到的程序逻辑。首先介绍所提出的形状图和形状图逻辑;然后在此基础之上,设计一种基于形状图逻辑的形状分析方法。