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

Data structure of real valued functions



I would like to do differentiation (of real -> real functions) by having a
function that calculates (rewrites) to the derivative. I also want to be
able to prove that the function is somehow correct.

So I define a data structure for me functions (here only identity,
constant, addition, subtraction and multiplication):

  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

I then define a size function for this datatype (so that I can use the
size function as the measure in all later induction):

  g1, g2 : VAR function_datatype[T]
  f1, f2 : VAR [T -> real]
  x : VAR real  
  size(f:function_datatype) : recursive nat = 
	cases f of
		const(x) : 0,
		id : 0,
		add(g1,g2) : size(g1) + size(g2) + 1,
		mul(g1,g2) : size(g1) + size(g2) + 1,
		sub(g1,g2) : size(g1) + size(g2) + 1
  	endcases
  MEASURE reduce_nat(0,0,(lambda (i,j:nat) : i+j+1),
	     (lambda (i,j:nat) : i+j+1),(lambda (i,j:nat) : i+j+1))

I then define a conversion from my data structure back into the usual
functions [T -> real]:

  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) + eval(g2))(y),
		mul(g1,g2) : lambda (y : T) : (eval(g1) * eval(g2))(y),
		sub(g1,g2) : lambda (y : T) : (eval(g1) - eval(g2))(y)
	endcases
  MEASURE size(f)
  CONVERSION eval

And finally my differentiation operation:

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

Now I can prove by structural induction that the function diff gives the
correct result compared with my ordinary definition of differentiation.

This all works very well, but of course I loose all the facilities in PVS
to help me prevent problems like division by zero (note that I have left
division out so far due to this problem).

So my question is: at this level, could I "get at" the structure of a
function described by a lambda abstraction? And would that even be useful,
ie would I (one) be able to prove anything about it?


I hope someone can help me here, but as usual, if something is unclear let
me know and I'll try to expand on the explanation.

Thanks,
Hanne
---------------------------------------------------------
Hanne Gottliebsen		    Office P337
Dept. of Computer Science	    Ph: +44 1334 46 3265
University of St Andrews	    hago@dcs.st-and.ac.uk
  - I want a single-skin cotton tent like Mr Weasley's
---------------------------------------------------------