conditional equations in Maude

[Santiago Escobar]

Dear Steven (and Maude users),

In many functional programming languages, such as Haskell, the let  
expressions allow a programmer to explicit say what is shared or not.  
This has another benefit, ie readability of the code. In Maude, one  
has to use conditions of the form "Variable := Expression" but it  
seems that Maude then treats such equation as conditional and the  
performance is degraded.

Would it be possible to detect that some condition is going to return  
only one possible matching, like in conditions of the form  
"Variable := Expression", an avoid the conditional infrastructure?

Another possibility can be a cut operator, as in logic programming,  
described as a new class of conditions of the form "Exp1 :== Exp2"  
that has a mix meaning between "Exp1 := Exp2" and "Exp1 = Exp2", ie a  
condition using :== implies a matching, as in a condition using := but  
a confluent matching, as it happens in conditions using =.
In other words, ::= means a matching but without backtracking, which  
is safe only if one possible matching exists.

I raise this question because I am writing Maude specifications quite  
often and I have a big issue with performance of Maude with  
conditional equations containing matching conditions. But a big big  
issue of performance.

Many thanks.
Best,
-Santiago


________________________________________________________
Santiago Escobar
    Dept. of Information Systems and Computation (DSIC)
    Technical University of Valencia (UPV)
    Camino de Vera, 14. E-46022 Valencia (Spain)
   e-mail: sescobar@...
   URL:    http://www.dsic.upv.es/~sescobar
   Phone:  [phone] (Ext. 73556)
   Fax:    [phone]
                           
_______________________________________________
Maude-users mailing list
Maude-users@...
http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-users

[Steven Eker]

Hi Santiago,

On Monday 16 June 2008 14:00, Santiago Escobar wrote:

> In many functional programming languages, such as Haskell, the let
> expressions allow a programmer to explicit say what is shared or not.
> This has another benefit, ie readability of the code. In Maude, one
> has to use conditions of the form "Variable := Expression" but it
> seems that Maude then treats such equation as conditional and the
> performance is degraded.
>
> Would it be possible to detect that some condition is going to return
> only one possible matching, like in conditions of the form
> "Variable := Expression", an avoid the conditional infrastructure?

It is not the potential for multiple matches that incurs the overhead of the
conditional infrastructure but rather that Expression needs to be evaluated
in a side computation. Maude uses a lot of preallocated data structures in
the rewrite engine to avoid expensive memory allocations at runtime. The
downside is that if you start an side evaluation before the current rewrite
step is complete, all of these structures have to be saved, just in case they
were in use by the current rewrite step, and will be overwritten by the side
evaluation. Of course this saving requires a lot of memory allocations and
copying, followed by a lot of copying-back and memory deallocations when the
side evaluation is finished. Thus conditional rewriting is typically more
than an order of magnitude slower than unconditional rewriting.

In prinicple it might be possible to recognize the "Variable := Expression"
idiom and compile it away into node sharing in the rhs construction
automata...except that would be subltly incorrect in the case of operator
strategies.

> Another possibility can be a cut operator, as in logic programming,
> described as a new class of conditions of the form "Exp1 :== Exp2"
> that has a mix meaning between "Exp1 := Exp2" and "Exp1 = Exp2", ie a
> condition using :== implies a matching, as in a condition using := but
> a confluent matching, as it happens in conditions using =.
> In other words, ::= means a matching but without backtracking, which
> is safe only if one possible matching exists.

As I mentioned above, it is the side evaluation that is very expensive, not
the matching.

> I raise this question because I am writing Maude specifications quite
> often and I have a big issue with performance of Maude with
> conditional equations containing matching conditions. But a big big
> issue of performance.

You can always get the effect of sharing with an auxiliary operator.

ceq f(X) = F(G(Y), H(Y)) if Y := L(X) .

becomes

eq f(X) = aux(L(X)).
eq aux(Y) = F(G(Y), H(Y)) .

for large contexts F, G, H and L and a suitable declaration for aux. This has
very little runtime overhead. Of course if more variables are involved the
aux operator will need more arguments.

Steven
_______________________________________________
Maude-users mailing list
Maude-users@...
http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-users