There has been significant study of regular languages in computer science and much is known about how they relate to finite automata, symbolic logic, and algebraic formalisms. Each of these relationships has led to an increased understanding of regular languages, justifying that the study of formal language theory from different perspectives can be both insightful and highly significant.
This EPSRC funded project [EP/H012311/1] lies at the novel interface of diagrammatic reasoning and formal language theory. Until recently, nobody had observed the strong relationship between diagrammatic logics and formal languages or, therefore, recognized the possible significant benefits of pursuing this line of enquiry. The main aim of the project is to develop a second order diagrammatic logic, capable of defining regular languages. The development of such a logic could be a major step forward for the diagrams community, since the diagrammatic logics that have been formalized and investigated to-date are typicall first order, with the vast majority of them limited to the expressive power of at most monadic first order logic with equality.
The diagrammatic logics that the project will consider are those based on Euler diagrams, augmenting them with additional syntax. In particular, the team have been extending spider diagrams to second-order spider diagrams interpreted over a totally ordered universe. The example below shows such a diagram which expresses that the minimal element of the universal set, U, is in A, as is the maximal element. In addition, the unlabelled curves assert the existence of sets and the arrows represent a bijection between sets, indjuced by the total ordering. So, the arrow from the curve, C, containing min asserts that the successor of the elements in the set represented by C are in the set represented by the target of that arrow. As a whole, the diagram expresses that all elements are in A and there are an even number of them.
The research will develop the novel link between the new second order diagrammatic logic and regular languages. This will not be the first time that regular languages have been related to second order logic, with extensive research conducted into their relationship with symbolic logics. These previous investigations have proved fruitful in terms of our understanding of regular languages, including those that are star-free, and provided insight into the famous star-height problem. However, the syntactic structure of symbolic logic sentences is very different to the manner in which diagrammatic logics make statements. Thus, the development of the proposed diagrammatic logic stands to shed new light on the investigation of regular languages. With the highly significant role that formal language theory plays in computer science, the proposed research stands to bring with it important benefits for this community also.
The project runs from 2010 - 2011 and the proposal can be found here, which contains full details of the aims and objectives.
Dr Gem Stapleton is the Principal Investigator and Dr Peter Chapman is the Research Fellow on the Project. The team are closely collaborating with Aidan Delaney and are also working with Professor Simon Thompson and Dr John Taylor towards the project objectives.
The following publications directly contribute to the project outcomes.
The following publications contribute to the project outcomes in a variety of ways, most notably with regard to developing diagrammatic logics with expressiveness beyond monadic first-order logic.