The Pattern Calculus
Associate Professor Barry Jay (Faculty of Information Technology, University of Technology Sydney)
CSL SEMINAR SERIESDATE: 2005-08-29
TIME: 11:20:00 - 12:05:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
The lambda-calculus provides a foundation for computation in which functions are treated uniformly but data structures are not. More precisely, although able to support operations such as the append of lists which are polymorphic in the data, operations such as searching and updating must be re-defined for each new structure. By contrast, these are uniformly defined in database query languages such as SQL and XML (and at least handled by object-orientation).
The pattern calculus provides a foundation for computation based on pattern-matching in which both functions and data structures are treated uniformly. The approach is able to support five forms of polymorphism in a single calculus, as compared to the one or two forms supported elsewhere. Ongoing research is showing how to answer SQL queries, program using XML paths, and support object-orientation in this setting.
The uniform treatment of data structures is based on the simple observation that every data structure is either an atom or a compound, so that two patterns suffice to match against an arbitrary data structure. Using such patterns one can define equality of arbitrary data structures. A novel example is the operation updateSalary which takes a function f and a data structure d and updates each sub-structure of d of the form Salary(s) to Salary(f(s)). By allowing free variables in patterns one can go further, and define a function update that takes Salary as its first argument. More generally, one can apply update to a function that will be used to compute a path to the salaries. Generalising further, one can define an abstract data type of XML paths suitable for XML programming.
These examples require a rich collection of patterns, which creates significant difficulties. After several generalisations, the latest approach (August,2005) is the *all pattern calculus* in which
any term may be a pattern, and any pattern may be a term.
The difficulties are addresed by employing a non-standard treatment of variables and scope. That done, the usual properties of reduction, such as confluence and progress, are easily established.
Type derivation rules for the pattern calculus are able to handle the examples above. In addition, subtyping is supported, so that one can define methods such as getCentre which map a circle to a point or a coloured circle to a two-dimensional point. It also supports generic operations such as mapping, which is able to act on lists or trees, etc. The resulting five forms of polymorphism are (with examples):
- parametric polymorphism (append) - inclusion polymorphism (getCentre) - path polymorphism (equality) - pattern polymorphism (update) - structure polymorphism (mapping)
The core ideas of the pattern calculus are expressed in the programming language bondi. It, and papers documenting the pattern calculus can be found at www-staff.it.uts.edu.au/~cbj.
BIO:
Associate Professor Barry Jay is a member of the Dept of Software Engineering in the Faculty of Information Technology at the University of Technology, Sydney. He obtained his BSc (Hons, pure mathematics) from the University of Sydney (1980) and his PhD (mathematics) from McGill University, Montreal (1984). He learned about computing as a senior research fellow at the Laboratory for the Foundations of Computer Science in Edinburgh before moving to UTS in 1993. His current research interests focus on creating a deeper understanding of the role of data structures in programming, especially in developing new forms of polymorphic programming based on pattern matching.
