Friday, May 02, 2014

On the algebra of processes IV

In this post I want to begin describing simple sequential programming in terms of Cospan(Graph/A).  First let's look at two examples of (infinite) cospans:
N is the natural numbers. The span "error" is the partial function which takes 0 to error. The span "pred" is the partial function which takes n to n-1 if n is positive. The span "zero" is the function on one point that takes the value 0. The span "succ" is the successor function.


(As a graph (instead of split up into spans) predecessor has vertices N+1+N and edges N. The edge 0 goes from 0 of the first component of N+1+N to the single element of 1. The edge n+1 goes from n+1 in the first component of N+1+N to n in the third component.)

The composite of predecessor followed by successor is the following cospan, a behaviour of which takes n on the left to n-1 or error inside and then to n on the right (so the input output behaviour is the identity function of N).

The composite of successor followed by predecessor is the following cospan, a behaviour of which takes n on the left to n+1  inside and then to n on the right, and takes the one element of 1 to 0 inside and then the one element of 1 on the right (so the input output behaviour is the identity function of 1+N ). 




I will describe programming in Cospan(Graph/A) mostly in terms of pictures but each program is an expression in the operations of composition, tensor (sum) and the constants of Cospan, and one extra operation to be introduced. I haven't mentioned the constants but they are as follows (states only, no transitions). 

The last two are derived from the others by composition. These constants allow the identification of states when composed with other cospans (by pushout).

It looks like I wont get to programming today.

In the next post I will describe the constructions "while" and "if then else". Together with the the data type natural numbers described above this will imply that Cospan(Graph/A) as a programming language is Turing complete.

For other data types described in a way appropriate for Cospan(Graph/A) see my book.

--------------

Notice that I haven't mentioned recursion. In my view recursion comes after having an algebra of processes in the consideration of equations in the algebra.

The closest thing in the literature that I know to the material I am describing is the work of Elgot and collaborators who however (i) have algebras of behaviours (like Kleene) rather than of machines/programs,
and (ii) separate the memory from the control. It is interesting to read Dana Scott's view of Elgot's work in his foreword to Elgot's selected papers. Certainly Scott's view has till now received more attention in the categorical community interested in programming (though not perhaps his view on 2-categories reported by Vaughan Pratt).

I hope it will be clear from the next lecture that the Kleene theorem and the Bohm-Jacopini theorem are essentially the same theorem - namely that any graph (automaton, goto) may be given by an exression in Cospan(Graph/A) in terms of elementary graphs.

Labels: ,

0 Comments:

Post a Comment

<< Home