Dr. Peter Schachte
Department of Computing and Information Systems
The University of Melbourne
Doug McDonell Building
Parkville Campus, University of Melbourne
I regularly teach the following subjects:
I am currently supervising the following research postgraduate students:
I am a member of the Declarative Language Group at the University of Melbourne. I am currently investigating the efficient static analysis of logic programs, particularly Prolog programs, using abstract interpretation. Abstract interpretation is a provably sound semantics-based program analysis technique which works by interpreting the program to be analyzed using an abstraction of the data that will be used when the program is really run.
My publication list shows my past research. Also see Michael Ley's DBLP Bibliography Server for an index of my publications.
My current research projects, ranging from complete but not yet written up to highly speculative and not yet begun, include:
In the area of abstract interpretation, I am interested in:
Incremental abstract interpretation
Abstract interpretation is a global static analysis technique; in general, this means that all of an applications source code must be analyzed at once. It would be impractical for a compiler to process every source file every time the smallest change is made to one of them, so it is important to find a way to avoid as much reanalysis as possible.
One approach has been suggested. Another promising approach involves using condensing analysis domains domains which do not lose precision when a predicate is analyzed independently of how it will be called, and that information is combined with information about an invocation of that predicate to determine the state after that invocation. Incrementally reanalyzing a program becomes easy with such a domain, because the goal independent analysis of a predicate cannot change unless the its code, or the analysis of a predicate it calls, has changed, and the goal dependent analysis of a predicate need not be repeated unless the goal independent analysis of a predicate it calls, or the goal dependent analysis of a predicate that calls it, has changed. By performing the analysis in these two phases, we can easily minimize the analysis we must repeat.
Currently, the only known non-trivial condensing analysis domain is the Pos domain for groundness analysis. Clearly other practical condensing domains must be found before an analysis methodology can be built around condensation! Ideally, a practical method of finding condensing domains should be found. A recent paper shows how to build condensing domains, but it is not clear that this method is practical.
Boolean functions (propositional logic formulae), or subclasses of them, are a useful abstraction for representing information about dependencies among boolean-valued variables. They certainly are effective for groundness analysis. And since most of the time in program analysis is spent manipulating abstract values, being able to efficiently manipulate boolean functions is very important.
GER is a hybrid representation for Boolean functions that separates out variables that are definitely true (and maybe those that are definitely false), equivalence classes of equivalent variables (and perhaps classes of exclusive variables), from other information. The idea is to use the most efficient representation for each class of information. Implementation has shown this representation to be significantly more efficient than the standard ROBDD representation. However, opportunities remain for further improvement, including improving the algorithms used and factoring out more information that can be represented more efficiently.
Improved ROBDD algorithms
Even using the GER representation, performance of ROBDD operations is the dominant factor determining analysis performance. We have shown that specialized ROBDD operations can significantly improve groundness analysis performance. More such optimizations can be made.
Controlled Impurity in Logic Programming
Practical purely declarative programming languages must provide an interface to existing code written in imperative languages. Until it is practical to prove the purity of foreign code, this creates the possibility that impurity will leak from the foreign code into the (supposedly) declarative program.
Of course, it is possible to write pure code using impure facilities (ultimately, all declarative code is implemented that way). However, most pure languages take the attitude that the programmer must construct her pure primitives wholly outside the pure language, using the foreign interface only to interface to pure primitives. Often, though, it would be more convenient to implement parts of the pure facility in the declarative language, using impure primitives through the foreign interface. Generally, the only alternative is to understand the implementation of the declarative language well enough to predict how it will handle impure primitives that are permitted to cross the foreign interface. This is highly undesirable, as the implementation details of the language may change, or the program may need to be ported to another implementation of the same language. If you lie to the compiler, it will eventually have its revenge.
Mercury solves this problem by requiring users to indicate which primitives made available through its foreign interface are pure and which are not. A predicate may invoke impure operations provided it is declared impure, or it is promised to be pure. The Mercury compiler is not permitted to perform certain kinds of optimizations on impure parts of a predicate, assuring the user that, although it uses impure primitives, her predicate will behave as intended.
New Mode System
Mercury uses a mode system that requires the user to specify each allowable call pattern of argument instantiations and the corresponding result pattern. Additionally, the user must specify the determinism of each mode. A major shortcoming of this approach is that the user of a predicate will not be able to use any mode that its author did not anticipate. Another shortcoming of the current approach is that it reorders code minimally to meet the declared determinism. Perhaps a more efficient implementation of the predicate could be created with more aggressive reordering. And in any case, the current mode system discourages predicates with multiple modes.
An alternative approach would be to specify the instantiation dependencies of predicates, instead of what Mercury calls modes. One might declare the mode of append/3 by specifying that the backbone of the third argument is bound iff the backbones of both of the other arguments are bound, and likewise the elements of the lists. This says all that is needed for mode analysis of a call to append/3.
I would argue that this style of mode system could be less verbose than the current system, and at least as natural. One thing this would not provide, though, is a list of the modes for each predicate that the compiler should generate code for. Ideally, code for different modes of a predicate would be generated on demand.
Sequence quantification is a refinement of bounded quantification, which has been well studied. The improvement over bounded quantification lies in giving users the ability to define new ranges to quantify over. By carefully constructing the mechanism for users to define new sequences, we are able to provide much of the power of looping constructs in conventional languages such as C or PASCAL.
Sequence Quantification can be implemented with a few very simple higher order predicates and a few user-extensible predicates defining the kinds of sequences that can be quantified over. However, this implementation gives poor performance. To get high performance, specialized versions of these predicates need to be created for each invocation. Doing this sort of specialization without accidentally slowing the code down in some cases is rather difficult. Doing it with acceptable (or even just finite) compilation times can be tricky.
A declarative approach to programming, and to software design, has much to contribute to software engineering. However, the software engineering community appears uninterested in declarative languages. Conversely, the declarative language community is largely uninterested in software engineering.
Declarative Software Design Methodology
A software design methodology oriented towards declarative implementation is needed. Ideally it would build on an existing methodology, preferably based on UML due to its popularity. Probably many of the existing UML diagrams would be equally applicable to declarative development. Even class diagrams would be applicable, though inheritance may be less desirable.
Some of the freely-distributable software I have written is available for download.
I am available for consulting jobs. See my curriculum vitae for my work experience.