Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    Recursion Diagrams: Ideas for a Geometry of Formal Methods

    3rd BCS-FACS Northern Formal Methods Workshop

    Ilkley, UK. 14th - 15th September 1998


    Dr. A. Butterfield


    This paper describes work leading towards the concept of a Geometry of Formal Methods [Mac96], [HM97], which explores the relationship between various formal description techniques and aspects of modern abstract algebraic theories with a strong geometric interpretation, in particular such concepts as fibre-bundles, sheaves and related ideas in topology and category theory.

    Inspired by ideas and notions of seeking a geometry of computing and of formal methods, and with the category theoretic concepts of topos in mind, we explore how such a geometry might be expressed in concrete diagrams, and explore their ability to lay clear some of the concepts behind tail recursion optimisation.

    We also indicate how this approach can be used in an exposition of various published program transformation rules in this area. We also show the use of category theoretic notions to help explain the similarity of two apparently quite different diagrams.

    All of this points towards a future foundation for our geometry, both in diagrammatic and algebraic form, in the area of category theory.


    PDF filePDF Version of this Paper (348kb)