An Introduction to the Bird-Meertens Formalism
by Jeremy Gibbons (link to paper).
Introduces the BMF, also called Squiggol, by using an example: a derivation of a linear algorithm to compute the Maximum Segment Sum of a list of numbers. The problem is presented in the book Programming Pearls by Bentley, and the derivation of the linear solution using Horner's rule apparently was first suggested by Bird. The paper first presents some motivation to using the formalism, then takes care of notation, proving some theorems by the way, then presents Horner's rule for polynomials and a generalization of the rule for arbitrary operations (that satisfy certain conditions). When the groundwork is completed, it presents a clear specification of the MSS problem that would take cubic time to compute; from this specification, using the theorems presented earlier and the generalized Horner's rule, it is derived an efficient linear algorithm based on list scans.
The paper is also interesting for showing the properties of catamorphisms and folds. Folds are more general than catamorphisms, but if the fold operation is associative, it can be expressed as catamorphism as well.
The paper makes the claim that "creativity is not needed" when deriving an efficient program from a simple specification. This doesn't seem to hold up well. Sure there is creativity somewhere in it, and although the derivation itself seems simple, it depends on the available theorems. So the choice of which theorems to state and prove, a priori (that is, when you don't know the answer beforehand) seems to involve a lot of creativity. Of course, the paper does not claim that you don't need creativity there, only in the derivation itself. Even so, the example presented is quite small. It uses only a handful of theorems, all of them stated earlier. So how does one go about choosing which theorems to use in a derivation? Is it trial and error? Isn't there some creativity involved? In a realistic formalism to derive programs from specifications, you'd probably end with lots of theorems. It seems to me that it is far from trivial to decide which one to use in each step. Maybe a experienced practitioner can decide where to go based on previous sessions of trial and error, by considering the "look" of the current expression.
Another problem is where to stop. How do you know you got an interesting, efficient implementation of your specifications? You must be able to recognize good implementations somehow. This isn't different from how you can express mathematical expressions in many ways, some more useful than others depending on circumstance. But the properties of good implementations are not clear.
All in all, claiming that "creativity is not needed" in the derivation process mostly makes me think it can be automated without resorting to AI techniques. But if you think about how to do it -- trial and error amounts to exponential search, lack of clear goals or evaluation criteria for results makes termination difficult to specify -- it becomes clear that implementing an automatic tool for derivating programs from specifications would be quite difficult. My doubts are mostly concerned with how a formalism like this would scale to the derivation of realistic programs, instead of small toys.
I've found the book by Bird and de Moor at a very good price in an online bookstore and ordered it. If it ever gets to me, we'll see how the formalism scales.
Introduces the BMF, also called Squiggol, by using an example: a derivation of a linear algorithm to compute the Maximum Segment Sum of a list of numbers. The problem is presented in the book Programming Pearls by Bentley, and the derivation of the linear solution using Horner's rule apparently was first suggested by Bird. The paper first presents some motivation to using the formalism, then takes care of notation, proving some theorems by the way, then presents Horner's rule for polynomials and a generalization of the rule for arbitrary operations (that satisfy certain conditions). When the groundwork is completed, it presents a clear specification of the MSS problem that would take cubic time to compute; from this specification, using the theorems presented earlier and the generalized Horner's rule, it is derived an efficient linear algorithm based on list scans.
The paper is also interesting for showing the properties of catamorphisms and folds. Folds are more general than catamorphisms, but if the fold operation is associative, it can be expressed as catamorphism as well.
The paper makes the claim that "creativity is not needed" when deriving an efficient program from a simple specification. This doesn't seem to hold up well. Sure there is creativity somewhere in it, and although the derivation itself seems simple, it depends on the available theorems. So the choice of which theorems to state and prove, a priori (that is, when you don't know the answer beforehand) seems to involve a lot of creativity. Of course, the paper does not claim that you don't need creativity there, only in the derivation itself. Even so, the example presented is quite small. It uses only a handful of theorems, all of them stated earlier. So how does one go about choosing which theorems to use in a derivation? Is it trial and error? Isn't there some creativity involved? In a realistic formalism to derive programs from specifications, you'd probably end with lots of theorems. It seems to me that it is far from trivial to decide which one to use in each step. Maybe a experienced practitioner can decide where to go based on previous sessions of trial and error, by considering the "look" of the current expression.
Another problem is where to stop. How do you know you got an interesting, efficient implementation of your specifications? You must be able to recognize good implementations somehow. This isn't different from how you can express mathematical expressions in many ways, some more useful than others depending on circumstance. But the properties of good implementations are not clear.
All in all, claiming that "creativity is not needed" in the derivation process mostly makes me think it can be automated without resorting to AI techniques. But if you think about how to do it -- trial and error amounts to exponential search, lack of clear goals or evaluation criteria for results makes termination difficult to specify -- it becomes clear that implementing an automatic tool for derivating programs from specifications would be quite difficult. My doubts are mostly concerned with how a formalism like this would scale to the derivation of realistic programs, instead of small toys.
I've found the book by Bird and de Moor at a very good price in an online bookstore and ordered it. If it ever gets to me, we'll see how the formalism scales.
Labels: functional, squiggol
posted by tautologico at
10:53 AM
0 Comments:
Post a Comment
<< Home