On stratified disjunctive programs

We address the problem of a consistent fixpoint semantics for general disjunctive programs restricted to stratifiable programs which do not recurse through negative literals. We apply the nonmonotonic fixpoint theory developed by Apt, Blair and Walker to a closure operatorT ^c and develop a fixpoint semantics for stratified disjunctive programs. We also provide an iterative definition for negation, called the Generalized Closed World Assumption for Stratified programs (GCWAS), and show that our semantics captures this definition. We develop a model-theoretic semantics for stratified disjunctive programs and show that the least state characterized by the fixpoint semantics corresponds to a stable-state defined in a manner similar to the stable-models of Gelfond and Lifschitz. We also discuss a weaker stratification semantics for general disjunctive programs based on the Weak Generalized Closed World Assumption.     

Chart parsers as inference systems for fixed-mode logic programs

Logic programs resemble context-free grammars. Moreover, Prolog’s proof procedure can be viewed as a generalization of a simple top-down parser with backtracking. This simple parser has disadvantages that motivated the design of more sophisticated parsing methods. As similar disadvantages occur in Prolog’s proof procedure, it may be desirable to develop other proof procedures for logic programs than the one used by Prolog. The resemblance between definite clauses and productions suggests looking at parsing to develop such procedures. We obtain proof procedures for fixed-mode logic programs, based on “chart” parsers. Our approach concentrates on transforming (fixed-mode) logic programs rather than the parser. We first add unification to a chart parser obtaining a proof procedure for programs severely restricted in their syntax, in which the body of the clauses denotes the composition of binary relations: “chain” programs. We then show how to transform fixed-mode programs into chain form. We arrive at proof procedures that avoid some nonterminating loops as well as the recomputation of some partial results.     

Non-standard posynomial geometric programs

Non-standard posynomial geometric programs are non-linear programs that can be transformed into posynomial geometric programs. In this paper, new classes of nonstandard geometric programs are introduced. We focus on minimax posynomial programs and fractional posynomial programs. A complete duality theory is developed for each class.     

Intensional Properties of Polygraphs

We present polygraphic programs, a subclass of Albert Burroni's polygraphs, as a computational model, showing how these objects can be seen as first-order functional programs. We prove that the model is Turing complete. We use polygraphic interpretations, a termination proof method introduced by the second author, to characterize polygraphic programs that compute in polynomial time. We conclude with a characterization of polynomial time functions and non-deterministic polynomial time functions.     

Semantic Forcing in Disjunctive Logic Programs

We propose a semantics for disjunctive logic programs, based on the single notion of forcing. We show that the semantics properly extends, in a natural way, previous approaches. A fixpoint characterization is also provided. We also take a closer look at the relationship between disjunctive logic programs and disjunctive-free logic programs. We present certain criteria under which a disjunctive program is semantically equivalent with its disjunctive-free (shifted) version.     

Compiling C for the EARTH multithreaded architecture

Multithreaded architectures provide an opportunity for efficiently executing programs with irregular parallelism and/or irregular locality. This paper presents a strategy that makes use of the multithreaded execution model without exposing multithreading to the programmer. Our approach is to design simple extensions to C, and to provide compiler support that automatically translates high-level C programs into lower-level threaded programs. In this paper we present EARTH-C our extended C language which contains simple constructs for specifying control parallelism, data locality, shared variables and atomic operations. Based on EARTH-C, we describe compiler techniques that are used for translating to lower-level Threaded-C programs for the EARTH multithreaded architecture. We demonstrate our approach with six benchmark programs. We show that even naive EARTH-C programs can lead to reasonable performance, and that more advanced EARTH-C programs can give performance very close to hand-coded threated-C programs. This work supported, in part, by NSERC and FCAR.     

Specification and Verification of Concurrent Programs Through Refinements

