ALP'96 Abstracts of Accepted Papers

Specifying Type Systems

by Dieter Nazareth
Abstract:

This paper presents a flexible type system developed for an axiomatic specification language. The type system can be dynamically adapted to different application areas. In particular, it allows the modelling of different kinds of polymorphism, like type classes or subtyping. The type system is based on the concept of qualified types. It allows one to abstract from concrete types by using type variables and to qualify these type variables by type predicates. The properties of the type predicates are described by a specification language based on Horn clauses. The notion of well-typedness is defined via a type inference calculus. We investigate the implementation of the type inference calculus and present an inference algorithm which splits into two phases. The first phase checks the well-formedness of the given term and computes the necessary type predicate restrictions. The second phase uses resolution to prove the computed restrictions to be correct with respect to the type predicate specification. We show that the inference algorithm is correct and complete with respect to the type inference calculus. In general, the type inference algorithm terminates only for well-typed terms because the problem is only semi-decidable. If particular polymorphism concepts, as for example the type class system of Haskell, are modelled the problem becomes decidable, and the given type inference algorithm terminates for all terms.

The Semantic Treatment of Polymorphic Specification Languages

by Dieter Nazareth
Abstract:

Polymorphic type systems combined with type inference are commonly used in functional programming languages. Specification languages aiming at the development of functional programs should therefore also include these concepts. In this paper we investigate the semantic treatment of polymorphism in axiomatic specification languages. We present a concept of model that is neither based on some intermediate language, nor on a particular sort inference algorithm. We investigate the semantic relations between different sort derivations of a specification and show that syntactically more general derivations have less models. This result allows us to define an equivalent model concept based on some most general sort derivation of a specification.

Prime Factorizations of Abstract Domains Using First Order Logic

by Elena Marchiori
Abstract:

This paper proposes an alternative approach based on first--order logic for reasoning about abstract domains for the static analysis of logic programs. Abstract domains for logic programming are closed w.r.t.~variance, in the sense that the names of the variables used in their de*nitionis irrelevant. This property allows us to use a standard algebraic notion of (conjunctive) factorization in order to decompose abstract domains in prime factors. Factorizations are used for a comparative study of abstract domains. The benefits of this approach can be summarized as follows: a) The approach is simple and direct. b) The familiar setting of first--order logic is used both for formalizing the properties (i.e.~the abstract domains) of interest and for writing the programs. c) A comparative analysis of abstract domains is facilitated by the syntactic form of the domains, being these sets of assertions: comparing abstract domains amounts to inspecting the form of the corresponding assertions. d) The framework provides a natural setting for proving properties of abstract domains, like correctness and optimality: the problem of proving a property is translated into the problem of checking the validity of a suitable assertion in the assertion language.

In order to substantiate the above claims, a comparative study of various useful abstract domains for ground, dependency and aliasing analysis in logic programming is performed.

Meaningless terms in rewriting

by Richard Kennaway, Vincent van Oostrom, Fer-Jan de Vries
Abstract:

We present an axiomatic approach to the notion of meaninglessness in finite and transfinite term rewriting and lambda calculus. We justify our axioms in two ways. First, they are shown to imply important properties of meaninglessness: genericity of the class of meaningless terms, the consistency of equating all meaningless terms, and the construction of Bohm trees. Second we show that they can be easily verified for existing notions of meaninglessness.

Unravelings and Ultra-properties

by Massimo Marchiori
Abstract:

Conditional rewriting is universally recognized as being much more complicated than unconditional rewriting. In this paper we study how much of conditional rewriting can be automatically inferred from the simpler theory of unconditional rewriting. We introduce a new tool, called unraveling, to automatically translate a conditional term rewriting system (CTRS) into a term rewriting system (TRS). An unraveling enables to infer properties of a CTRS by studying the corresponding ultra-property on the corresponding TRS. We show how to rediscover properties like decreasingness, and to give easy proofs of some existing results on CTRSs. Moreover, we show how unravelings provide a valuable tool to study modularity of CTRSs, automatically giving a multitude of new results. Finally, we perform an abstract analysis of the unraveling approach, showing that in a sense the results of this paper are the best possible.

Unique Normal Form Property of Higher-Order Rewriting Systems

by Ken Mano, Mizuhito Ogawa
Abstract:

Van Oostrom proposed the framework of Higher-Order Rewriting Systems (HORSs), capable of unifying various existing theory of rewriting. He also proved that a non-overlapping left-linear pattern HORS has the Church-Rosser property.

