RFC Walters' "Categories and Computer Science" : Functional Specification

["Bill Halchin" <bhalchin@hotmail.com>]

     In Chapter 5 "Categories of Functors", there is Section 5 entitled
"The Specification of Functions". To me this is pretty interesting and
neat stuff!! I have some thoughts, questions, etc. which I will now
enumerate:

1) The method of specification defined in this section seems to be
essentially a rewrite system, i.e. we do a series of rewrites or
reductions on "data" (actually a certain kind of path in a Data graph)
until we possibly terminate. Hence the finite set of Equation that
Walters' describes is basically a set of rewrite rules, i.e.  one-way
rules in Rewriting Systems parlance.

2)  We have  two sets of Data paths that define the domain and codomain, 
respectively::
       - The Domain is respresented by a set of paths starting  at Data 
graph's "I" node and  ending at "J" node
      - The Codomain is represented by a set of paths starting at the Data 
graph's "I" node and ending at the "K" node
      Question: I guess using "I" for both Domain and Codomain is just a 
clever way of partitioning some of the possible paths of the Data graph into 
one set of paths representing Domain and another set of paths representing 
the Codomain (of course these sets can be the same!)???? I.e. we could
have chosen a different mechanism that I, J, K, yes???

3) On pg. 118, there is a "Note" about work that Robie Gates did to show
that we can achieve Turing completeness with this method of function
specfication.i.e. we can compute all parial recursive functions from N to
N. Hence the computation may not be terminating!!!! Otherwise, we would
not have Turing completeness and could solve Halting problem.

     Also mentioned in this Note is that not only are we not guaranteed
total functions (hence possibly partial functions), but we may also be
computing a relation.

     - Question: what restrictions must we put on the finite set Equation
to guarantee confluence???? I.e. computing a function and not computing a
relation???  Probably the answer to this is in a book on Rewriting Systems
or maybe Dershowitz paper.


4) Also it seems that Walters' approach of functional/relational
specification, could be looked at in terms of equational reasoning. I.e.
if we have a "specfied arrow" f: J -> K and lambda, a path from I to J and
epsilon, a path belonging to I to K, then Equation |- (f.lambda, epsilon).
Yes???


5) Finally and important to me, has work been continued by anyone else in
this area?? I don't see any papers in Walters' groups archive!! This
approach to function (and relation) specification is pretty spiffy from a
theoritcal viewpoint, but it seems it could be used as a basis to do
functional programming or even logic programming (computing relations) by
specifying the programs graphically!!



Regards,

Bill Halchin