Fwd: Re: Maude licensed under GPL, 2.0 approaching

[Massimo Dentico]

On Mon, 2 Jun 2003 22:05:17 +0100 (BST), Alexis Read <ucapare@ucl.ac.uk> wrote:

>
> On Mon, 2 Jun 2003, Massimo Dentico wrote:
>> [..]
>>
>> My idea for a next step for Tunes is to advance in parallel different
>> aspects of the system:
>>
>> 1) to explore what we can "steal" from Maude as high level declarative
>> language and what to change or inject to approach Tunes ideas;
>>
>
> All of maude is useful. It IS possible to express the whole of maude
> within itself - see the online manual where it talks about a universal
> theory U that includes itself (this is mathematically demonstrated as
> well).

I know this, but is not incredible useful for bootstrapping the system
from itself and discarding the C++ part.


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


>> 2) how to express Maude implementation in Maude itself or how to bootstrap
>> our Maude/Tunes (M/T from now), or:
>>
>> 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?);
>
> a) Maude captures the concept of rewriting relatively completely as is
> known so far (mathematically), BOBJ extends the concepts in useful
> directions (both languages are in the same family).
> I'm not quite clear on what you mean by abstracting from the nature of
> base objects - maude supports user defined types and proofs on those
> types, BOBJ can do proofs on black-box code and other behavioral objects
> which is about as good as you can hope to get without a brain like
> newton's/einstein's etc.

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


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

Well, this is a simplification: the logic on which Maude is based can
arrange different paradigms. See for example:

  "A Hidden Herbrand Theorem: Combining the Object, Logic and Functional
  Paradigms"
  - http://citeseer.nj.nec.com/48960.html

(This is yet another paper that I need to study in depth).

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?"


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


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

Regards.

--
Massimo Dentico