Pat Hill and Andy King

This is a project whose aims are: to investigate techniques for determinacy analysis that will improve the performance of logic programming, and to build practical tools using these techniques that can be interfaced with a variety of logic programming systems. It is a project between the Universities of Leeds and Kent, supported by EPSRC, the UK Research Council for Science and Engineering, and jointly managed by Dr Andy King (Kent) and Dr Pat Hill (Leeds). There are two research fellows working for the project, Jan-Georg Smaus at Kent and Dr Andrew Heaton at Leeds although, currently, Andrew Heaton is taking a three month break from the project and visiting Dr Michael Codish at Ben-Gurion University. The industrial collaborator is IF Computer GmbH who has agreed to provide industrial Prolog programs for the purposes of assessment and tuning. We are also discussing our results with Logic Programming Associates (LPA). The project started in early in 1996 and finishes in 1998.

We are particularly interested in developing analysis tools for modern logic programming languages which allow for constraints (and hence, co-routining) and types. Constraints are now available and widely used with the main Prolog systems such as SICStus Prolog and IF/Prolog, while the Goedel and Mercury programming languages have illustrated the benefits of having types in the language.

The key to analysing programs for determinacy is the detection of the modes with which the predicates are used [hill-king:jpl]. However, mode analysis in the presence of co-routining is hard and previously the methods have either lacked precision or were very inefficient (compared to methods for programs without co-routining). We have been studying this problem and found a nice solution which is essentially very simple and easy to implement. We now have an efficient analyser which can detect the call patterns of variables at the different program points but whose precision is, in the main, largely unaffected by the possible co-routining behaviour. This work was presented at LOPSTR'97 and the full paper (submitted for publishing in the post-conference proceedings) is available as a technical report from Leeds [heaton-hill-king:lopstr97].

The precision of an analyser depends, to a large extent, on the precision of the abstract domain itself. In Prolog, the lack of adequate information about the intended types of the arguments to the predicates makes it difficult to provide a domain that is precise for all situations. The exception to this is with lists and list processing predicates. It has already been shown how, having a suitable domain just for lists, the analyser can detect at which points in the computation a list will be nil-terminated. (Nil-termination has ben shown to be important for determinacy and termination analysis.) We have devised a procedure that can automatically define and construct specialised domains for each type in a typed logic programming [smaus-hill-king:iclp97, smaus-hill-king:tech97]. These domains can then capture the modes of subterms to any required level of precision. Moreover, if these types are recursive (as for a list) then the domain can capture a termination property (corresponding to nil-termination for lists) of terms with that type.

In April, we held a workshop at Leeds called "Constraint Programming for Reasoning about Programming". This was a combined event, organised by Kent and Leeds together with the Bristol logic programming group led by Dr John Gallagher. Compulog Net supported us, enabling Dr Michael Codish and Dr Mark Wallace to join us and give invited talks. The event was a success and proved a good forum for discussion and informal presentations for both students and experienced researchers alike. Details including the names of participants and papers presented can be found at http://www.scs.leeds.ac.uk/hill/cpp97.html.

Other projects at Leeds and Kent are contributing both directly and indirectly to this project. At Kent, a Nuffield Foundation award has led to an implementation technique for inferring argument size relations which are particularly useful in termination [benoy-king96] and time-complexity analysis [king-shen-benoy97]. We have also studied how typed logic programs, such as Goedel programs, can be used to define the norms that specify how argument size should be measured [king-martin-soper:lopstr96]. One application of this work is on control generation. Joint work with Southampton has shown how termination analysis can be applied in in control generation [king-martin:tapsoft97] to automatically deduce control that is both efficient (in that co-routining is permitted) and correct (in that program termination is guaranteed). Southampton is now taking this work forward by exploring the connection between control generation and partial evaluation. Kent is also collaborating with the University of Manchester on designing and implementing an analyser that infers lower-bounds on the time-complexity of a logic program [king-shen-benoy:ilps97]. This is useful in parallelisation to avoid spawning fine-grained processes. Other granularity control techniques are also being investigated [shen-costa-king:ilpsworkshop97].

At Leeds, a second EPSRC project entitled "Declarative Language Interface for Constraint Solving" started in January and Dr Roberto Bagnara has been working for the project. To support an easy to use interface for constraint solving, the compiler must be able to infer precise information about the flow of data in a program. CHINA is a data-flow analyser for constraint logic programming languages developed by Dr Bagnara as part of his PhD studies [bagnara:phdthesis]. Thus, we have continued with this work, improving and extending CHINA. A knowledge of variable aliasing is an important component of data-flow analysis and, with Enea Zaffenella (Modena), we are investigating the design of suitable procedures for capturing this information [bagnara-hill-zaffanella:sas97]. Another aspect of the work on constraints has been in the study of constraint logic languages. Antonio Fernandez, a PhD student with the Universidad di Malaga visited the group for three months, initiating an ongoing collaboration between Malaga and Leeds on CLP language design. As a first step in this work, we have made a comparative study of a large number of constraint languages comparing their expressiveness and efficiency [fernandez-hill:agp97].

Recently, Kent and Leeds have applied to EPSRC for funding for a new project entitled "Semantic-Based Software Support for Constraint Logic Programs". If this application is successful, we will research and develop the semantic-based technologies that will enable software support for constraint logic programming and also provide a set of experimental software support tools for the evaluation and demonstration of these technologies.

References

[bagnara:phdthesis] R. Bagnara, Data-Flow Analysis for Constraint Logic-Based Languages, Dipartimento di Informatica, Universita di Pisa, Report TD-1/97, 1997.

[bagnara-hill-zaffanella:sas97] R. Bagnara, P.M. Hill, E. Zaffanella, Set Sharing is Redundant for Pair Sharing, Proc. of the Int. Symp. on Static Analysis, LNCS 1302, Springer-Verlag, 1997.

[benoy-king96] F. Benoy, A. King, Inferring Argument Size Relationships with {CLP(R), Proc. of Logic Program Synthesis and Transformation 1996, LNCS 1207, Springer-Verlag, 1997.

[fernandez-hill:agp97] A. Fernandez, P. M. Hill, Finite Domain solvers compared using Self Referential Quizzes, School of Computer Studies, University of Leeds, Report 97.03, Presented at APPIA/GULP/PRODE'97.

[heaton-hill-king:lopstr97] A.J. Heaton, P.M. Hill, A. King, Analysing Logic Programs with Delay for Downward-closed Properties, School of Computer Studies, University of Leeds, Report 97.11, Presented at LOPSTR'97.

[hill-king:jpl] P.M. Hill, A. King, Determinacy and Determinacy Analysis, Journal of Programming languages, vol 5, pp 135-171, 1997.

[king-martin-soper:lopstr96] J. Martin, A. King, P. Soper, Typed Norms for Typed Logic Programs, Proc. of Logic Program Synthesis and Transformation, 1996, LNCS 1207, Springer-Verlag 1997.

[king-martin:tapsoft97] J. Martin and A. King, Generating Efficient, Terminating Logic Programs, TAPSOFT, 1997, Springer-Verlag, 1997.

[king-shen-benoy97] A. King, K. Shen and F. Benoy Lower-bound Time-complexity Analysis of Logic Programs, International Logic Programming Symposium, MIT Press, 1997.

[shen-costa-king:ilpsworkshop97] K Shen, V. Santos Costa and A. King A New Metric for Controlling Granularity for Parallel Execution Presented at the ILPS'97 post-conference workshop: Parallelism and Implementation Technology for Constraint Logic Programming Languages, 1997.