Re: reflexive TRW tool

[Till Mossakowski <till@informatik.uni-bremen.de>]

Dear Serge,

>  (1) Order(many?)-sorted TRW,  maybe, membership axioms,
>      AC rewriting, abstract theories, parameterized modules,
>      views from theories, and such,
>      modules are considered as equational theories, a language
>      itself is not tied to any particular computation strategy;
>      equations separated to two sets: oriented (rules) and
>      bi-directed,  the set of o-rules can be applied by the
>      meta-reduce  library function,  b-equations  are subjected
>      only to individual  meta-apply  application.

This seems to be much in the vein what Maude implements for rewriting
logic.
We are currently implementing the heterogeneous CASL tool set. It will
integrate and relate different logics and tools. Once we have established
a link to Maude, the Maude approach also can be used for a subset of CASL.
 
>  (R) Reflection.

We have the idea of establishing a reflection for Isabelle/HOL.
Then, also HOL-CASL would come with reflection.
 
> I look into the CASL tools and do not see, so far, such ATRL.
> Maybe, someone can help me to discover such?
> (I am a newbie in the world of these tools, sorry if my impression
> occurs wrong).
> The TRW tools  ELAN, ASF  seem to lack reflection ...
> Do they need any special language beyond TRW to formulate strategies?
> For example, how to program in ELAN various uninfication versions,
> KBC?  In ASF ?

As far as I know, there are strategy languages, but no reflection.

> Imagine a sublanguage of CASL including the features (1)
> -- expressing this modern version of TRW logic
> (is it a sublanguage?).
> Let us call it          SubCASL-1.
> Also imagine a tool     SubCASL-1-tool
> 
> providing an Interpreter (rewrite engine) for SubCASL-1 modules and
> a Library with  meta-reduce  function, sorts and items to express
> reflection and meta-coding.
> I think, reflection here is NOT an addition to language,
> it is simply a matter of certain library module. Right?
> 
> What CoFI community has for such  SubCASL-1-tool ?
> Does it have sense to develop such a tool?

See my remarks about a CASL subset, used in the heterogeneous
CASL tool set.

Indeed, we would be grateful to cooperate with people being more
involved in rewriting and reflection when doing the integreation
in the heterogeneous CASL tool set.

Greetings,
Till
-- 
Till Mossakowski                Phone +49-421-218-4683
Dept. of Computer Science       Fax +49-421-218-3054
University of Bremen            till@tzi.de           
P.O.Box 330440, D-28334 Bremen  http://www.informatik.uni-bremen.de/~till