Author 
Message 
S Ramesh Ba #1 / 8

BirdMeerten Formalism
BirdMeerten Formalism  Considering BirdMeertens formalism [1] for (functional) program derivation from a given specification, following questions were encountered : 1. What is the expressive power of this formalism? 2. Can this be easily extended for various other data structures such as trees? Any references? 3. Is this formalism consistent and complete? What I meant by this is, does the following operators such as map, reduce, directed reduce, accumulate, filter, prefix etc always suffice for the fixed set of operators? 4. It has been shown that certain function compositions for the given problem might result in an efficient program derivation. This may not be true always by just trying some means. So, is there a way out to find, when does some new composition of functions could result in a faster implementation. 5. What is the criteria that a given formalism should possess? I mean, if I have to derive a program from a given specification with some available formalisms what should I look at in those given formalisms? For instance, Partsch[2] also speaks about Transformational Program Development but doesn't have a motivation for mathematical considerations and is based on pragmatic needs of the given specification and program. How does this exactly differ from [1] apart from the fact that [1] has some nice algebraic properties. Any answers and guidance would be gratefully appreciated. Thanks a lot. S. Ramesh Babu
========================References================================= 1. Bird R S: `A Calculus of Functions for Program Derivation' in Research Topics in Functional Programming, AddisonWesely Publishing Company, ed. D.Turner 1990.  2. Partsch H: `Transformational Program Development in a Particular Domain', Science of Computer Programming, Vol. 7, No. 2, 1986 ===================================================================  ====================================================================
 Research Scholar   Dept. Of Computer Science & Engg. 

Tue, 03 Jan 1995 13:01:48 GMT 


Daniel Tuijnm #2 / 8

