Re: [isabelle] the state of the lattice theories



Hi Peter,

first of all, HOL-Lattice is more an example than a library.  I would
guess that the lattice in HOL-Algebra is what you want to start an.  The
order development in HOLCF is traditionally something specific apart.

> Has there been enough exploration of this design space such that the one true order and lattice theory is waiting to spring forth?

Well, there *has* been a lots of effort to reduce the number of lattice
developments to effectively two.  For the background, I quote here from
an e-mail from isabelle-dev:

> a few years
> ago, around 2006, when I entered this type class adventure in more deep,
> I came to the conclusion that it is usually better to have
> »constructive« type classes, e.g. if we specify a semilattice as type
> class, we don't assume »there exists a inf such that …« but we add an
> explicit parameter »inf« which a corresponding set of properties.
> 
> Otherwise we would define »inf« with »THE x. …«, and this means that for
> particular instances of lattices (sets, nats, …) you have to derive
> type-specific primitive rules (e.g. inf on 0/Suc representation, inf on
> {}/insert representation) manually starting with a »THE x. …«
> definition.  In practice, it is much more straightforward to define inf
> on particular types directly and then prove that this instance conforms
> to its axiomatic specification.  As a side effect, you get reasonable
> code equations, something which can hardly be achieved if inf would be a
> generic polymorphic operation rather than a class parameter.
> 
> Of course, these constructive type classes are more specific than the
> mathematical concept they represent, but for meta-theory a
> record/locale-based approach with explicit carrier sets as in
> HOL-Algebra is much more feasible anyway.  But see also the funny lemma
> http://isabelle.in.tum.de/repos/isabelle/file/7270ae921cf2/src/HOL/Lattices.thy#l447
> which shows how even the contructive type classes are able to talk about
> uniqueness.

Cheers,
	Florian

-- 

PGP available:
http://www.haftmann-online.de/florian/florian_at_haftmann_online_de

-- 

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

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

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.