[isabelle-dev] NEWS / CONTRIBUTORS

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Sep 15 16:33:03 CEST 2011


Hi Lukas,

> The rename AssocList to AList_Impl was actually already glimpsing into
> the future, where there will exist an abstract AList, as our brave users
> have already done this in the AFP-Collections framework.
> 
> I now followed your suggestion, but in the future, this will be revised
> once again, until the Isabelle/ML library and the HOL/Library theories
> coincide.

the point I am hinting at is that association lists are not an abstract
type.  Of course you can use them to implement finite mappings, but in
practice you can do much better using trees or something similar.

When Markarius and me where pondering whether to abandon association
lists in Isabelle entirely, we came to the conclusion that there are
applications beyond simple mappings:

(1) mappings with history
(2) access with different notions of equality
(3) grouping and coalescing entries with the same keys

Leaving aside that in Isabelle (2) is not easy to get, all those issues
speak against turning association lists into an abstract type, except
maybe for scholastical reasons.

Cheers,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110915/3ec77405/attachment.sig>


More information about the isabelle-dev mailing list