On the other hand, it is well-known that a non-overlapping left-linear Term Rewriting System (TRS) has the Church-Rosser property. Without left-linearity and with a slight modification of the non-overlap requirement, some results have concluded the unique normal form property of TRSs. The unique normal form property is a sufficient condition for consistency of the system and weaker than the Church-Rosser property. In this paper we extend one of these results to pattern HORSs. The main theorem states that ``a strongly non-overlapping pattern HORS has the unique normal form property''.

To do that, we introduce the notion of Context-Conditional Linearisation (CCL) of HORSs, and give a sufficient condition for the Church-Rosser property of CCL systems.

Abstractions of uniform proofs

by Paolo Volpe
Abstract:

In this paper we analyze a framework for abstract interpretation of programs written in abstract logic programming languages in the sense of Miller et al. . The framework is based on the sequent calculus formulation of the class of considered languages. Two systems of inductive definitions to model the bottom-up and the top-down constructions of proof trees in a sequent system are introduced. These constructions are then abstracted on domains in which a possible less precise yet correct description of computations is given. In the abstract domain, the meaning of a program is still characterized by sets of inference rules and by the induced operators. Anyway the abstract operators we define this way are the most precise approximations of the concrete ones.
Some properties of the abstraction function with respect to the sequent system are given that allow to restate in the abstract domain the equivalence of the bottom-up and top-down approaches and the compositionality of the semantic operators.

Heterogeneous Constraint Solving

by Frederic Benhamou
Abstract:

Most CLP languages designed in the past few years feature at least some combination of constraint solving capabilities. These combinations can take multiple forms since they achieve either the mixing of different domains or the use of different algorithms over the same domain. These solvers are also very different in nature. Some of them perform complete constraint solving while others are based on propagation methods. This paper is an attempt to design a unified framework describing the cooperation of constraint solving methods. Most techniques used in constraint-based systems are shown to be implementations of operators called constraint narrowing operators. A generalized notion of arc-consistency, called weak arc-consistency is proposed and is used to model heterogeneous constraint solving. We provide conditions on the constraint solving algorithms which guarantee termination, correctness and confluence of the resulting combined solver. This framework is shown to be general enough to describe the operational semantics of the basic constraint solving mechanisms in a number of current CLP systems.

Order-sorted Termination: the Unsorted Way

by Peter C. Olveczky and Olav Lysne
Abstract:

We consider the problem of proving termination of order-sorted rewrite systems. The dominating method for proving termination of order-sorted systems has been to simply ignore sort information, and use the techniques developed for unsorted rewriting. The problem with this approach is that many order-sorted rewrite systems terminate because of the structure of the set of sorts. In these cases the corresponding unsorted system would not terminate.

In this paper we approach the problem of order-sorted termination by mapping the order-sorted rewrite system into an unsorted one such that termination of the latter implies termination of the former. By encoding sort information into the unsorted mapping, we are able to use general purpose termination orderings to prove termination of order-sorted rewrite systems whose termination depend on the sort hierarchy. We present a sequence of gradually stronger methods, and show that a previously published method is contained in ours as a special case.

A Strict Border for the Decidability of E-Unification for Recursive Functions

by Heinz Fassbender and Sebastian Maneth
Abstract:

During the execution of functional logic programs, E-unification problems have to be solved quite frequently, where the underlying equational theory is induced by recursive functions. But, what about the decidability of those E-unification problems? Up to now, there does not exist a concrete answer to this question. In this paper, we answer this question by drawing and verifying a strict border between undecidability and decidability of E-unification problems for particular classes of recursive functions. By this border, the existing approaches in implementing those E-unification problems will be justified in the case of undecidability or, otherwise, improvements may be suggested.

A Language for the Logical Specification of Processes and Relations

by Luis Caires
Abstract:

Due to its ability to handle resources in a finely controlled way, linear logic is being adopted as a foundation of several logic programming and specification languages in which some notions of state can be modelled. In particular, some were proposed with the main motivation of allowing the specification of concurrent systems. Such systems incorporate small subsets of linear logic or have operational interpretations that exclude the ``don't know'' search behaviour expected from a logic programming language. On the other hand, systems incorporating larger subsets of linear logic must pay their expressiveness with a greater operational complexity. In this paper, we present LC, a simple language that combines, in a uniform way, the reduction and state-oriented style of specification expected from a concurrent process calculus, with the more declarative and relational style of specification usual in logic programming. We will also show that LC is an expressive language both as a logic programming and as a process specification language.

