Formal derivation of an algorithm to test if two sequences have the same elements

[elih...@gmail.com]

Dear all,

Anyone know if there is an EWD/WF/AvG/AB/JAW etc that formally derives an algorithm to test if two sequences have the same elements?

Eric

[Kim-Ee Yeoh]

If by sequence you mean a list then functional programming-wise, all the work that’s merely needed is to state what’s meant (in other words, the definition) of when two lists are equal. You get a correct-by-construction algorithm for free from the definition.

Or do you mean equality testing on lists modeling multisets?

Kim-Ee

--
You received this message because you are subscribed the mathmeth.com mailing list.
To unsubscribe from this group, send email to Calculational-Math...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/Calculational-Mathematics?hl=en
---
You received this message because you are subscribed to the Google Groups "Calculational Mathematics" group.
To unsubscribe from this group and stop receiving emails from it, send an email to calculational-math...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/0b1ed8a8-75a7-48ed-8b3b-f68245da571fn%40googlegroups.com.

--

-- Kim-Ee

[elih...@gmail.com]

Well, two lists xs and ys are equal iff (A x :: x in xs == x in ys) .

Eric

[Kim-Ee Yeoh]

On Tue, Nov 22, 2022 at 4:07 AM elih...@gmail.com <elih...@gmail.com> wrote:

Well, two lists xs and ys are equal iff (A x :: x in xs == x in ys) .

Did you mean sets in the above? Or lists?

To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/44485ce8-4b6e-4c4f-8c74-4bde7874df37n%40googlegroups.com.

--

-- Kim-Ee

[elih...@gmail.com]

I mean lists/sequences (for example the program should find that [1,2,3] equals [3,2,1].)

[Kim-Ee Yeoh]

Does [1,2,3] also equal [1,1,2,3] ?

To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/ef4e6df2-90af-400f-b4a8-c13ece19f1a5n%40googlegroups.com.

--

-- Kim-Ee

[elih...@gmail.com]

In this case yes. Let set.xs be the set of elements in list xs. We want to compute xs ~ ys where:

xs ~ ys == (Ax :: x in set.xs == x in set.ys)