[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 
  	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
  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)
  MEASURE size(f)

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)
  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.

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