John P. Gallagher

LOPSTR Conference 2023 Conference Paper

Transforming Big-Step to Small-Step Semantics Using Interpreter Specialisation

• John P. Gallagher
• Manuel V. Hermenegildo
• José F. Morales 0001
• Pedro López-García 0001

Abstract Natural semantics (big-step) and structural operational semantics (small-step) each have advantages, so it can be useful to produce both semantic forms for a language. Previous work has shown that big-step semantics can be transformed to small-step semantics. This is also the goal of our work, but our main contribution is to show that this can be done by specialisation of an interpreter that imposes a small-step execution on big-step transition rules. This is arguably more direct, transparent and flexible than previous methods. The paper contains two examples and further examples are available in an online repository.

LOPSTR Conference 2019 Conference Paper

A General Framework for Static Cost Analysis of Parallel Logic Programs

• Maximiliano Klemen
• Pedro López-García 0001
• John P. Gallagher
• José F. Morales 0001
• Manuel V. Hermenegildo

Abstract The estimation and control of resource usage is now an important challenge in an increasing number of computing systems. In particular, requirements on timing and energy arise in a wide variety of applications such as internet of things, cloud computing, health, transportation, and robots. At the same time, parallel computing, with (heterogeneous) multi-core platforms in particular, has become the dominant paradigm in computer architecture. Predicting resource usage on such platforms poses a difficult challenge. Most work on static resource analysis has focused on sequential programs, and relatively little progress has been made on the analysis of parallel programs, or more specifically on parallel logic programs. We propose a novel, general, and flexible framework for setting up cost equations/relations which can be instantiated for performing resource usage analysis of parallel logic programs for a wide range of resources, platforms, and execution models. The analysis estimates both lower and upper bounds on the resource usage of a parallel program (without executing it) as functions on input data sizes. In addition, it also infers other meaningful information to better exploit and assess the potential and actual parallelism of a system. We develop a method for solving cost relations involving the max function that arise in the analysis of parallel programs. Finally, we instantiate our general framework for the analysis of logic programs with Independent And-Parallelism, report on an implementation within the CiaoPP system, and provide some experimental results. To our knowledge, this is the first approach to the cost analysis of parallel logic programs.

LOPSTR Conference 2011 Conference Paper

Analysis of Logic Programs Using Regular Tree Languages - (Extended Abstract)

• John P. Gallagher

Abstract The field of finite tree automata provides fundamental notations and tools for reasoning about sets of terms called regular or recognizable tree languages. We consider two kinds of analysis using regular tree languages, applied to logic programs. The first approach is to try to discover automatically a tree automaton from a logic program, approximating its minimal Herbrand model. In this case the input for the analysis is a program, and the output is a tree automaton. The second approach is to expose or check properties of the program that can be expressed by a given tree automaton. The input to the analysis is a program and a tree automaton, and the output is an abstract model of the program. These two contrasting abstract interpretations can be used in a wide range of analysis and verification problems.

LOPSTR Conference 2008 Conference Paper

Analysis of Linear Hybrid Systems in CLP

• Gourinath Banda
• John P. Gallagher

Abstract In this paper we present a procedure for representing the semantics of linear hybrid automata (LHAs) as constraint logic programs (CLP); flexible and accurate analysis and verification of LHAs can then be performed using generic CLP analysis and transformation tools. LHAs provide an expressive notation for specifying real-time systems. The main contributions are (i) a technique for capturing the reachable states of the continuously changing state variables of the LHA as CLP constraints; (ii) a way of representing events in the LHA as constraints in CLP, along with a product construction on the CLP representation including synchronisation on shared events; (iii) a framework in which various kinds of reasoning about an LHA can be flexibly performed by combining standard CLP transformation and analysis techniques. We give experimental results to support the usefulness of the approach and argue that we contribute to the general field of using static analysis tools for verification.

LPAR Conference 2008 Conference Paper

Approximating Term Rewriting Systems: A Horn Clause Specification and Its Implementation

• John P. Gallagher
• Mads Rosendahl

