Authors: Sandra Alves (University of Porto), Besik Dundua (Porto / Ivane Javakhishvili Tbilisi State University), Mário Florido (Porto), and Temur Kutsia (Johannes Kepler University).
Workshop: 2nd International Workshop on Confluence (IWC 2013), 28 June 2013, Eindhoven, The Netherlands.
Reference: Retrieved from workshop website, 8 July 2013.
Comments: This week's paper is certainly the shortest I've looked at for this blog - no bad thing in a week I've been wrestling with a conference deadline - at just 4 pages plus a half page of references. But this it isn't a formally `published' paper at all, although it has been reviewed; rather, it is a short communication to the specialist workshop IWC 2013, and ideas in here will probably form part of some bigger published paper in the future. Like many such workshops, IWC is a satellite orbiting a bigger event, the International Conference on Rewriting, Deduction, and Programming (RDP 2013), whose main events are two conferences, RTA and TLCA, that do have formally published proceedings (last week's paper hailed from one of those conferences).
The topic of the workshop IWC is confluence. Some computational systems are non-deterministic - at certain points their next steps may not be completely determined, like a Choose Your Own Adventure book. A non-deterministic system is confluent if those 'choices' don't really matter in the end - whenever possible paths diverge, they must always be able to converge again. In a Choose Your Own Adventure book this would imply that there was at most one accessible ending (there could be loops in the book, and hence perhaps no ending at all; confluence says nothing about termination, but rather says you can never make a choice that closes off where you would have gone if you'd made a different choice). In such a book confluence would be a bit of a rip-off, but for a computational system it is highly desirable, because it means the overall behaviour of the system is predictable without going to the trouble of specifying a totally deterministic strategy.
A class of computational systems for which confluence is highly prized are formal calculi, among which the λ (lambda) calculus is king. Here computation is expressed as the simplification, or reduction, of a term, and confluence corresponds to the notion that it doesn't matter which part of the term you choose to reduce first. While the λ-calculus is powerful enough to model any and all computations, there is good reason why most programmers use languages with many more built-in commands - just because you can use the λ-calculus for something like complex data structures doesn't mean it's easy to do so, so ready-to-hand support for them is to be desired. However even with such 'higher' commands the λ-calculus comes in useful, as by bolting them directly on to the basic calculus we can study their behaviour, including how they effect confluence.
One such 'extension' to the λ-calculus known to cause problems with confluence is pattern matching, the process of comparing a term with some pattern, attempting to unify them (as discussed last week), then proceeding to compute using that unification somehow. I'm being intentionally vague here - there are many notions of pattern matching, differing for example in their choice of what constitutes a 'pattern', and a whole host of them have been added to the λ-calculus. The most important reference for this work is the dynamic pattern λ-calculus of Cirstea and Faure, itself an attempt to unify various other calculi with similar intent. This workshop paper extends the dynamic pattern λ-calculus with hedge variables, which instead of being substituted for by terms, may be substituted for by lists of terms, and discusses how such a calculus can be constrained to get the desired confluence property.
No comments:
Post a Comment