Catálogo de publicaciones - libros

Information about the nondeterminism behavior of a functional logic program is important for various reasons. For instance, a nondeterministic choice in I/O operations results in a run-time error. Thus, it is desirable to ensure at compile time that a given program is not going to crash in this way. Furthermore, knowledge about nondeterminism can be exploited to optimize programs. In particular, if functional logic programs are compiled to target languages without builtin support for nondeterministic computations, the transformation can be much simpler if it is known that the source program is deterministic.

In this paper we present a nondeterminism analysis of functional logic programs in form of a type/effect system. We present a type inferencer to approximate the nondeterminism behavior via nonstandard types and show its correctness w.r.t. the operational semantics of functional logic programs. The type inference is based on a new compact representation of sets of types and effects.

Any finite tree automaton (or regular type) can be used to construct an abstract interpretation of a logic program, by first determinising and completing the automaton to get a pre-interpretation of the language of the program. This has been shown to be a flexible and practical approach to building a variety of analyses, both generic (such as mode analysis) and program-specific (with respect to a type describing some particular property of interest). Previous work demonstrated the approach using pre-interpretations over small domains. In this paper we present techniques that allow the method to be applied to more complex pre-interpretations and larger programs. There are two main techniques presented: the first is a novel algorithm for determinising finite tree automata, yielding a compact “product” form of the transitions of the result automaton, that is often orders of magnitude smaller than an explicit representation of the automaton. Secondly, it is shown how this form (which is a representation of a pre-interpretation) can then be input directly to a BDD-based analyser of Datalog programs. We demonstrate through experiments that much more complex analyses become feasible.

Model checking is a widely used technique for verifying complex concurrent systems. The models used in classical model checking methods are assumed to be complete and consistent. However, a recent body of work has shown that this is not always the case, and multi-valued logics have been proposed to represent such models, spawning an extension of classical model checking, known as, multi-valued model checking. In this paper, we define a multi-valued set based semantics for the multi-valued modal -calculus and present a novel interpretation of logic programs to support multi-valued sets as first-class entities, that can be used as a practical deductive multi-valued model checking framework. This framework provides a semantics preserving encoding of multi-valued transition systems, and allows verification of arbitrary multi-valued modal -calculus properties. A prototype implementation of this framework has also been realized.

This paper introduces a new technique for termination analysis of definite logic programs based on polynomial interpretations. The principle of this technique is to map each function and predicate symbol to a polynomial over some domain of natural numbers, like it has been done in proving termination of term rewriting systems. Such polynomial interpretations can be seen as a direct generalisation of the traditional techniques in termination analysis of LPs, where (semi-) linear norms and level mappings are used. Our extension generalises these to arbitrary polynomials. We extend a number of standard concepts and results on termination analysis to the context of polynomial interpretations. We propose a constraint based approach for automatically generating polynomial interpretations that satisfy termination conditions.

Termination analysis is often performed over the abstract domains of monotonicity constraints or of size change graphs. First, the transition relation for a given program is approximated by a set of descriptions. Then, this set is closed under a composition operation. Finally, termination is determined if all of the idempotent loop descriptions in this closure have (possibly different) ranking functions. This approach is complete for size change graphs: An idempotent loop description has a ranking function if and only if it has one which indicates that some specific argument decreases in size. In this paper we generalize the size change criteria for size change graphs which are not idempotent. We also illustrate that proving termination with monotonicity constraints is more powerful than with size change graphs and demonstrate that the size change criteria is incomplete for monotonicity constraints. Finally, we provide a complete termination test for monotonicity constraints.

In this paper we develop a new semantics for disjunctive logic programs, called (), by resorting to a fixed point-based operator. Coinciding with the Well-Founded Semantics (WFS) for normal logic programs, our semantics is uniquely defined for every disjunctive logic program. By exploring examples, we show does not agree with any other semantics we have studied, such as Brass and Dix’s  − , Przymusinski’s Static, Baral ’s , Wang’s , and van Gelder ’s . Despite that, we ensure is strictly stronger than  −  by guaranteing allows the five, desirable, program transformations proposed by Brass and Dix: unfolding, elimination of tautologies and non-minimal rules, and positive and negative reduction.

This paper investigates semantics of framed temporal logic programs. To this end, a projection temporal logic and its executable subset are presented. Based on this language, a framing technique is introduced. The semantics of a non-framed program is well interpreted by the canonical model. However, since introducing a framing operator destroys monotonicity, a canonical model may no longer capture the intended meaning of a program. Hence, a minimal model theory is developed. Within this model, negation by default is used to manipulate frame operator. Further, the temporal semantics of framed programs is captured by means of the minimal models. The existence of a minimal model for a given framed program is also proved. An example is given to illustrate how the semantics of framed programs can be captured.

Higher-order pattern unification problems arise often in computations within systems such as Twelf, Prolog and Isabelle. An important characteristic of such problems is that they are given by equations appearing under a prefix of alternating universal and existential quantifiers. Most existing algorithms for solving these problems assume that such prefixes are simplified to a ∀ ∃ ∀ form by an a priori application of a transformation known as raising. There are drawbacks to this approach. Mixed quantifier prefixes typically manifest themselves in the course of computation, thereby requiring a dynamic form of preprocessing that is difficult to support in low-level implementations. Moreover, raising may be redundant in many cases and its effect may have to be undone by a subsequent pruning transformation. We propose a method to overcome these difficulties. In particular, a unification algorithm is described that proceeds by recursively descending through the structures of terms, performing raising and other transformations on-the-fly and only as needed.

We instrument a higher-order logic programming search procedure to generate and check small proof witnesses for the Twelf system, an implementation of the logical framework LF. In particular, we extend and generalize ideas from Necula and Rahul [16] in two main ways: 1) We consider the full fragment of LF including dependent types and higher-order terms and 2) We study the use of caching of sub-proofs to further compact proof representations. Our experimental results demonstrate that many of the restrictions in previous work can be overcome and generating and checking small witnesses within Twelf provides valuable addition to its general safety infrastructure.

The language of (CHR) of T. Frühwirth [1] is a successful rule-based language for implementing constraint solvers in a wide variety of domains. It is an extension of a host language, such as Prolog [2], Java or Haskell [3], allowing the introduction of new constraints in a declarative way. One peculiarity of CHR is that it allows multiple heads in rules. For the sake of simplicity, we consider only simpli.cation rules, since the distinction of propagation and simpagation rules [1] is not needed for typing purposes. A simpli.cation rule is of the form , where ,..., is a nonempty sequence of CHR constraints, the guard ,..., is a sequence of native constraints and the body ,..., is a sequence of CHR and native constraints.