Abstract We present a technique for approximating the set of reachable terms of a given term rewriting system starting from a given initial regular set of terms. The technique is based on previous work by other authors with the same goal, and yields a finite tree automaton recognising an over-approximation of the set of reachable terms. Our contributions are, firstly, to use Horn clauses to specify the transitions of a possibly infinite-state tree automaton defining (at least) the reachable terms. Apart from being a clear specification, the Horn clause model is the basis for further automatic approximations using standard logic program analysis techniques, yielding finite-state tree automata. The approximations are applied in two stages: first a regular approximation of the model of the given Horn clauses is constructed, and secondly a more precise relational abstraction is built using the first approximation. The analysis uses efficient representations based on BDDs, leading to more scalable implementations. We report on preliminary experimental results.

LOPSTR Conference 2008 Conference Paper

From Monomorphic to Polymorphic Well-Typings and Beyond

• Tom Schrijvers
• Maurice Bruynooghe
• John P. Gallagher

Abstract Type information has many applications; it can e. g. be used in optimized compilation, termination analysis and error detection. However, logic programs are typically untyped. A well-typed program has the property that it behaves identically on well-typed goals with or without type checking. Hence the automatic inference of a well-typing is worthwhile. Existing inferences are either cheap and inaccurate, or accurate and expensive. By giving up the requirement that all calls to a predicate have types that are instances of a unique polymorphic type but instead allowing multiple polymorphic typings for the same predicate, we obtain a novel strongly-connected-component-based analysis that provides a good compromise between accuracy and computational cost.

LOPSTR Conference 2007 Conference Paper

Type-Based Homeomorphic Embedding and Its Applications to Online Partial Evaluation

• Elvira Albert
• John P. Gallagher
• Miguel Gómez-Zamalloa
• Germán Puebla

Abstract Homeomorphic Embedding ( HEm ) has proven to be very powerful for supervising termination of computations, provided that such computations are performed over a finite signature, i. e. , the number of constants and function symbols involved is finite. However, there are situations, for example numeric computations, which involve an infinite (or too large) signature, in which HEm does not guarantee termination. Some extensions to HEm for the case of infinite signatures have been proposed which guarantee termination, but they either do not provide systematic means for generating such extensions or the extensions are too simplistic and do not produce the expected results in practice. We introduce Type-based Homeomorphic Embedding ( TbHEm ) as an extension of the standard, untyped HEm to deal with infinite signatures. In the paper, we show how TbHEm can be used to improve the accuracy of online partial evaluation. For this purpose, we propose an approach to constructing suitable types for partial evaluation automatically based on existing analysis tools for constraint logic programs. We also present useful properties of types which allow us to take full advantage of TbHEm in practice. Experimental results are reported which show that our work improves the state of the practice of online partial evaluation.

LOPSTR Conference 2005 Conference Paper

Converting One Type-Based Abstract Domain to Another

• John P. Gallagher
• Germán Puebla
• Elvira Albert

Abstract The specific problem that motivates this paper is how to obtain abstract descriptions of the meanings of imported predicates (such as built-ins) that can be used when analysing a module of a logic program with respect to some abstract domain. We assume that abstract descriptions of the imported predicates are available in terms of some “standard” assertions. The first task is to define an abstract domain corresponding to the assertions for a given module and express the descriptions as objects in that domain. Following that they are automatically transformed into the analysis domain of interest. We develop a method which has been applied in order to generate call and success patterns from the CiaoPP assertions for built-ins, for any given regular type-based domain. In the paper we present the method as an instance of the more general problem of mapping elements of one abstract domain to another, with as little loss in precision as possible.

LOPSTR Conference 2005 Conference Paper

Non-leftmost Unfolding in Partial Evaluation of Logic Programs with Impure Predicates

• Elvira Albert
• Germán Puebla
• John P. Gallagher

Abstract Partial evaluation of logic programs which contain impure predicates poses non-trivial challenges. Impure predicates include those which produce side-effects, raise errors (or exceptions), and those whose truth value varies according to the degree of instantiation of arguments. In particular, non-leftmost unfolding steps can produce incorrect results since the independence of the computation rule no longer holds in the presence of impure predicates. Existing proposals allow non-leftmost unfolding steps, but at the cost of accuracy: bindings and failure are not propagated backwards to predicates which are potentially impure. In this work we propose a partial evaluation scheme which substantially reduces the situations in which such backpropagation has to be avoided. With this aim, our partial evaluator takes into account the information about purity of predicates expressed in terms of assertions. This allows some optimizations which are not feasible using existing partial evaluation techniques. We argue that our proposal goes beyond existing ones in that it is a) accurate, since the classification of pure vs impure is done at the level of atoms instead of predicates, b) extensible, as the information about purity can be added to programs using assertions without having to modify the partial evaluator itself, and c) automatic, since (backwards) analysis can be used to automatically infer the required assertions. Our approach has been implemented in the context of CiaoPP, the abstract interpretation-based preprocessor of the Ciao logic programming system.