BirdMeerten Formalism
Quote: > BirdMeerten Formalism > 
In our Software Engineering group in Nijmegen, The Netherlands, we work on both formalisms mentioned hereunder, the BirdMeertens Formalism (BMF), and the CIP wide spectrum language [CIP85]. Since Helmut Partsch is our professor, and former member of the Munich CIPproject, we work mainly with this formalism, and are less familiar with BMF; our colleagues will certainly be able to answer the questions we left open. Quote: >Considering BirdMeertens formalism [1] for (functional) program >derivation from a given specification, following questions were >encountered :
First some general remarks on BMF. Begun as a theory on lists [Bir87,Bac89c], the method has been generalized to other data structures as well [Bir89b,Jeu91]  which answers your second question. The theoretical foundations for this were first laid on basis of the Hagino types [Mal90a]. The current situation is that the proponents of BMF make heavily use of category theory; Fokkinga shows in his PhD thesis [Fok92] nicely how categorical "arrow chasing" can be translated into calculations. Quote: >1. What is the expressive power of this formalism?
BMF merely is interested in functions over polynomial datatypes (using cartesian product, coproduct (= disjoint sum) and primitive sets as type constructors). With regard to these datatypes, and assuming "interesting" functions over the primitive sets, all possible functions can be constructed. Quote: >2. Can this be easily extended for various other data structures > such as trees? Any references?
See above, and [Bir89b,Jeu91]. Quote: >3. Is this formalism consistent and complete? > What I meant by this is, does the following operators such as > map, reduce, directed reduce, accumulate, filter, prefix etc > always suffice for the fixed set of operators?
What you mean by consistency, I don't know; and with regard to completeness, it seems the same question as 1. For the theoretical foundations, BMF has drifted away from the "primitiveness" of the operators you mention. These now follow directly from the categorical construction of the datatype involved; for instance, the map, seen as a mapping from a function f: A > B to a function f*: A* > B*, basically is the morphismaspect of the functor which constructs from the datatype A the datatype A* of lists over A. Quote: >4. It has been shown that certain function compositions for the > given problem might result in an efficient program derivation. > This may not be true always by just trying some means. So, is > there a way out to find, when does some new composition of > functions could result in a faster implementation.
We don't know any theory about which steps are "right" and which not. I guess sometimes one even has to go to a less efficient expression temporarily  "recuperer pour mieux sauter" as the French say. Quote: >5. What is the criteria that a given formalism should possess? > I mean, if I have to derive a program from a given > specification with some available formalisms what should > I look at in those given formalisms? > For instance, Partsch[2] also speaks about Transformational > Program Development but doesn't have a motivation for > mathematical considerations and is based on pragmatic needs > of the given specification and program. How does this exactly > differ from [1] apart from the fact that [1] has some nice > algebraic properties.
Comparing the methods of BMF and CIP, one observes that both advocate transformational programming, with the same fundamental ideas, but that they differ greatly in the scope to which the method is applied. BMF on the one hand concentrates on functional programs, which initially are stated in an *executable* way (with some syntactic adjustments, you can type in your BMF expression in any functional programming language!) and then only are optimized w.r.t. execution time and/or space. Sometimes Bird gives an example how a BMF program can be translated into an imperative program (which is straightforward) but leaves it with that. CIP on the other hand, is meant as an overall method for program development [Boi92e]. One first specifies an algebraic data type  without the BMF constraint of polynomial types  and then has several layers of expression constructs for making programs over these data types. Apart from the usual functional and imperative constructs, the socalled descriptive constructs need to be mentioned: one can specify functions by means of predicates, using quantifiers, and one can "describe" the result of a function by means of a predicate which it has to fulfill. Thus one can start program development with a very abstract specification and stepbystep transform this into a concrete, executable program. An overview over the method is given in [Par90a]. Since all language layers (algebraic, descriptive, functional, imperative) are combined in one, formally defined, language [CIP85], the transformations from one layer to another are correct. So, both methods are mathematically sound, and formally defined, but differ in their scope and objective. Your question w.r.t. the criteria solely depends on what you have in mind: do you want to improve the efficiency of an existing (functional) program, or do you want to develop a program from scratch? Daniel Tuijnman Max Geerling
Dept. of Computing Science, Software Engineering group University of Nijmegen The Netherlands References: (in BibTeX format) On the BirdMeertens Formalism:
Bir87, Author= {Bird, R.S.}, Title= {An Introduction to the Theory of Lists}, Pages= {542}, Crossref= {NATO.ASI.F36}}
NATO.ASI.F36, Title= {Logic of Programming and Calculi of Discrete Design. {NATO ASI} Series Vol. {F}36}, Booktitle= {Logic of Programming and Calculi of Discrete Design. {NATO ASI} Series Vol. {F}36}, Editor= {M. Broy}, Publisher= sv, Address= {Berlin}, Year= 1987}
Bir89b, Author= {Bird, R.S.}, Title= {Lectures on Constructive Functional Programming}, Crossref= {NATO.ASI.F55}, Pages= {151218}}
NATO.ASI.F55, Title= {Constructive Methods in Computing Science. {NATO ASI} Series Vol. {F}55}, Booktitle= {Constructive Methods in Computing Science. {NATO ASI} Series Vol. {F}55}, Editor= {M. Broy}, Publisher= sv, Address= {Berlin}, Year= 1989}
Mei91a, Author= {Meijer, E. and Fokkinga, M.M. and Paterson, R.}, Title= {Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire}, Booktitle= {Functional Programming and Computer Architecture}, Year= 1991}
Fok92, Author= {M.M. Fokkinga}, Title= {Law and Order in Algorithmics}, Year= 1992, School= {Universiteit Twente}}
Mal90a, Author= {G.R. Malcolm}, Title= {Algebraic Data Types and Program Transformation}, School= {Rijksuniversiteit Groningen}, Month= Sep, Year= 1990}
Mee89c, Author= {L.G.L.T. Meertens}, Title= {Constructing a calculus of programs}, Pages= {6690}, Crossref= {lncs375}}
Mee91, Author= {L.G.L.T. Meertens}, Title= {Paramorphisms}, Journal= {Formal Aspects of Computing}, Year= 1991, Note= {To appear}, Referencefrom= {Jeu91 says it's still to appear}}
Bac89c, Author= {Backhouse, R.C.}, Title= {An Exploration of the {BirdMeertens} Formalism},
Ame89, Organization= {STOP}, Title= {STOP International Summer School on Constructive Algorithmics, {A}meland}, Booktitle= {STOP International Summer School on Constructive Algorithmics, {A}meland}, Author= {Bird, R.S. and Backhouse, R.C. and Malcolm, G. and de Moor, O. and Jeuring, J.T. and Jones, G. and Fokkinga, M.M. and Sheeran, M. and Meertens, L.G.L.T.}, Referencefrom= {Eerke Boiten}, Note= {Lecture notes}, Month= sep, Year= 1989}
Jeu91, Author= {J.T. Jeuring}, Title= {The Derivation of Hierarchies of Algorithms on Matrices}, Pages= {932}, Crossref= {TC291}}
TC291, Booktitle= {Proceedings of the IFIP TC2 Working Conference on Constructing Programs from Specifications}, Title= {Proceedings of the IFIP TC2 Working Conference on Constructing Programs from Specifications}, Editor= {B. M{\"o}ller}, Publisher= nhpc, Address= {Amsterdam}, Year= 1991} On the CIP formalism:
... read more »

Tue, 03 Jan 1995 22:22:18 GMT 


Nico Verw #3 / 8

BirdMeerten Formalism
A nice survey of literature on the BMF, as well as answers to
I would like to add the following to Daniel's posting: Quote: >The current situation is that the proponents of BMF make heavily use of >category theory; Fokkinga shows in his PhD thesis [Fok92] nicely how >categorical "arrow chasing" can be translated into calculations.
Don't say that! Maarten Fokkinga is absolutely against diagram chasing (which is what you mean by `arrow chasing'). Instead, all his proofs are equational, which is much more concise. It takes some time to get used to, however. Quote: >>1. What is the expressive power of this formalism? >With regard to these datatypes, and assuming >"interesting" functions over the primitive sets, all possible functions >can be constructed.
Of course it is as powerful as lambdacalculus, or a turing machine. But since its aim is to specify programs, the real question is: does it look nice? Since BMF makes much use of initial algebras, initial homomorphisms are one of the basic constructs. These are called catamorphisms. There are many other interesting patterns of recursion, and these have been added. They have fancy names like anamorphism, hylomorphism, paramorphism, zygomorphism, etc. Why bother with encapsulating all these different recursion patterns? Because they have nice characteristic properties, which enables the programmer to _calculate_ programs. And calculating programs with these `laws' is what BMF was invented for. Quote: >>3. Is this formalism consistent and complete? >> What I meant by this is, does the following operators such as >> map, reduce, directed reduce, accumulate, filter, prefix etc >> always suffice for the fixed set of operators?
It is consistent, in the sense that you will never derive an erroneous program from a correct one (as long as you stick to the rules). As Daniel already mentioned, the operators you mention are special cases of morphisms. It is not the case that everything that is true can be derived in BMF. That would be equivalent to the halting problem, since it requires a complete decision procedure for equality of functions. Quote: >>4. It has been shown that certain function compositions for the >> given problem might result in an efficient program derivation. >> Is there a way out to find, when does some new composition of >> functions could result in a faster implementation.
There are some laws which always improve on space/time. Sometimes it just depends... Quote: >>5. What is the criteria that a given formalism should possess?
It should be correct, and it should be usable. If this is important for you, use BMF. If, on the contrary, your criterium is that there is an implementation on your favorite machine, use CIP. Quote: >CIP on the other hand, is meant as an overall method for program >development [Boi92e]. One first specifies an algebraic data type  >without the BMF constraint of polynomial types  and then has several >layers of expression constructs for making programs over these data types.
If you can give an example of a datatype which uses nonpolynomial constructors, I would be very interested! All datatypes occurring in current programming languages, however, are polynomial. Quote: >Thus one can start program development with a very abstract >specification and stepbystep transform this into a concrete, >executable program. An overview over the method is given in [Par90a]. >Since all language layers (algebraic, descriptive, functional, >imperative) are combined in one, formally defined, language [CIP85], >the transformations from one layer to another are correct.
I don't see how this can guarantee correctness. I think that you always have to prove correctness of the transformation steps yourself. It doesn't really matter if you use one language or more, in this respect. It helps if your language is formally defined (it helps even more if it is simple, like BMF), but that doesn't take away the proof obligations. Quote: >Daniel Tuijnman Max Geerling

Sat, 07 Jan 1995 00:07:06 GMT 


Daniel Tuijnm #4 / 8

BirdMeerten Formalism
Quote:
>>The current situation is that the proponents of BMF make heavily use of >>category theory; Fokkinga shows in his PhD thesis [Fok92] nicely how >>categorical "arrow chasing" can be translated into calculations. >Don't say that! Maarten Fokkinga is absolutely against diagram chasing >(which is what you mean by `arrow chasing'). Instead, all his proofs are >equational, which is much more concise. It takes some time to get used >to, however.
Actually, that is what I meant to say. And I agree with you wholeheartedly, that Maarten's proofs are much more elegant. Quote: >>>5. What is the criteria that a given formalism should possess? >It should be correct, and it should be usable. If this is important for >you, use BMF. If, on the contrary, your criterium is that there is an >implementation on your favorite machine, use CIP.
We don't think you're being serious here. Are you referring to the CIPS system? That does indeed give machine support for carrying out the transformations, but certainly doesn't produce executable code. The distinction you draw here between BMF and CIP sounds very strange to me. Both methods have their merits in their own right, but they are aimed quite differently, as we pointed out in our previous post. Both BMF and CIP are defined formally, and their transformation rules are correct. Usability applies to both methods, as numerous examples demonstrate. Yes, as far as manipulating functional programs, e.g. transforming one recursion pattern to another, is concerned, BMF has done a great deal more than CIP, and has developed a much conciser (and elegant, and at last uniform) notation. But this is due to the deliberate restriction of BMF to functional programming  which we do not condemn, but merely state as a fact that is relevant for the comparison above. Within functional programming, both methods do have the same power. We challenge you to present us a BMF law which cannot be expressed as a CIP transformation rule. Quote: >>CIP on the other hand, is meant as an overall method for program >>development [Boi92e]. One first specifies an algebraic data type  >>without the BMF constraint of polynomial types  and then has several >>layers of expression constructs for making programs over these data types. >If you can give an example of a datatype which uses nonpolynomial >constructors, I would be very interested! All datatypes occurring in >current programming languages, however, are polynomial.
You're right about the latter. But for instance bags (multisets) or (finite) sets are not expressible as a polynomial datatype, since additionally laws are needed to express commutativity and idempotency. Certainly, under some conditions, they can be represented by one (e.g., finite sets over an ordered carrier set as ordered sequences without multiple occurrences), but this has not been a topic of research within BMF. With respect to datatypes with laws, only Chapter 5 of Maarten Fokkinga's PhDthesis comes to mind, which certainly is promising for the future. But then, to actually implement these datatypes with laws in an everyday programming language, you still need some kind of representation theorem in order to obtain an isomorphism between the datatype with laws and a (subset of a) purely polynomial datatype. Quote: >>Thus one can start program development with a very abstract >>specification and stepbystep transform this into a concrete, >>executable program. An overview over the method is given in [Par90a]. >>Since all language layers (algebraic, descriptive, functional, >>imperative) are combined in one, formally defined, language [CIP85], >>the transformations from one layer to another are correct. >I don't see how this can guarantee correctness. I think that you always >have to prove correctness of the transformation steps yourself.
No! Just like in BMF, CIP transformational rules are of the form condition(s) => E1 = E2 Furthermore, some rules establish a refinement between E1 and E2, which is not possible in BMF as it has no nondeterministic constructs. Here, E1 and E2 are *expression schemes* rather than expressions. After matching E1 (or E2 for that matter) with your actual expression, giving a substitution s, and checking the condition(s), the actual transformation step s(E1) > s(E2) can be established. So, not the transformation *steps* have to be proven correct, only the general transformation *rules*. Quote: > ... It >doesn't really matter if you use one language or more, in this respect.
In theory you're right. But it can be quite a pain in the ass to try to make an "interface" of transformation rules between two completely different languages. In view of that, a wide spectrum language comprising various layers which have been tuned to one another, like CIPL, gives better support to program development than using a different language for every layer. For example, in CIPL, transformation from (tail)recursive functional programs to imperative, iterative programs is straightforward: f:: m > r f x = H(x), if B(x) = f (K(x)), otherwise ^  +  v function f (x : m) r; begin var vx : m := x; while not(B(x)) do vx := K(vx); f := H(vx) end; where for the sake of clarity, for the functional program a Mirandalike syntax is used, and for the imperative part Pascallike syntax. Furthermore, B, H and K are arbitrary expressions only containing x as free variable. The double arrow means that both programs are equivalent. Quote: >It helps if your language is formally defined (it helps even more if it >is simple, like BMF), but that doesn't take away the proof obligations.
It helps? I should say, it is an absolutely necessary prerequisite to have it formally defined. Greetings, Daniel Tuijnman Max Geerling
 Daniel Tuijnman

Sat, 07 Jan 1995 21:08:43 GMT 


Nico Verw #5 / 8

BirdMeerten Formalism
writes, as a followup to my posting, that CIP is a `widespectrum' programming language, capable of expressing abstract, nonexecutable specifications, as well as concrete programs (both imperative and functional). Quote: >Within functional programming, both methods do have the same power. We >challenge you to present us a BMF law which cannot be expressed as a CIP >transformation rule.
I suppose you can encode BMF in CIP, but that was not my point, and hence you thought that I was ``not serious''. I stated that, in my opinion, BMF is much conciser, and simpler to learn, than CIP. On the other hand, there is not yet a system for automatic reasoning in BMF. There is such a system for CIP, although I recall the demonstration of it at CWI, where attempts to transform the program `1+1' to the more efficient program `2' ended in a core dump, after some 15 minutes of trying the thing to work. Making things concise and simple is the _aim_ of BMF. For instance, using category theory has reduced the number of different laws dramatically. Being able to do everything is the aim of CIP. But that has lead to an enormous system, which is hard to master. Quote: >>>[In CIP] One first specifies an algebraic data type  >>>without the BMF constraint of polynomial types  and then has several >>>layers of expression constructs for making programs over these data types. >>If you can give an example of a datatype which uses nonpolynomial >>constructors, I would be very interested! All datatypes occurring in >>current programming languages, however, are polynomial. >You're right about the latter.
to me in a mail. For instance, the type of finitely branching trees is not. It is the least fixed point of the functor \lambda X . A + (X*) where X* means lists of X. There is a list functor (*) in there, which is not polynomial. This can be circumvented, however, by viewing this as a manysorted algebra, and defining lists and finitely branching trees together. Another example of a nonpolynomial type is the type of functions from A to B, A > B. The restriction made in BMF is that some nice properties do not hold for such types, which do hold for polynomiallygenerated types. But you're not going to change that in CIP, I think. (That would be truly amazing!) Quote: >But for instance bags (multisets) or (finite) >sets are not expressible as a polynomial datatype, since additionally >laws are needed to express commutativity and idempotency... but this >has not been a topic of research within BMF. >[Maarten Fokkinga's work] ... But then, to actually >implement these datatypes with laws in an everyday programming language, >you still need some kind of representation theorem in order to obtain an >isomorphism between the datatype with laws and a (subset of a) purely >polynomial datatype.
\begin{plug} Read my latest technical report, ``Congruences and Quotients in Categories of Algebras'' for this. It gives a simple way to model equations in BMF, and gives the connections with ``everyday programming languages''. \end{plug} Can you point out (preferably in mail) what representation theorem you mean? I'm not quite sure about this, so maybe it's still in my paper as well.

