[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: Lawrence Paulson <lp15@cam.ac.uk>*Subject*: Re: [PVS-Help] quotient constructions in PVS*From*: Paul Jackson <pbj@inf.ed.ac.uk>*Date*: Fri, 20 Aug 2004 16:28:55 +0100*Cc*: pvs-help@csl.sri.com*In-Reply-To*: Your message of "Thu, 19 Aug 2004 14:51:28 BST."<DE82F4A1-F1E6-11D8-90DD-00039384D4B8@cam.ac.uk>*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com

Lawrence Paulson <lp15@cam.ac.uk> wrote: > Can anyone refer me to a paper describing a quotient construction > performed using PVS? Does PVS provide any support for quotienting type > or set with respect to an equivalence relation? Hi Larry, if by `support' you mean some special built-in code, I would argue that PVS doesn't need any. I would cite as evidence the short collection of PVS theories on quotienting I described in my post to the pvs and isabelle-users maillists on 20th May this year (I've included a copy of the relevant part of the post below). I would be interested in hearing about what support beyond this you or others might consider desirable. - Paul. -------------------------------------------------------------------------- Quotients in PVS -------------------------------------------------------------------------- Quotient types are straightforward to define in PVS. I've experimented with them a few times: - in the construction of integers as pairs of naturals, - in the essence of the first isomorphism theorem for groups, - in a proof of the Myhill Nerode theorem. None of this is published, but if anyone is interested, I've put the PVS theory files up at: http://www.dcs.ed.ac.uk/home/pbj/pvs/ I've also included explicitly below a PVS theory file sketch of this work that hopefully gives the idea of how one can approach quotients in PVS. Particular capabilities that one gains with PVS's type theory as compared to that of HOL or Isabelle/HOL include: - Since the PVS type theory includes subtypes, quotient types can be directly defined from predicate sets without the need for a typedef facility with abstraction and representation functions. - It's useful that types can take value arguments. E.g. given a function f : A -> B, one can define a type Quot(f) which contains a set of equivalence classes of A induced by the equivalence relation E(x,y) = (f(x) = f(y)). Another example is if you want to define a type Mod(n) for the integers mod n. If you are using HOL or Isabelle/HOL, I would guess you could get much of these capabilities using something like Joe Hurd's predicate subtyping approach. See his TPHOLs 2001 paper: http://www.cl.cam.ac.uk/users/jeh1004/research/papers/subtypes.html % Sketch of one way of doing quotients in PVS % PVS notation: % set[A] = [A->bool] % equivalence?[A](R) says that R is an equivalence relation % If s : [T->bool], (s) is the type of all elements a of T for which s(a) % is true. % PVS theories have parameters in [] at start of theory definition. % These implicitly parameterise each definition introduced in the theory. % When definitions are used, such parameters can often be automatically % inferred, though they can also be explicitly supplied. % Below, most of the theory switching is used to alter which % definition arguments are optional. quot_demo_1 [A : TYPE+] : THEORY BEGIN x,y : VAR A E : VAR (equivalence?[A]) eclass(x,E) : set[A] = {y | E(x,y)} % e(quivalence) class of x Z : VAR set[A] Qset(E) : set[set[A]] = {Z | Exists x : eclass(x,E) = Z} Qtype(E) : TYPE = (Qset(E)) % Qtype[A](E) is the quotient type A/E ecl(x,E) : Qtype(E) = eclass(x,E) % An example lemma for eliminating quantification over Qtype: qtype_forall_elim : LEMMA Forall (P : pred[Qtype(E)]) : (Forall (U :Qtype(E)) : P(U)) = (Forall (x : A) : P(ecl(x,E))) % The indefinite choice operator `choose' selects out elements % of equivalence classes. END quot_demo_1 % Here we switch to theory with E as additional parameter, so E is % optional value argument to `rep' function. (Both A and E args to % rep should be inferrable from the type of its argument U) quot_demo_2[A : TYPE+, E : (equivalence?[A]) ] : THEORY BEGIN IMPORTING quot_demo_1[A] U : VAR Qtype(E) rep(U) : A = choose(U) % rep(resentative) of U % The following lemmas abstract away from any need for further % fiddly reasoning with choose. x : VAR A rep_ecl : LEMMA E(rep(ecl(x,E)), x) ecl_rep : LEMMA ecl(rep(U),E) = U END quot_demo_2 functions_1 [D,R : TYPE] : THEORY BEGIN x1,x2 : VAR D f : VAR [D->R] E : VAR (equivalence?[D]) respects?(E)(f) : bool = Forall x1,x2 : E(x1,x2) => f(x1) = f(x2) END functions_1 % In some circumstances it is more elegant to extract % elements using a `lifting' operator qlift that lifts E-respecting % functions of type A->B to type (A/E)->B: quot_demo_3 [A:TYPE+, E:(equivalence?[A]), B:TYPE] : THEORY BEGIN IMPORTING quot_demo_2[A,E], functions_1 f : VAR [A->B] U : VAR Qtype(E) qlift(f)(U) : B = f(rep(U)) x : VAR A qlift_elim : LEMMA Forall (f:(respects?[A,B](E))) : qlift(f)(ecl(x,E)) = f(x) END quot_demo_3

**References**:**[PVS-Help] quotient constructions in PVS***From:*Lawrence Paulson <lp15@cam.ac.uk>

- Prev by Date:
**[PVS-Help] quotient constructions in PVS** - Next by Date:
**[PVS-Help] Example of PVS -raw mode** - Prev by thread:
**[PVS-Help] quotient constructions in PVS** - Next by thread:
**Re: [PVS-Help] quotient constructions in PVS** - Index(es):