LOPSTR Conference 2004 Conference Paper

Fully Automatic Binding-Time Analysis for Prolog

• Stephen-John Craig
• John P. Gallagher
• Michael Leuschel
• Kim S. Henriksen

Abstract Offline partial evaluation techniques rely on an annotated version of the source program to control the specialisation process. These annotations guide the specialisation and ensure the termination of the partial evaluation. We present an algorithm for generating these annotations automatically. The algorithm uses state-of-the-art termination analysis techniques, combined with a new type-based abstract interpretation for propagating the binding types. This algorithm has been implemented as part of the logen partial evaluation system, along with a graphical annotation visualiser and editor, and we report on the performance of the algorithm for a series of benchmarks.

LOPSTR Conference 2003 Conference Paper

A Program Transformation for Backwards Analysis of Logic Programs

• John P. Gallagher

Abstract The input to backwards analysis is a program together with properties that are required to hold at given program points. The purpose of the analysis is to derive initial goals or pre-conditions that guarantee that, when the program is executed, the given properties hold. The solution for logic programs presented here is based on a transformation of the input program, which makes explicit the dependencies of the given program points on the initial goals. The transformation is derived from the resultants semantics of logic programs. The transformed program is then analysed using a standard abstract interpretation. The required pre-conditions on initial goals can be deduced from the analysis results without a further fixpoint computation. For the modes backwards analysis problem, this approach gives the same results as previous work, but requires only a standard abstract interpretation framework and no special properties of the abstract domain.

LOPSTR Conference 2002 Conference Paper

Convex Hull Abstractions in Specialization of CLP Programs

• Julio C. Peralta
• John P. Gallagher

Abstract We introduce an abstract domain consisting of atomic formulas constrained by linear arithmetic constraints (or convex hulls). This domain is used in an algorithm for specialization of constraint logic programs. The algorithm incorporates in a single phase both top-down goal directed propagation and bottom-up answer propagation, and uses a widening on the convex hull domain to ensure termination. We give examples to show the precision gained by this approach over other methods in the literature for specializing constraint logic programs. The specialization method can also be used for ordinary logic programs containing arithmetic, as well as constraint logic programs. Assignments, inequalities and equalities with arithmetic expressions can be interpreted as constraints during specialization, thus increasing the amount of specialization that can be achieved.

LOPSTR Conference 2000 Conference Paper

Imperative Program Specialisation: An Approach Using CLP

• Julio C. Peralta
• John P. Gallagher

Abstract The semantics of an imperative programming language can be expressed as a program in a declarative constraint language. Not only does this render the semantics executable, but it opens up the possibility of applying to imperative languages the advances made in program analysis and transformation of declarative languages. We propose a method for carrying out partial evaluation of imperative programs, using partial evaluation in a declarative language, but returning the results in the syntax of the imperative program which is to be partially evaluated. The approach uses a special form of the semantics and program points to aid partial evaluation. The partially evaluated semantics program is represented as a labelled directed graph. An algorithm for reconstructing an imperative program from the graph and the residual program is presented. Constraints provide a means through which information is propagated inside both branches of a conditional, the body of a loop, and along def-use chains in the program. The method provides a framework for constructing a partial evaluator for any imperative programming language, by writing down its semantics as a declarative program (a constraint logic program, in the approach shown here).

LOPSTR Conference 1998 Conference Paper

Constrained Regular Approximation of Logic Programs

• Hüseyin Saglam
• John P. Gallagher

Abstract Regular approximation is a well-known and useful analysis technique for conventional logic programming. Given the existence of constraint solving techniques, one may wish to obtain more precise approximations of programs while retaining the decidable properties of the approximation. Greater precision could increase the effectiveness of applications that make use of regular approximation, such as the detection of useless clauses and type analysis. In this paper, we introduce arithmetic constraints, based on convex polyhedra, into regular approximation. In addition, Herbrand constraints can be introduced to capture dependencies among arguments.