We present a framework for the specification and verification of reactive concurrent programs using general-purpose mechanical theorem proving. We define specifications for concurrent programs by formalizing a notion of refinements analogous to stuttering trace containment. The formalization supports the definition of intuitive specifications of the intended behavior of a program. We present a collection of proof rules that can be effectively orchestrated by a theorem prover to reason about complex programs using refinements. The proof rules systematically reduce the correctness proof for a concurrent program to the definition and proof of an invariant. We include automated support for discharging this invariant proof with a predicate abstraction tool that leverages the existing theorems proven about the components of the concurrent programs. The framework is integrated with the ACL2 theorem prover and we demonstrate its use in the verification of several concurrent programs in ACL2.     

Transformation of structure-shy programs with application to XPath queries and strategic functions

Various programming languages allow the construction of structure-shy programs. Such programs are defined generically for many different datatypes and only specify specific behavior for a few relevant subtypes. Typical examples are XML query languages that allow selection of subdocuments without exhaustively specifying intermediate element tags. Other examples are languages and libraries for polytypic or strategic functional programming and for adaptive object-oriented programming.In this paper, we present an algebraic approach to transformation of declarative structure-shy programs, in particular for strategic functions and XML queries. We formulate a rich set of algebraic laws, not just for transformation of structure-shy programs, but also for their conversion into structure-sensitive programs and vice versa. We show how subsets of these laws can be used to construct effective rewrite systems for specialization, generalization, and optimization of structure-shy programs. We present a type-safe encoding of these rewrite systems in Haskell which itself uses strategic functional programming techniques. We discuss the application of these rewrite systems for XPath query optimization and for query migration in the context of schema evolution.     

Scaling of program fitness spaces

We investigate the distribution of fitness of programs concentrating on those represented as parse trees and, particularly, how such distributions scale with respect to changes in the size of the programs. By using a combination of enumeration and Monte Carlo sampling on a large number of problems from three very different areas, we suggest that, in general, once some minimum size threshold has been exceeded, the distribution of performance is approximately independent of program length. We proof this for both linear programs and simple side effect free parse trees. We give the density of solutions to the parity problems in program trees which are composed of XOR building blocks. Limited experiments with programs including side effects and iteration suggest a similar result may also hold for this wider class of programs.     

Enabledness and termination in refinement algebra

Refinement algebras are abstract algebras for reasoning about programs in a total correctness framework. We extend a reduct of von Wright’s demonic refinement algebra with two operators for modelling enabledness and termination of programs. We show how the operators can be used for expressing relations between programs and apply the algebra to reasoning about action systems.     

Properties of Input-Consuming Derivations

We study the properties of input-consuming derivations of moded logic programs. Input-consuming derivations do not employ a fixed selection rule, and can be used to model the behavior of logic programs using dynamic scheduling and employing constructs such as delay declarations.We consider the class of nicely-moded programs and queries. We show that for these programs one part of the well-known Switching Lemma holds also for input-consuming derivations. Furthermore, we provide conditions which guarantee that all input-consuming derivations starting in a Nicely-Moded query are finite. The method presented here is easy to apply and generalizes other related works.     

Extremal problems in logic programming and stable model computation

We study the following problem: given a class of logic programs ¢, determine the maximum number of stable models of a program from ©. We establish the maximum for the class of all logic programs with at most n clauses, and for the class of all logic programs of size at most n. We also characterize the programs for which the maxima are attained. We obtained similar results for the class of all disjunctive logic programs with at most n clauses, each of length at most m, and for the class of all disjunctive logic programs of size at most n. Our results on logic programs have direct implication for the design of algorithms to compute stable models. Several such algorithms, similar in spirit to the Davis-Putnam procedure, are described in the paper. Our results imply that there is an algorithm that finds all stable models of a program with n clauses after considering the search space of size O(3^n/3) in the worst case. Our results also provide some insights into the question of representability of families of sets as families of stable models of logic programs.     

A Framework for Datatype Transformation

We study one dimension in program evolution, namely the evolution of the datatype declarations in a program. To this end, a suite of basic transformation operators is designed. We cover structure-preserving refactorings, but also structure-extending and -reducing adaptations. Both the object programs that are subject to datatype transformations, and the meta programs that encode datatype transformations are functional programs.     

SAS macro programs for geographically weighted generalized linear modeling with spatial point data: applications to health research

