🚀 go-pugleaf

In article <1992Jul20.160706.10025@cs.ruu.nl> nico@cs.ruu.nl (Nico Verwer) writes:
>In <1992Jul17.142218.7319@sci.kun.nl> daniel@cs.kun.nl (Daniel Tuijnman) writes:
>>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.

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

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

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

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

>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@cs.kun.nl		max@cs.kun.nl
-- 
Daniel Tuijnman
daniel@cs.kun.nl