A graphical calculus
- 204 Downloads
We present a graphical calculus, which allows mathematical formulae to be represented and reasoned about using a visual representation. We define how a formula may be represented by a graph, and present a number of laws for transforming graphs, and describe the effects these transformations have on the corresponding formulae. We then use these transformation laws to perform proofs. We illustrate the graphical calculus by applying it to the relational and sequential calculi. The graphical calculus makes formulae easier to understand, and so often makes the next step in a proof more obvious. Furthermore, it is more expressive, and so allows a number of proofs that cannot otherwise be undertaken in a point-free way.
KeywordsComposition Operator Sequential Relation Graph Transformation Sequential Calculus Local Linearity
Unable to display preview. Download preview PDF.
- 1.Stephen Brien. A time-interval calculus. In R. Bird, C. Morgan, and J. Woodcock, editors, Mathematics of Program Construction, volume 669 of LNCS. Springer Verlag, 1992.Google Scholar
- 2.Carolyn Brown and Graham Hutton. Categories, allegories and circuit design. In Ninth Annual IEEE Symposium on Logic in Computer Science, pages 372–381, 1994.Google Scholar
- 3.Carolyn Brown and Alan Jeffrey. Allegories of circuits. In Third International Symposium, Logical Foundations of Computer Science, volume 813 of Lecture Notes in Computer Science, pages 56–68. Springer-Verlag, 1994.Google Scholar
- 4.E. W. Dijkstra. The unification of three calculi. In M. Broy, editor, Program Design Calculi, pages 197–231. Springer Verlag, 1993.Google Scholar
- 5.Peter Preyd and Andre Scedrov. Categories, Allegories. North-Holland, 1990.Google Scholar
- 6.C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.Google Scholar
- 7.Graham Hutton, Erik Meijer, and Ed Voermans. A tool for relational programmers. Available on WWW from http://www.cs.ruu.nl/people/graham/allegories.txt, 1994.Google Scholar
- 8.S. Kleene. Representation of events in nerve nets and finite automata. In Shannon and McCarthy, editors, Automata Studies, pages 3–42. Princeton University Press, 1956.Google Scholar
- 9.A. Tarski. On the calculus of relations. Journal of Symbolic Logic, 6:73–89, 1941.Google Scholar
- 10.Burghard v. Karger and C. A. R. Hoare. Sequential calculus. Information Processing Letters, 53:123–130, 1995.Google Scholar
- 11.Chaochen Zhou, C. A. R. Hoare, and Anders P. Ravn. A calculus of durations. Information Processing Letters, 40:269–276, 1992.Google Scholar