In search of descriptive and inferential semantics for FBP.
TL;DR In trying to develop mathematical semantics for FBP, in order to reason about FBP programs and design experiments to test hypotheses, it is proposed that Graph Theory (GT) can describe the properties and behaviours of an FBP program. Which is nice.
The value of defining mathematically based compliance design criteria for libfbp is that such a definition could serve as a standard. Such a precise specification for any FBP implementation informs the programmer using it that they can rely on certain axiomatic behaviours and, being a modular programming paradigm, be assured of the reliable conjunction of FBP modules from widely differing sources.
Beyond its immediate utility then, developing mathematical semantics for libfbp/FBP at an early stage will hopefully forestall problems with the quality of libfbp programs—as Brookes states[1]
“Clearly, no program can be more reliable than the implementation of the language in which it is expressed for input to a computer.”
The benefits to FBP go beyond quality issues and extend to the potential for the formal proof of correctness for a libfbp program. Given that each libfbp component is in, and as of, itself an isolated Von-Neumann machine, then Hoare-style logics for sequential languages based on state-transformation semantics are particularly suited to the way a component functions.
In this way the modular approach to building a FBP program provides islands of correctness communicating via connections. Subsequently, and given proof of conformity with the mathematical model, FBP developers have powerful mathematical tools at their disposal to formally prove correctness.
The question then arises as to what
mathematical semantics are most appropriate for describing libfbp program structure or rather its form?
Graph Theory
Graph theory sees its origins with Swiss mathematician Leonard Euler’s 1736 paper on his negative solution to the historically notable Seven Bridges of Königsberg problem [2]. He developed a technique of analysis and of subsequent tests that established his assertion with mathematical rigor. In modern terms Euler’s abstraction of the problem is to regard each bridge as an abstract connection termed an edge and each island a corner to turn or vertex. Each edge serves only to indicate which pair of vertices are connected, the whole description of edges and vertices becomes the mathematical concept of a graph.
Graph Theory for FBP
In the context of Flow Based Programming then, when graphically representing the form of a program the literature, after Morrison[3], represents components as discrete entities, commonly a box, with an arc or arcs representing the connections between them and arrow indicating the direction of flow of the information packets.
N.B. This graphical depiction should not be confused with the software implemented non-visual structure of the program itself, as there are many ways to implement an FBP program in actual software.
Lemma 1: This diagrammatic approach to defining an FBP program has clear and complete conceptual one-to-one relationships with the graphical depiction of the mathematical structures used to model the pairwise relationships between objects i.e. a graph.
At its nub all that matters semantically is that the abstract structure of directionally connected components that constitute a libfbp program can be generalised to a graph. Such that each fbp::component can be regarded as the node or vertex of a graph and each fbp::connection can be regarded as a directed edge.
Lemma 2: A libfbp program can be considered as the graph G composed of the ensemble of components v as the set of vertices V, such that v ∈ V.
Which is all well and good, but graph theory describes the connections between vertices in a directed graph with a second set of ordered pairs such that, formally, for two vertices u and v, the edge between them is {u,v}.
However, as per Morrison's descriptive stipulations[3] for the properties of an FBP software artefact requires the presence of a defined (buffered) connection between two components.
Consider two such FBP components u and v joined by an FBP connection u.v where u.v passes IPs from u to v then u.v can also be represented by the directed edge as an ordered pair {u,v}.
∴ u.v ≡ {u,v}
Further given an fbp::connection e that defines an edge between two fbp::components and the totality of fbp::connections in the libfbp executable as the set of edges E, such that E={e | e∈E∧e is fbp::connection}.
And physical fbp::connections are conceptual FBP connections which are edges in a program graph G—the notation may be bad but not catastrophic and aided by context.
In this way if the set of processing fbp::components that comprises G can be denoted by V(G), or simply V and the total number of processing components is the order of the graph |V(G)|.
Similarly, if the set of fbp::connections that comprises G can be denoted by E(G), or simply E then there is no danger of ordered pair confusion but safe in their equivalence and the total number of connections is the order of the graph |E(G)|.
Consequently the FBP program to be executed and, ergo, the mathematical problem to be solved becomes:
G=(V,E)
There is nothing in Morrison's[3] descriptive definition of FBP that restricts the multiplicity of the ensemble executable graph G nor requires it to be acyclic, merely that the connections are directed.
However, as much as the graphical depiction of a GT graph should not be confused with the abstract non-visual underlying mathematical structure, in as much as there are several ways to layout a graph, neither should an FBP diagram be confused with the underlying software implantation. Indeed, the semantics of an FBP program might require several different kinds of graph in order to communicate not simply the layout of the connection network but using different weights for the vertices to communicate, for example, the latencies associated with each component. Thus the graph theory semantics for FBP go beyond simple form but extend into a wide domain of function.
Therefore, graph theoretic methods, in various forms, could prove particularly useful for analysing FBP software and, as will become evident in later posts, not least for experimental design.
References:
[1] "A Theory of Communicating Sequential Processes" S.D. Brookes, C.A.R. Hoare, and A.W. Roscoe, 1984
[3] J. Paul Morrison, Flow-Based Programming, 2nd Edition: A New Approach to Application Development, CreateSpace, 2010, ISBN 1-4515-4232-1
No comments:
Post a Comment