Independence in Dynamically Scheduled Logic Languages

by M. Garcia de la Banda, M. Hermenegildo, and K. Marriott
Abstract:

The notion of {\em independence} is useful in conventional logic programming as the basis for several optimizations, including program parallelization, intelligent backtracking, and goal reordering. In this paper we extend this notion to deal with dynamic scheduling. This type of scheduling, in which some calls are dynamically ``delayed'' until their arguments are sufficiently instantiated, is currently provided in most real languages because it offers advantages both in terms of programming power and declarativeness. We focus on the notion of independence required for ensuring correctness, completeness, and efficiency of parallelization within the independent and-parallel model. We first show that traditional concepts of independence are not useful in this context. We then revisit the notion of search space preservation, and prove that it is not only sufficient but also necessary for ensuring the correctness, completeness, and efficiency of parallel execution. We also show that space preservation is equivalent to previously proposed independence notions for (constraint) logic programs. We then discuss search space preservation in the context of dynamically scheduled languages and, based on it, extend the concept of independence to this context. Finally we also provide sufficient conditions for independence which can be evaluated ``a-priori'' (i.e., at run-time), as is needed in many practical applications.

On Negation As Instantiation

by W. Drabent, Alessandra Di Pierro
Abstract:

Given a logic program $P$ and a goal $G$, we introduce a notion which states when an SLD--tree for $P\cup\{G\}$ instantiates a set of variable $V$ with respect to another one, $*$. We call this notion weak instantiation, as it is a generalization of the instantiation property introduced in [3]. A negation rule based on instantiation, the so--called Negation As Instantiation rule (NAI), allows for inferring existentially closed negative queries, that is formulas of the form $\exists\not Q$ from logic programs. We show that, by using the new notion, we can infer a larger class of negative queries, namely the class of the queries of the form $\forall{}w\exists{}v\not{}Q$ and of the form $\forall{}w\exists{}v\forall{}z\not{}Q$, where $z$ is the set of the remaining variables of $Q$.

An Algebraic Approach to Mixins and Modularity

by Davide Ancona and Elena Zucca
Abstract:

We present an algebraic formalization of the notion of {\em mixin module\/}, i.e.\ a module where the definition of some components is {\em deferred\/}. Moreover, we define a set of basic operators for composing mixin modules, intended to be a kernel language with clean semantics in which to express more complex operators of existing modular languages, including variants of inheritance in object oriented programming. The semantics of the operators is given in an ``institution independent'' way, i.e.\ is parameterized on the semantic framework modeling features of the underlying core language.

Lambda-calculi with explicit substitutions and composition which preserve beta-strong normalization

by Conceicao Ferreira, Delia Kesner and Laurence Puel
Abstract:

This paper studies preservation of $\beta$--strong normalization by two different confluent $\lambda$--calculi with explicit substitutions defined in [14]; the particularity of these calculi, called $\lambda_d$-- and $\lambda_{dn}$ resp., is that both have a composition operator for substitutions. We develop an abstract simulation technique allowing to reduce preservation of $\beta$--strong normalization of one calculus to that of another one, and apply said technique to reduce preservation of $\beta$--strong normalization of $\lambda_d$ and $\lambda_{dn}$ to that of $\lambda_f$, another calculus having no composition operator. Then, preservation of $\beta$--strong normalization of $\lambda_f$ is shown using the same technique as in [2]. As a consequence, $\lambda_d$ and $\lambda_{dn}$ become the first $\lambda$--calculi with explicit substitutions having composition and preserving $\beta$--strong normalization. As an aside, we also apply our technique to reduce preservation of $\beta$--strong normalization of the calculus $\lambda_v$ in [19] to that of $\lambda_f$.

Algebraic Semantics for Functional Logic Programming with Polymorphic Order-Sorted Types

by J. M. Almendros-Jimenez,A. Gavilantes-Franco,A. Gil-Luezas
Abstract:

In this paper we present the semantics of a functional logic language with parametric and order-sorted polymorphism. Typed programs consist of a type specification, a polymorphic signature and a set of constructor-based conditional rewriting rules for whi ch we define a semantic calculus. The denotational semantics of the language is based on Scott domains interpreting constructors and functions by monotonic and continuous mappings, respectively, in every instance of the declared type. We prove initiality results for the free ground term algebra. We also prove that the free term algebra with variables is freely generated in the category of models. The semantic calculus is proved to be sound and complete w.r.t. the denotational semantics. As in logic progr amming, we define the immediate consequence operator, proving that the Hebrand model is the least model of a program.

