Mathematical Semantics for FBP - Describing Fundamental FBP Program Types

photopin cc

A glittering treasure of mathematical semantics for FBP or fool's gold?

TL;DR Examples of using mathematical semantics for FBP by combining (named channel) Theory of CSP and Graph Theory to describe 3 fundamental FBP program graph types which can form the basis for both reasoning about experimenting with libfbp programs.

As I have argued so far here, here, here, here, here and here, my overarching proposition in searching for a useful mathematical description for Flow Based Programming is that an FBP network of black box processing components that communicate information packets via one-way connections can be modelled as a directed graph of communicating sequential processes.

But how might such a model be usefully applied to reasoning about FBP and what might a fundamental FBP program be?

In searching for fundamental classes of FBP programs is it worth trying to define programmatic identities that can be compared both within and across implementations to reason about a class of FBP programs?

Mathematical Semantics for FBP - Graph Theory

photopin cc

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?