# Data structure of real valued functions

• To: pvs-help@csl.sri.com
• Subject: Data structure of real valued functions
• From: Hanne Gottliebsen <hago@dcs.st-and.ac.uk>
• Date: Mon, 6 Nov 2000 16:51:08 +0000 (GMT)
• Delivery-Date: Mon Nov 6 08:51:18 2000

```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,

function_datatype[ T : TYPE FROM real ] : DATATYPE
BEGIN
const(x:real): const?
id: id?
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
---------------------------------------------------------

```