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

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

[Bill Halchin]

     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

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

[Sebastiano Vigna]

On Mon, 7 Feb 2000, Bill Halchin wrote:

> 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.

Yes. Indeed as part of my Ph.D. dissertation I wrote a complete specification
of the interpreter in ASF+SDF, a rewrite rule-based system for algebraic
specifications used at the University of Amsterdam. It can execute programs
of that kind. I can send it to you if you want so. The interpreter is
partially described also in the following papers:

Sebastiano Vigna. Specifying IMP(G) using ASF+SDF: A case study. In Proc. of
the ASF+SDF95 workshop on generating tools from algebraic specifications.
Technical Report P9504 of the University of Amsterdam, 1995.

Sebastiano Vigna. Towards an efficient implementation of distributive
programs. In Proc. of the 2nd International Workshop on the Theory and
Practice of Algebraic Specifications ASF+SDF, Workshops in Comput.
Springer-Verlag, 1998.


> 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.

Of course (the book is a bit confusing about this issue). Turing completeness
is proved in

Nicoletta Sabadini, Sebastiano Vigna, and Robert F.C. Walters. A note on
recursive functions. Math. Struct. Comp. Sci., 6:127-139, 1996.

and BSS (real numbers computability) completeness is proved in 

Sebastiano Vigna. On the relations between distributive computability and the
BSS model. Theoret. Comput. Sci., 162:5-21, 1996.

> 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

Not to my knowledge, but you should ask Bob Walters directly.

Greetings,

					Sebastiano Vigna