[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?)]
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
ELSE reduce?(f1) AND reduce?(f2)
ENDCASES MEASURE id BY <<
On Wed, 2006-05-24 at 06:00, 许庆国 wrote:
> Hello every one:
> I have a smaple theory :
> Reduce: THEORY
> 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)
> 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
> 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.
Cesar A. Munoz H., Senior Staff Scientist mailto:email@example.com
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