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?

A CSP approach to FBP inter-component communication

photopin cc

Any portal in a storm!

TL;DR Sometimes maligned, C++ multiple inheritance allows an object to be 2 things at once—such as both an input port and an output port. In this way any would-be-component class that multiply descends from both fbp::input and fbp::output port classes has the is-a-relationship that enables it to be connected to any other so descended component. Neat huh?

It is axiomatic in Hoare's CSP theory[1][2][3] that the internal states of a Component are invisible to its environment and communication between processes can only take place at one of two unidirectional input and output channels. Most common variants[4] of CSP approach the two channel restriction problem by describing communication at multiple named unidirectional channels such that each CSP event m.t consists of two  parts: m the channel name and t the message content. Thus for a process that engages in event t via channel m and then behaves as process P is denoted:

m.t -> m.P

In order for libfbp to be CSP compliant then, the only communication that an fbp::component can engage in is via its named input and output ports. Assuming it is possible to build any functional FBP program using libfbp  then there is no reason that CSP compliance should be sacrificed, and with it the opportunity to use process calculus to prove program correctness. With this goal of CSP compliance in mind, what then is the best way to implement port only based communication?

Compile-Time Brittle Run-Time Robust Static Type Safe FBP Connections

photopin cc

A bit of C++ untyped-to-typed separation template magic...

TL;DR You can have your cake and eat it! With collections of non-typed connectable classes static_cast to the typed template connection<T> interface opens up a world of ways of connecting together components!

The design decision to construct libfbp as a strictly type safe implementation of FBP is primarily aimed ensuring that no operation leads to undefined behaviour. 

Unfortunately there is an implementation dichotomy between being able to create a typed first-class FBP connection object and freely pass around such connections as the arguments in generic functions that manage those connections or the collections that store them.

A CSP approach to FBP Information Packets

What exactly are we delivering here?

TL;DR Don't look now the CSP event is the FBP IP, the FBP IP is the std::unique_ptr.

The real world has put a significant crimp on my programming of late but I have had plenty of time to think about things, so this post is rather theory heavy and code light.

The axiomatic processes of CSP Theory have been implemented as FBP Components here, here and here; but what of the FBP Information Packet (IP) - does it have a CSP equivalent?