*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] One more question about recursive functions*From*: Tambet <qtvali at gmail.com>*Date*: Mon, 26 Jul 2010 01:53:01 +0300

This is a conceptual question - I would need an answer soon, but it's quite much to optimize my learning paths. Say that I have a set of mutually recursive functions [A_0..A_n]. Then I make up a set of properties [P_0..P_m], which apply to inputs and outputs of those functions. Say that those n and m are natural numbers (so that the sequences are finite). For example, this: - A_0 might return a result or call A_1 with some value and return it's result in slightly modified form. - A_1 might return a result or call A_2 in same way. - A_2 might call A_0 or A_1 depending on something. This makes up somewhat complicated call path. I want to prove that in case a call to A_2 returns, it's result will have property P_x iff it's input has property P_y. Assume that I can prove that: - In case parameter passed to A_2 has property P_y, it will - call A_0 with parameter having property P_0 or - call A_0 with parameter having property P_1 or - call A_1 with parameter having property P_0 - In case parameter of call to A_0 has property P_0 - It will instantly return result, which has property P_1 - and so on In case I am able to prove those things about concrete calls, I have made up a finite call graph, which is basically having very small mathematical complexity (in terms of O(f(n)), where n is the number of facts I have given it and f(n) is the number of operations). It would be also nice knowledge about how to make functions over those properties so that I could show that return values of them are decreasing to show that function will always return, but this raises the complexity so much that I better won't ask it right now - I will ask it later, when I have learnt to handle the more basic case :) Second case is about returning in this simple graph. Could I show that for some property of value, another function will be called with such value that third function will be called and third will call second one with such property that it forms a cycle? Tambet

- Previous by Date: [isabelle] an inductive datatype and n inductively defined set
- Next by Date: Re: [isabelle] One more case about induction
- Previous by Thread: Re: [isabelle] One more case about induction
- Next by Thread: [isabelle] Mutually recursive coinductive predicates
- Cl-isabelle-users July 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list