Bird-Meerten Formalism
Author Message
Bird-Meerten Formalism

Bird-Meerten Formalism
----------------------

Considering Bird-Meertens 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, Addison-Wesely
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
Bird-Meerten Formalism

Quote:

>          Bird-Meerten Formalism
>      ----------------------

In our Software Engineering group in Nijmegen, The Netherlands, we work
on both formalisms mentioned hereunder, the Bird-Meertens Formalism
(BMF), and the CIP wide spectrum language [CIP85]. Since Helmut Partsch
is our professor, and former member of the Munich CIP-project, 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 Bird-Meertens 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
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 morphism-aspect 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 so-called
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 step-by-step 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 Bird-Meertens Formalism:

Bir87,
Author= {Bird, R.S.},
Title= {An Introduction to the Theory of Lists},
Pages= {5--42},
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,
Year= 1987}

Bir89b,
Author= {Bird, R.S.},
Title= {Lectures on Constructive Functional Programming},
Crossref= {NATO.ASI.F55},
Pages= {151--218}}

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,
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= {66--90},
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 {Bird-Meertens} 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= {9--32},
Crossref= {TC2-91}}

TC2-91,
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,
Year= 1991}

On the CIP formalism:
...

Tue, 03 Jan 1995 22:22:18 GMT
Bird-Meerten 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 lambda-calculus, 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 non-polynomial
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 step-by-step 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
Bird-Meerten 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 CIP-S
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 non-polynomial
>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 PhD-thesis 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 step-by-step 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
CIP-L, gives better support to program development than using a
different language for every layer. For example, in CIP-L,
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 Miranda-like
syntax is used, and for the imperative part Pascal-like 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
Bird-Meerten Formalism

writes, as a follow-up to my posting,

that CIP is a wide-spectrum' programming language, capable of
expressing abstract, non-executable 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 non-polynomial
>>constructors, I would be very interested! All datatypes occurring in
>>current programming languages, however, are polynomial.

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 many-sorted algebra, and defining lists and finitely branching trees
together.
Another example of a non-polynomial 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 polynomially-generated 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
well.

Sun, 08 Jan 1995 22:57:10 GMT
Bird-Meerten 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
(CADE-11), Saratoga Springs, New York, June 1992.

Leo Fegaras

Tue, 10 Jan 1995 00:03:33 GMT
Bird-Meerten 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" CIP-S
transformation system, a modern (really) window-based 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

 Page 1 of 1 [ 8 post ]

Relevant Pages