An increasing interest in exploring spatial non-stationarity has generated several specialized analytic software programs; however, few of these programs can be integrated natively into a well-developed statistical environment such as SAS. We not only developed a set of SAS macro programs to fill this gap, but also expanded the geographically weighted generalized linear modeling (GWGLM) by integrating the strengths of SAS into the GWGLM framework. Three features distinguish our work. First, the macro programs of this study provide more kernel weighting functions than the existing programs. Second, with our codes the users are able to better specify the bandwidth selection process compared to the capabilities of existing programs. Third, the development of the macro programs is fully embedded in the SAS environment, providing great potential for future exploration of complicated spatially varying coefficient models in other disciplines. We provided three empirical examples to illustrate the use of the SAS macro programs and demonstrated the advantages explained above.     

A study of potential parallelism among traces in Java programs

The exploitation of parallelism among traces, i.e. hot paths of execution in programs, is a novel approach to the automatic parallelization of Java programs and it has many advantages. However, to date, the extent to which parallelism exists among traces in programs has not been made clear. The goal of this study is to measure the amount of trace-level parallelism in several Java programs. We extend the Jupiter Java Virtual Machine with a simulator that models an abstract parallel system. We use this simulator to measure trace-level parallelism. We further use it to examine the effects of the number of processors, trace window size, and communication type and cost on performance. We also analyze the dependence characteristics of the benchmarks and see how they relate to parallelism. The results indicate that enough trace-level parallelism exists for a modest number of processors. Thus, we conclude that trace-based parallelization is a potentially viable approach to improve the performance of Java programs.     

Disjunctive LP+integrity constraints= stable model semantics

We show that stable models of logic programs may be viewed as minimal models of programs that satisfy certain additional constraints. To do so, we transform the normal programs into disjunctive logic programs and sets of integrity constraints. We show that the stable models of the normal program coincide with the minimal models of the disjunctive program thatsatisfy the integrity constraints. As a consequence, the stable model semantics can be characterized using theextended generalized closed world assumption for disjunctive logic programs. Using this result, we develop a bottomup algorithm for function-free logic programs to find all stable models of a normal program by computing the perfect models of a disjunctive stratified logic program and checking them for consistency with the integrity constraints. The integrity constraints provide a rationale as to why some normal logic programs have no stable models.     

Probabilistic incremental program evolution

Probabilistic incremental program evolution (PIPE) is a novel technique for automatic program synthesis. We combine probability vector coding of program instructions, population-based incremental learning, and tree-coded programs like those used in some variants of genetic programming (GP). PIPE iteratively generates successive populations of functional programs according to an adaptive probability distribution over all possible programs. Each iteration, it uses the best program to refine the distribution. Thus, it stochastically generates better and better programs. Since distribution refinements depend only on the best program of the current population, PIPE can evaluate program populations efficiently when the goal is to discover a program with minimal runtime. We compare PIPE to GP on a function regression problem and the 6-bit parity problem. We also use PIPE to solve tasks in partially observable mazes, where the best programs have minimal runtime.     

Programming-in-the-Large Versus Programming-in-the-Small

We distinguish the activity of writing large programs from that of writing small ones. By large programs we mean systems consisting of many small programs (modules), usually written by different people.     

基于交互式定理证明的并发程序验证工作综述

并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度,在现实中有着非常广泛的应用。但是并发程序与并发系统往往难以保证其实现的正确性,实际应用程序运行中的错误会带来严重的后果。同时,并发程序执行时的不确定性会给其正确性验证带来巨大的困难。在形式化验证方法中,人们可以通过交互式定理证明器严格地对并发程序进行验证。本文对在交互式定理证明中可用于描述并发程序正确性的验证目标进行总结,它们包括霍尔三元组、可线性化、上下文精化和逻辑原子性。交互式定理证明方法中常用程序逻辑对程序进行验证,本文分析了基于并发分离逻辑、依赖保证逻辑、关系霍尔逻辑等理论研究的系列成果与相应形式化方案,并对使用了这些方法的程序验证工具和程序验证成果进行了总结。