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

Data structure of real valued functions (& PVS being too clever?)




1. By the way, you might not realise that you are exploiting a 
feature of PVS whereby - in your case - it automatically lifting
arithmetic operations on reals to pointwise operations on real-valued
functions.  E.g. take your definition of eval which I've introduced
some variety too.

  eval(f:function_datatype) : recursive [T -> real] =
	cases f of
		const(x) : lambda (y : T) : x,
		id : lambda (y : T) : y,
		add(g1,g2) : lambda (y : T) : eval(g1)(y) + eval(g2)(y),
		mul(g1,g2) : lambda (y : T) : (eval(g1) * eval(g2))(y),
		sub(g1,g2) : eval(g1) - eval(g2)

If you do prettyprint-pvs-file and look again, you'll see actually
what PVS is interpreting the definition as:

 eval(f: function_datatype): RECURSIVE [T -> real] =
    CASES f
      OF const(x): LAMBDA (y: T): x,
         id: LAMBDA (y: T): y,
         add(g1, g2): LAMBDA (y: T): eval(g1)(y) + eval(g2)(y),
         mul(g1, g2):
           LAMBDA (y: T): (LAMBDA (x: T): eval(g1)(x) * eval(g2)(x))(y),
         sub(g1, g2): LAMBDA (x: T): eval(g1)(x) - eval(g2)(x)
      ENDCASES
     MEASURE size(f)




Like the K_conversions complained about back in May 2000 on pvshelp, it
would be useful to be able to turn these off.

2. 

A few comments.  I'm not sure if these will answer your question, but
hopefully they are relevant.

* Your `function_datatype' has little to do with the type T, so it shouldn't
  be parameterised by this type.

>   function_datatype[ T : TYPE FROM real ] : DATATYPE 
>    BEGIN
>   	const(x:real): const?
>  	id: id? 
> 	add(g1:function_datatype, g2:function_datatype): add?
> 	mul(g1:function_datatype, g2:function_datatype): mul?
> 	sub(g1:function_datatype, g2:function_datatype): sub?
>    END function_datatype
> 

* If you extend function_datatype to include division, your eval function
  cannot have typing:

>  eval(f:function_datatype) : [T -> real] 

since on some arguments in T it will be undefined (when trying dividing by 0).
You have two main alternatives:

- lift the real type adding a bottom or undefined element. 
  e.g. for x:real, elements of lift[real] might be def(x) or undef. and
  we might have x = val(def(x))

  This gives the typing:

    eval(f:function_datatype) : [T -> lift[real]]

  You then must lift the arithmetic functions too so they return undef if
  either arg is undef.

 The eval function body might then look like:

  cases f of
	const(x) : lambda (y : T) : def(x),
	id : lambda (y : T) : def(y),
	add(g1,g2) : lambda (y : T) : l_add(eval(g1)(y), eval(g2)(y)),
	mul(g1,g2) : lambda (y : T) : l_mul(eval(g1)(y), eval(g2)(y)),
	sub(g1,g2) : lambda (y : T) : l_sub(eval(g1)(y), eval(g2)(y)),
	div(g1,g2) : lambda (y : T) : l_div(eval(g1)(y), eval(g2)(y)),
  endcases
  MEASURE size(f)

  where e.g:

  l_add(a,b) : lift[real] = 
    if def?(a) and def?(b) 
      then def(val(a) + val(b)) 
      else undef
    endif

  l_div(a,b) : lift[real] = 
    if def?(a) and def?(b) and val(b) != 0 
      then def(val(a) / val(b)) 
      else undef
    endif
  
   
- Define f with domain a subtype of T on which eval is defined.

  Using the definition of eval above:

    domain(f:function_datatype)(x:T) : bool = def?(eval(f)(x))

    eval2(f:function_datatype)(x : (domain(f))) : real = val(eval(f)(x))




* You give the differentiation function diff the typing

    diff(f:function_datatype) : recursive [T -> real] 

  Wouldn't it be cleaner to define it as

    diff(f:function_datatype) : function_datatype

  and compose with eval to get the diff you originally defined?