Remove duplicate elements: Difference between revisions

The parametrized module NO-DUP-LIST(ELEMENTS :: TRIV) defines the signature of simple Haskellspace likeseparated list structure. The removal of duplicates is handled by the equational properties listed after the signature in brackets {}. There is no user written code in module NO-DUP-LIST. The binary operation _,_ is associative, commutative, and idempotent, meaning (x , x) = x. This list structure does not permit duplicates, they are removed during evaluation (called reduction in CafeOBJ). Using this module we can perform set union, just by evaluating two lists e.g:

op _,___ : Elt Elt -> Elt { comm assoc idem assoc }

red 2 , 1 , 2 , 1 , 2 , 1 , 3 .

-- Gives (2 , 1 , 3):Int

reduce 1 , 1 , 2 , 1 , 1 .

reduce 'a' , 'b' , 'a' , 'a' .

reduce "abc" , "def" , "abc" , "abc" , "abc" .

<lang> (1 , 1 , 2 , 1 , 1)</lang>

<lang> (1 , ((1 , 2) , (1 , 1))) </lang>

We get rewrite ''(1 , 1) -> 1'' . The term is now:

<lang> (1 , ((1 , 2) , 1)) </lang>

By idempotency applied at inner brackets ''(1 , 2) ''.

We get rewrite ''(1 , 2) -> 2 ''. Term is now:

<lang>(1 , (2 , 1))</lang>

<lang>(2 , 1)</lang>