Sun, 08 Jan 1995 22:57:10 GMT 


Leo Fegar #6 / 8

BirdMeerten Formalism
Quote: Nico Verwer writes: > On the > other hand, there is not yet a system for automatic reasoning in BMF.
There is an automatic theorem prover based on Fokkinga's paramorphisms. This work is described in the paper: L. Fegaras, T. Sheard, and D. Stemple. "Uniform Traversal Combinators: Definition, Use and Properties" In eleventh International Conference on Automated Deduction (CADE11), Saratoga Springs, New York, June 1992. Leo Fegaras

Tue, 10 Jan 1995 00:03:33 GMT 


Eerke Boit #7 / 8

BirdMeerten Formalism
Over four years of discussion within the Dutch STOP project have led to a certain amount of consensus about the "CIP vs. BMF" issue. Now, moving on to the other important discussion, transformation systems: Quote:
>[..] BMF is much conciser, and simpler to learn, than CIP. On the >other hand, there is not yet a system for automatic reasoning in BMF.
Chisholm/Backhouse, and by Lindsey. That no system exists to do everything one could want it to, well, that's no surprise. See our "Ustopia" report for a list of interesting requirements. Quote: >There is such a system for CIP, although I recall the demonstration of >it at CWI, where attempts to transform the program `1+1' to the more >efficient program `2' ended in a core dump, after some 15 minutes of >trying the thing to work.
I must concur that the CIP *prototype* system (written at TU Munich in the early 80's, Riethmayer et al.) has not done much for the popularity of program transformation systems, to say the least. We asked a student to work with it for a few months, and he wasn't much more enthusiastic than Nico is. This may be partly due to the *prototype* character of the system, and to the {*filter*} machines on which it was first brought up. Most of the early work on program transformation systems was aimed at showing the feasibility of the approach, and not as much on the practicability of the systems, I'm afraid. Our group is currently experimenting with the "real" CIPS transformation system, a modern (really) windowbased system developed more recently by TU Munich and Siemens. Our first experiences are much more positive than those with the prototype system. We hope to report more extensively on this later. 
Dept. of Informatics (STOP Project) University of Nijmegen, NL

Mon, 23 Jan 1995 21:08:34 GMT 


