reflexive TRW tool

["Serge D. Mechveliani" <mechvel@botik.ru>]

Dear CASL tools developers,

I asked recently a couple of naive questions about CASL tools,
and thank  Peter Mosses <pdmosses@brics.dk>  who has given 
explanations.


>> What does provide CASL to support programming reasoning about
>> algebraic specifications?
>> The spec examples in documentation show the formulae like
>>     x + y    = y + x
>>     (x*y)*z  = x*(y*z)    (assoc)
>>     inv(x)*x = 1          (inv)
>>
>> So, one could guess that the language supports processing of explicit
>> equational laws: the feature natural for a `logical' kind of language.
>> For when one writes "(x*y)*z = x*(y*z)" in one's program, the program
>> is supposed to exploit such a law.

> One's program - in which language? CASL is for writing specifications, 
> not programs, and cannot be used directly in programming languages. 
> Some CASL specifications can be executed, e.g. by term rewriting or 
> resolution, but their semantics is model-theoretic, not operational.


I am starting to understand.
Probably, my questions is on the quality of available *tools*.
 
I dealt earlier with Computer Algebra  (CA).
And now thinking of some sort of open project of 

              computation system for mathematics 
              joined with the reasoning system, 
              and maybe, with FP program transformation. 

A system like "CA + proofs + program transformation", 
which is able to compute/prove, say, in algebra and in functional 
programming. Consider, for example, the formulae

  forall N M .  N + M = M + N                   for arithmetic and
  forall Xs .   reverse(reverse(Xs)) = Xs       for programs on lists.

This concerns proof "in variety" and in "initial model", 
scolemization, and such. 
But it should also support a mathematically adequate functorial
style of programming computations: to understand abstract classes
(categories, theories) and their instances -- concrete domains 
(models).

It is needed a  language_&_tool  of, let us call it

                 ATRL   -- Appropriate Term Rewriting Language

This is a (hypothetic) language_&_tool providing the following
features.

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

 (R) Reflection. 

 (KB) Some library for KBC variants is desirable, 
      besides, in any case, ATRL should fit well enough to express 
      KBC.

 (O) It should be  open-with-source,  supported, open for discussion
     (like, say, ML and Haskell are in the FP world).

I think of doing proofs  only by TRW,  without resolution.

And all the proof strategies have to be expressed in the very ATRL.

No extra strategy language is needed as soon as we have a good 
TRW language_&_tool with reflection.
For equations and modules are the Term data made, again, of operators, 
and the library function  meta-reduce(M, t)  applies a meta-coded 
module to term.

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 ?

The HOL-CASL prover also does not seem to fit the line described 
above.

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?

With kind regards,

-----------------
Serge Mechveliani
mechvel@botik.ru