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

Re: Mathematical and PVS syntactic equivalence?




how about

  my_add (I : REALSET, delta : real) : REALSET = 
	{t : real | member(t - delta, I)}

?

John





> 
> Hello,
> 
> Giving a set of reals S, I am trying to specify a + operation which
> constructs another set being the same as S except that every member has
> been added a fixed constant:
> 
> In PVS I wrote:
> 
>   REALSET: TYPE = setof[real]
>   ; + (I: REALSET, delta: real): REALSET =
>     {t:real | EXISTS(i: real): member(i, I) AND t = i + delta}
> 
> 
> Mathematically speaking I would rather write something like:
> 
>   ; + (I: REALSET, delta: real): REALSET =
>     {i + delta | member(i, I)}
> 
> (By the way, are the two specifications equivalent?)
> 
> I am wondering if it is possible to specify the + operation in a way
> which would be syntactically (and maybe semantically) closer to the
> mathematical one...
> 
> Thank you for your help...
> -- 
> 
>     - François

==============================++====================
Dr. John Hoffman              ||                    
Secure Computing Corporation  || What do you want to
2675 Long Lake Road           || read for, when you 
Roseville, MN  55124          || can watch TV?      
hoffman@securecomputing.com   ||                    
Fax  :(612)628-2701           ||  - Matilda's Father
Phone:(612)628-2808           ||                    
==============================++====================