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

Re: [PVS-Help] quotient constructions in PVS



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