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

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

- Prev by Date:
**problem** - Next by Date:
**Problem with "WITH"** - Prev by thread:
**Problem with "WITH"** - Next by thread:
**problem** - Index(es):