Advertisement

A graphical calculus

  • Sharon Curtis
  • Gavin Lowe
Contributed Lectures
Part of the Lecture Notes in Computer Science book series (LNCS, volume 947)

Abstract

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.

Keywords

Composition Operator Sequential Relation Graph Transformation Sequential Calculus Local Linearity 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. 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. 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. 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. 5.
    Peter Preyd and Andre Scedrov. Categories, Allegories. North-Holland, 1990.Google Scholar
  6. 6.
    C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.Google Scholar
  7. 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. 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. 9.
    A. Tarski. On the calculus of relations. Journal of Symbolic Logic, 6:73–89, 1941.Google Scholar
  10. 10.
    Burghard v. Karger and C. A. R. Hoare. Sequential calculus. Information Processing Letters, 53:123–130, 1995.Google Scholar
  11. 11.
    Chaochen Zhou, C. A. R. Hoare, and Anders P. Ravn. A calculus of durations. Information Processing Letters, 40:269–276, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Sharon Curtis
    • 1
  • Gavin Lowe
    • 1
  1. 1.Computing LaboratoryOxford UniversityOxfordUK

Personalised recommendations