Maude-help mailing list

["andrea.vandin AT imtlucca.it IMT" <andrea.vandin AT imtlucca.it>]

Hi,

just add the following line at the end of the module:

eq sort(NL1) = NL1 [ owise ] .

The "owise" keyword instructs maude in applying this equation only if no other equations can be applied. Hence, it will be applied on the final sorted list only.

Actually, note that now you can remove the following equation: eq sort(nil) = nil .

Regards,

Andrea Vandin

This is the complete specification:

fmod SORT is

   inc LIST{Nat} .

   vars NL1 NL2 NL3 : List{Nat} .

   vars M N : Nat .

    op  sort : List{Nat} -> List{Nat} .

    eq sort(NL1) = NL1 [ owise ] .

   ceq sort(NL1 M NL2 N NL3) = sort(NL1 N NL2 M NL3) if N < M .

   

endfm

*** red in SORT : sort(11 12 55 3 2 1) .

*** result NeList{Nat}: 1 2 3 11 12 55

On Tue, May 3, 2016 at 12:04 PM, Francesco Bongiovanni <bongiovanni AT gmail.com> wrote:

Hi everyone,

I found what I consider a beautiful one-line piece of code that does sorting
by term rewriting on Helene Kirchner slides
(https://wiki.bordeaux.inria.fr/Helene-Kirchner/lib/exe/fetch.php?media=wiki:rcdlecture.pdf)
(on slide 15)

fmod SORT is
   inc LIST{Nat} .

   vars NL1 NL2 NL3 : List{Nat} .
   vars M N : Nat .

    op  sort : List{Nat} -> List{Nat} .
    eq sort(nil) = nil .

   ceq sort(NL1 M NL2 N NL3) = sort(NL1 N NL2 M NL3) if N < M .

endfm

*** red in SORT : sort(11 12 55 3 2 1) .
*** result List{Nat}: sort(1 2 3 11 12 55)

What I would like is to have a proper List{Nat} as a result without the `sort`
before as I would like to do operation on the result list; e.g head( sort(11
12 55 3 2 1)) would result in result [List{Nat}]: head(sort(1 3 5 22 26 44))
instead of 1 as I would like.

Do you think its possible ?

Thanks a lot for your insights !

- Francesco

ps: in order to pre-answer some remarks, yes I know there are plenty of
materials around sorting and many quicksort/mergesort example in Maude, but I
wish to keep this one line :D

--

Andrea Vandin, PhD

Assistant Professor

SysMA Research Unit
IMT - Institute for Advanced Studies Lucca, Italy

URL: http://www.imtlucca.it/andrea.vandin

e-mail: andrea.vandin AT imtlucca.it