Fwd: Re: Maude licensed under GPL, 2.0 approaching

[Alexis Read]

On Tue, 3 Jun 2003, Massimo Dentico wrote:

> > Bootstrapping will depend on what is in maude 2.0 -i haven't looked
> > yet but i think there's a compiler, if so then very possible.
>
> >From a brief (my fault: my english is horrible) conversation on IRC with
> Brian Rice about Maude, I know some details of its internals and I think
> you are referring here to a compiler, in C++, from rewriting rules to
> Binary Decision Diagrams (BDDs), not to machine code.
>
> The release of open source Maude is imminent so I think I can "reveal"
> that it is based on this library:
>
>   BuDDy - A Binary Decision Diagram Package
>   - http://www.itu.dk/research/buddy/
>
My apologies - I haven't looked at the maude 2.0 code and assumed that
the compiler produced C++ or machine code output. I don't know anything
about BDDs so can't say anything useful here...

> >> a) how to express in M/T the transformation from term rewriting
> >> to BDD (I don't know if this makes sense: I'm speaking without
> >> a true knowledge of the Maude implementation). In case for M/T
> >> we can research how to go beyond term (or graph/string/whatever)
> >> rewriting and capture the concept of rewriting in general,
> >> abstracting from the nature of base objects with our abstract
> >> notion of object (or someone have done this already?);
>
> Maude, from what I know, is a *term* rewriting system. There are other
> rewriting systems based on graphs, trees, strings: I was questioning
> myself if it is possible to abstract the nature of the objects being
> rewritten. It was a pure speculation from my part, perhaps not so useful.
>
> For the Tunes perspective about the term "object" see CTO definition:
>
>   - http://cliki.tunes.org/Object

Ok.
I think that this paper
http://maude.cs.uiuc.edu/papers/postscript/tcs4012.ps.gz
(Rewriting logic as a logical and semantic framework)
discusses the equivalences between term rewriting and other forms of
rewriting. (I haven't got my refs to hand at the moment though) What I'm
trying to say is that these are mathematical equivalences so unless there
is an abstraction to show that term rewriting is a specialised case of
rewriting (and hence reflection), this is as general as it gets for the
moment, short of doing your own math proofs to show otherwise. (note, as
far as i've read)

My take on the def of an object vs the cliki version is that every object
has attributes (that make up its data type) - these are the defining
properties of it. For every object there is a supertype for representing
the object's attributes and so on up the abstraction tree. Providing that
the reflection implementation is 'complete', you have abstracted your
object concept (I'm probably stating the obvious here!)

>
>
> >> b) how to model low level (machine) entities, beginning from the CPU,
> >> in M/T;
> >>
> > b) maude can already do this - most circuits are designed in VHDL which is
> > a more primative precursor to maude.
> > You can even probably write a specification translator to move the hardware
> > spec across to maude.
>
> Are you sure? From what I recall VHDL is procedural (but I could be wrong,
> never used really), not declarative based on rewriting rules as Maude.
> Are you speaking about the module systems? There are probably some analogy
> between the two but this don't change the fact that they are based on
> different paradigms.

Pretty sure. See next post.

>
> Anyway, the possibility of modelling an instruction set or other kind of
> hardware resources was not in question. "How" in my original post means
> really "what model(s) to choose that satisfy our requirements?"

Ok. I've got the wrong end of the stick then :o)
I'd imagine taking maude, extending it with BOBJ's rewriting algorithms
and moving as many commands/structures etc. out of the maude interpreter
i.e. boolean operators and so on are currently using ID hooks to the
interpreter as their attributes. It is less efficient but better from an
abstraction point of view to define them completely in maude.
This should leave you with a small VM-style kernel (cpu driver for want
of a better phrase) and (hopefully) a usable compiler/partial evaluator/
driver for each piece of hardware. Everything else should be maude-native
a la squeak.
>
>
> >> c) at last, how to map the transformation in a) in terms of entities
> >> in b);
> >>
> > c) See any of the maude tutorial examples to see how this can be done.
>
> Again, probably I was not very clear: I have no doubts that Maude can
> express this transformation and I can add that IMO it can express it
> in a more clear and succint ways that in other paradigms.
>
> This is like to say that in Maude one can express a compiler, an interpreter,
> a partial-evaluator, an aspect waver (AOP), a tool to refactor code: no doubts
> from my part.
>
> But how organize this transformations in a way conforming to Tunes
> principles is an open question.

I'll just shut up now on this - we're talking about details which are the
devil! Personnally, i'll be trying to either write a proper
compiler/evaluator for maude or porting in BOBJ stuff.
>
>
> >> 3) co-evolving the spec with feedback from 1) and 2).
> > [..]
> >
> > 3) This is a topic to look at once a start has been made surely :o)
> >
> > Maude will always be useful as it has solid math foundations for the
> > language, it is to my knowledge the most state of the art system available
> > and there are a few choices (most of them in the same language family).
> > BOBJ runs a close second, and the algorithms need to be incorporated into
> > maude.
> > Alexis
> >
>
> This could be a god news for this project: are we gradually approaching a
> shared agreement about Maude as good platform to bootstrapping (at least
> some aspects of) Tunes?

Check the posts from 2 years ago- people were talking about this then.
Alexis.

>
> Regards.
>
> --
> Massimo Dentico