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

Re: [PVS-Help] reduce adt



Regardless of PVS, you cannot define 

reduce : [Conj -> (true_free?)]

such that 

reduce(True AND True AND True) = True

because, according to your definition, true_free?(True) = FALSE.

Furthermore, although PVS supports overloading, it doesn't seem a good
idea to overload True and And. Notice, for example, that in your
definition of reduce "reduce?(f1) AND reduce?(f2)" you are using the
constructor "AND" rather than the boolean operator. 

Maybe, you want to define something like:

true_free_or_true(f) : bool =
  true_free?(f) OR f = True 

reduce(f: Conj): recursive (true_free_or_true?)  = CASES f
          OF AND(f1, f2): IF reduce?(f1) = True THEN reduce?(f2)
                               ELSIF reduce?(f2) = True  THEN
reduce?(f1)
                               ELSE reduce?(f1) AND reduce?(f2) 
                               ENDIF, 
             ELSE Conj
        ENDCASES   MEASURE id BY <<

Cesar


On Wed, 2006-05-24 at 06:00, 许庆国 wrote:
> Hello every one:
> 
> I have a smaple theory :
> 
> Reduce: THEORY
> 
> BEGIN
>   Conj: DATATYPE   BEGIN
>    True : TURE?
>     Hold(b: bool): a?
>     AND(a1, a2: Data): and?
> END Conj
> 
>   f: VAR Conj;
> 
>   |=(f): RECURSIVE bool =
>    CASES f OF Hold(b): b, 
>         True: true,
>         AND(a1, a2):  |= (a1) AND |= (a2) 
>    ENDCASES    
>   MEASURE id BY <<
> 
>   true_free?(f):  INDUCTIVE bool =
>         CASES f
>           OF AND(f1, f2): true_free?(f1) AND true_free?(f2), True: FALSE
>           ELSE TRUE
>           ENDCASES
>  reduce(f: Conj): recursive (true_free?)  = CASES f
>           OF AND(f1, f2): reduce?(f1) AND reduce?(f2), True: ...,
>              ELSE TRUE
>         ENDCASES   MEASURE id BY <<
> 
> 
> 
>       ...
>  END Reduce
> 
>    I want to reduce an arbitrary  fomula of datatype "Conj" to compact form:
> i.e., for instance,
> 
>    "b1 AND True AND (True AND True)"  -->  b1,  %where  b1 is the form of Hold(b) for some b.
>     "True AND True AND True"  ---> True
> 
>    Is it possible to implement this process using a recursive fucntion in PVS? I cannot know how to deal with True.
> 
> 
> Can you give me some hints?
> 
> 
> thank you in advance.
> 
> Q.G .XU.
> 
> 2006-05-24
-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace        mailto:C.A.Munoz@larc.nasa.gov
100 Exploration Way, Room 214       http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4