Email Gateway (Aug 18 2022 at 15:45): Email Gateway (Aug 18 2022 at 15:45):From: Tambet <qtvali@gmail.com>
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
Last updated: Nov 21 2024 at 12:39 UTC