Re: [isabelle] Questions on type classes for lattices



Hi Alessandro,

> Since a (non-empty) finite lattice is also complete, I would like to
define
> 
>   class finite_lattice = finite + lattice
> 
> and then prove
> 
>   instance finite_lattice < complete_lattice
> 
> after giving suitable definitions for Inf/Sup/bot/top.
> 
> But apparently
> 
>   instance A < B
> 
> requires A to have (at definition time) all the operators of B. Are
> there "deep" reasons for this requirement, or could it be relaxed with
> relative ease to allow the extra operators to be defined after A has
> been defined and then used to show that A is a subclass of B?

this is a well-known restriction of type classes.  The short answer is,
no, this restriction cannot be lifted.  This is the price you have to
pay to have operations *and* assumptions about them: in order for a
structure to be a complete lattice, it is not necessary that there exist
operations which satisfy its properties, but these operations must be
explicitly defined for that particular type.

> Anyhow, given the current situation, one approach is to define
> finite_lattice as above, define Inf/Sup/bot/top on finite_lattice

Such definitions would be rejected, since they violate the rules for
overloading: Inf/Sup/bot/top can only be instantiated on particular type
constructors, not (sort-constrained) type variables.

> Another approach is to define class finite_lattice to include
> Inf/Sup/bot/top, along with assumptions that define these four operators
> in terms of the existing operators of finite_lattice. In this way,
> finite_lattice can be a subclass of complete_lattice. The drawback is
> that proving that a type L has class finite_lattice will require more
> work because of the extra operators and assumptions that must be
> satisfied (but perhaps this work can be eased by proving and using
> general lemmas that relate Inf/Sup/bot/top to inf and sup). Furthermore,
> the approach seems (to me) methodologically less clean than the previous
> one.

IMHO it is the cleanest one you can achieve inside the current
infrastructure.  E.g.

> lemma finite_complete_lattice:
>   assumes Inf: "\<And>A. (Inf :: ('a::{Inf, Sup, bounded_lattice, finite}) set ⇒ 'a) A =
>     (if A = {} then top else Inf_fin A)"
>   assumes Sup: "\<And>A. (Sup :: ('a::{Inf, Sup, bounded_lattice, finite}) set ⇒ 'a) A =
>     (if A = {} then top else Sup_fin A)"
>   shows "OFCLASS('a::{Inf, Sup, bounded_lattice, finite}, complete_lattice_class)"
> proof

> A third approach is to define
> 
>   class finite_lattice = finite + complete_lattice
> 
> and avoid proving subclass relations altogether. The drawback is that
> proving that a type L has class finite_lattice is even more work (but
> again perhaps this work can be eased by suitable general lemmas).

This does indeed save you nothing on instance proofs.

> This
> seems to be the approach taken in the library definition of class
> complete_lattice, which includes bounded_lattice explicitly, even though
> Inf and Sup suffice. Also, this approach seems (to me) methodologically
> less clean than the previous two.

The issue is that class bot already demands assumptions on bot and thus
you cannot instantiate bot without actually proving these.

There have been two ideas around to lift this somehow:
* Provide purely syntactic classes for operations without further
assumptions; this has a long tradition in isabelle (cf. plus, times,
zero etc.), but has the disadvantage that you can write down things
syntactically which do not obey properties you would expect naively
(i.e. "a + 0 = a" does not hold in general).
* Build a fancy wrapper around instantiation in the spirit of Haskell
default class method definitions.  Since this must also cover proofs, it
would be a tedious affair and maybe not worth doing it.

Cheers,
	Florian

-- 

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.