Standardization Theorem Revisited

by Taro Suzuki
Abstract:

Standardization theorem for TRSs was first discussed by Huet and L\'{e}vy for orthogonal TRSs, and later extended by Boudol for left-linear TRSs. In this paper we show the standardization of a given rewrite sequence can be seen as the rewriting in an abstract rewriting system. In this viewpoint, standardization theorem results in the proof of completeness, i.e., termination and confluence, of the ARS. We give a new proof of standardization theorem based on this view. Furthermore, we also consider a standardization theorem for conditional term rewriting systems.

A Hierarchy of Semantics for Normal Constraint Logic Programs

by Francois Fages, Roberta Gori
Abstract:

The different properties characterizing the operational behavior of logic programs can be organized in a hierarchy of fixpoint semantics related by Galois insertions, having the least Herbrand model as most abstract semantics, and the SLD operational semantics as most concrete semantics. The choice of a semantics in the hierarchy allows to model precisely the program properties of interest while getting rid of useless details of too concrete semantics.

The aim of this paper is to push forward these methods by making them apply to normal (constraint) logic programs, that is full first-order (non Horn) programs. The fixpoint semantics defined by the first author for the rule of constructive negation by pruning is at the center of the hierarchy developed in this paper. We show that that semantics can be obtained by concretization of Kunen's semantics defined as a fixpoint, taken as the most abstract semantics of the hierarchy, and that by further concretization it leads to a new operational semantics for normal CLP programs. The different observable properties of the program, such as successful derivations, finite failure, set of computed answer constraints, etc. are modeled by precise semantics in the hierarchy.

Complementing Logic Program Semantics

by Gilberto File, Roberto Giacobazzi and Francesco Ranzato
Abstract:

We consider abstract interpretation, and in particular the basic operators of reduced product and complementation of abstract domains, to systematically derive denotational semantics by composition and decomposition. Reduced product allows to perform the logical conjunction of semantics, while complementation characterizes precisely what is left from a semantics when the information concerning a given observable property is ``subtracted'' from it. We apply this idea to the case of logic programming, characterizing in a uniform algebraic setting, the interaction between a number of well known declarative semantics for logic programs.

Discrete Normalization and Standardization in Deterministic Residual Structures

by Zurab Khasidashvili and John Glauert
Abstract:

We prove a version of the Standardization Theorem and the Discrete Normalization (DN) Theorem in stable semi-linear Deterministic Residual Structures, which are Abstract Reduction Systems with axiomatized residual relation, and model orthogonal rewrite systems. The latter theorem gives an algorithm for construction of reductions Le'vy-equivalent (or permutation-equivalent) to a given, finite or infinite, reduction. This and other results of this paper add to the understanding of Le'vy-equivalence of reductions, and consequently, Le'vy's reduction space. The importance of the latter is already well-understood, and the substantiate it further by demonstrating how elements of this space can be used to give denotational semantics of known functional languages in an abstract manner. Since functional programming languages are given with (often orthogonal) rewrite systems and deterministic reduction strategies, a value is associated to a program via a finite or infinite reduction computed by that strategy. And our DN theorem gives characterization of all reductions computing the same value. Similar arguments apply to several logic based languages and proof procedures (e.g., to the narrowing

A Process Algebra for Synchronous Concurrent Constraint Programming

by Lubos Brim, Jean-Marie Jacquet, Mojmir Kretinsky and David Gilbert
Abstract:

Concurrent constraint programming is classically based on asynchronous communication via a shared store. Synchrony can be achieved by forcing concurrently running ask and tell primitives to synchronise on ``new common information''. This paper outlines this framework, called scc, and develops an algebraic semantics for it.

The scc framework is shown to share similarities with both the traditional concurrent constraint setting and algebraic languages like CCS but also to have major differences which requires the use of new techniques in formulating the algebraic semantics. Among these are the introduction of an auxiliary communication operator to handle the treatment of synchrony and the extension of the concept of cylindric algebras by allowing the hiding of the empty set of variables in order to permit local computations. More importantly, new axioms have been introduced to describe our variants of the tell and ask primitives.

The algebraic semantics is proved to be sound and complete with respect to a compositional operational semantics which is also presented in the paper.