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

*To*: pvs-help@csl.sri.com*Subject*: Recursive declarations*From*: David Delahaye <delahaye@jurancon.inria.fr>*Date*: Thu, 22 Jan 1998 18:13:05 +0100 (MET)

Good evening, I am a new user of PVS and I have some questions about the recursive declarations. First of all, I wonder how the termination TCC is generated opposite the measure term. For example, at the section 3.7 of your tutorial with the very simple case of the factorial function, could you explicit the process of generation? At last, in the same section, you tell that mutual recursion is not directly possible but we can produce the same effect by means I don't understand very well in fact. Could you put into practice the two means you propose with the following example that I give in ML: let rec add1 n= if n=0 then 1 else 1+add2(n-1) and add2 n= if n=0 then 2 else 2+add1(n-1);; Many thanks for your answer. Best regards. David Delahaye. =============================================================================== David Delahaye <Email>: David.Delahaye@inria.fr <Laboratory>: The Coq Project <Domain>: Proofs <Adress>: INRIA-Rocquencourt Domaine de Voluceau BP105 78153 Le Chesnay Cedex FRANCE <Tel>: (33)-(0)1 39 63 57 53 <Fax>: (33)-(0)1 39 63 56 84 <Url>: http://pauillac.inria.fr/~delahaye =============================================================================== [If you have time to waste, you can have a look on my proof that all the real number are positive. Given x in R: x^2>=0 (well-known result) (x^2)^(1/2)>=(0)^(1/2) (use of power on each member) x^(2*1/2)>=0 (use of the propertie: (x^n)^m=x^(n*m) x^1>=0 (very easy simplification) x>=0 (great!)]

- Prev by Date:
**Re: Recursive declarations** - Next by Date:
**EXPAND and IF-THEN?** - Prev by thread:
**Re: Recursive declarations** - Next by thread:
**A problem about rule "inst"** - Index(es):