LOPSTR Conference 1998 Conference Paper

Constraint-Based Partial Evaluation of Rewriting-Based Functional Logic Programs

• Laura Lafave
• John P. Gallagher

Abstract The aim of this work is to describe a procedure for the partial evaluation of functional logic programs in rewriting-based languages using constraint-based information propagation. The constraint-based partial evaluation algorithm incorporated with local and global control describes a KMP partial evaluator. Results from the implementation of the partial evaluator in the functional logic language Escher show that the algorithm is also able to perform intermediate list elimination. Renaming operations and termination and correctness properties are presented. Finally, extensions of the constraint-based procedure which may lead to greater specialisation are discussed.

LOPSTR Conference 1994 Conference Paper

A Transformation System for Definite Programs Based on Termination Analysis

• J. Cook
• John P. Gallagher

Abstract We present a goal replacement rule whose main applicability condition is based on termination properties of the resulting transformed program. The goal replacement rule together with a multi-step unfolding rule forms a powerful and elegant transformation system for definite programs. It also sheds new light on the relationship between folding and goal replacement, and between different folding rules. Our explicit termination condition contrasts with other transformation systems in the literature, which contain conditions on folding and goal replacement, often rather complex, in order to avoid “introducing a loop” into a program. We prove that the goal replacement rule preserves the success set of a definite program. We define an extended version of goal replacement that also preserves the finite failure set. A powerful folding rule can be constructed as a special case of goal replacement, allowing folding with recursive rules, with no distinction between old and new predicates. A proof that Seki's transformation system preserves recurrence, an important termination property, is outlined.

LOPSTR Conference 1994 Conference Paper

Schema-Based Top-Down Design of Logic Programs Using Abstract Data Types

• Emmanuil I. Marakakis
• John P. Gallagher

Abstract This paper presents a set of schemata that support stepwise top-down design of logic programs using abstract data types (ADTs). There are thus three main components to this approach: top-down design, program schemata and ADTs, all of which are already well established notions. Our aim is to combine these ideas in a framework, amenable to support by design tools and allowing the use of existing logic program transformation techniques to optimise the final programs.

LOPSTR Conference 1993 Conference Paper

Deletion of Redundant Unary Type Predicates from Logic Programs

• John P. Gallagher
• D. Andre de Waal

Abstract In this paper, program transformation is proposed as a way of handling type information efficiently. A typed program is translated to an untyped program, with regular unary predicates replacing the types, and then an attempt is made to eliminate as many of the unary type literals as possible. The method is as follows: first a query-answer transformation of the program with a given goal is made. This gives a specification of the calls to each literal in the program arising in the computation of the goal. The set of calls defines the context of the literal in the computation. Any literal can be eliminated if its answers are implied by its context. We define a procedure for eliminating literals defined by regular programs, a class which includes the type literals. A regular approximation of the query-answer program is made, and then decidable properties of regular programs are used to check for the elimination of the literal. The method can be compared with type-checking, since the elimination procedure also shows whether some type literal fails, indicating a “badly-typed” clause. Our aim however is not to construct a type system, but rather to show that simple types can be handled using a general framework of program analysis and transformation.

LOPSTR Conference 1992 Conference Paper

Specialisation of a Unification Algorithm

• D. Andre de Waal
• John P. Gallagher

Abstract Automatically specialising an algorithm for unification is a challenge to current techniques for partial evaluation. In this paper a study is made of several specialisations of unification that are typically needed. The limitations of existing partial evaluation techniques are examined and proposals for extensions are made. Partial evaluation is modified by adding condition goals which are used to evaluate or prune more of the computation tree than is possible with partial evaluation alone. It is shown that abstract substitutions can be introduced to allow information from infinite computation trees to be exploited. If infinite failures are removed from the computation tree the resulting specialised program does not preserve the procedural semantics given by SLDNF (which defines negation by finite failure). There is a short discussion on correctness results for such specialisations.

ECAI Conference 1987 Conference Paper

Transforming Logic Programs by Specialising Interpreters

• John P. Gallagher