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