In 1971, J.H. Conway introduced the notion of a "factor" of a regular language. He established that factors can be organised in a matrix which is reflexive and transitive, and he showed how factors can be used to establish several non-trivial regularity-preserving properties of functions on languages. Subsequently, Backhouse (1975) showed that the factor matrix has a unique "starth root" (that is, there is a unique minimal matrix whose reflexive, transitive closure equals the factor matrix), which he called the "factor graph". Backhouse and Lutz (1977) showed how the well-known Knuth-Morris-Pratt string matching algorithm can be reformulated as computing the factor graph of a certain language derived from the pattern. In this talk, we will review this early work on factors, presenting it in a novel way that focuses on calculational properties. In particular, we will show that factors are instances of the more general concept of a Galois connection, and we will review the importance of Galois connections in algorithm development. A recent application of factor theory to program analysis, due to Oege de Moor, will conclude the presentation.
The demands of producing reliable software have inspired a revolution in the way that Mathematics, the art of effective reasoning, is conducted and presented. With the aid of a number of examples, of both good and bad practice, this talk illustrates how goal-directed construction replaces the traditional theorem-proof style of doing mathematics. The aim ---to revitalise the interest of future generations in the challenge of problem-solving and the value of technique--- will be discussed.
"Theorems for free" is a technique for deriving properties of parametrically polymorphic functions from their type. The technique is based on interpreting types as relations --- so-called ``logical'' relations. A problem is that it is often difficult to understand the significance of the logical relation associated with a particular function. This talk is about using point-free relation algebra to express algebraic properties of logical relations and how these properties are used to calculate properties of specific functions. As an example, we derive the dinaturality property of the fold function on lists.
Abstract interpretation is a technique for safely approximating the behaviour of computer programs. It is used widely in compiler optimisation and, increasingly, as a basis for model checking. "Theorems for free" is a technique for deriving properties of parametrically polymorphic functions from their type. This talk is about combining abstract interpretations with theorems-for-free. We introduce the use of Galois connections in abstract interpretations and we show how given base Galois connections can be extended to Galois connections of arbitrary type. It is then shown that theorems-for-free establishes the safety of the abstract interpretations.
Generic programs are programs that are parameterised by one or more type constructors. In this talk we show how the properties well-founded and admitting-induction of a relation are made generic. Unlike their non-generic instances, the generic notions are not equivalent. The talk focuses on the notion of F-reductivity, a generic notion of program termination, emphasising its importance in the construction of recursive programs and discussing its basic properties. (This is joint work with Henk Doornbos of EverMind.)
Many functions on context-free languages can be expressed in the form of the
least fixed point of a function whose definition mimics the grammar of the given language.
Examples include the function returning the length of the shortest word in a language, and
the function returning the smallest number of edit operations required to transform a given
word into a word in a language.
This paper presents the basic theory that explains when a function on a context-free
language can be defined in this way. It is shown how the theory can be applied in a
methodology for programming the evaluation of such functions.
Conway's book "Regular algebra and finite machines" has been mentioned frequently at this seminar.
However, one important contribution in his book that has not been mentioned is
his study of so-called ``factors'' of a regular language. The goal of this talk
is to bring this to everyone's attention.
Conway's ``factors'' are called ``residuals'' in relation algebra and
``weakest prespecifications'' in the programming literature; the fact that the same concept is known by various names attests to its importance.
Conway's contribution was to show that the factors of a regular language
can be organised in a matrix, which he called the factor matrix. This matrix
has a number of special properties -- for example, the matrix is reflexive and transitive. Conway's account of the factor matrix is however very wordy, making it difficult to read and check.
In one case, the unfortunate omission of the word ``not'' in a sentence caused me a great deal of confusion when first reading his text!!
In this talk, I show how factors are formulated using the now standard Galois connection defining the residuals of a relation. This allows one to give
precise, calculational formulations of the factor matrix. I also mention the relation between the factor ``graph'' and the Knuth, Morris, Pratt string matching algorithm (see Backhouse and Lutz, ICALP 1977).
Prompted by an earlier talk I show how factors are used to formulate the well-foundedness of a relation. This formulation is used to present a calculational proof of Newman's lemma (see Doornbos, Backhouse and Van der Woude, TCS, 1997).
Applications of regular algebra to language processing problems.
Presented at Dagstuhl Seminar Applications of Kleene Algebra, 18--23 February 2001
Extended abstract in ESOP 2001, LNCS 2028, pp. 107--121.
Factor Theory Revisited.
Presented at Dagstuhl Seminar Applications of Kleene Algebra, 18--23 February 2001