Does this criteria prove that Y calls X in infinite recursion?

Question

The purpose of this question is to determine the minimum correct halt status criteria required to detect infinite recursion, when we assume that the functions involved are pure functions (thus computable functions).

#include <stdint.h>
typedef void(*ptr)(); 

void X(ptr P, ptr I)  
{
  P(I); 
}

void Y(ptr P)  
{
  X(P, P);
}

int main()
{
  X(Y, Y);
}

Does that fact that Y calls its caller with the same parameters as its caller prove that Y is calling X in infinite recursion?

When we assume that Y is a pure function
If there were any conditional branch instructions in Y prior to its call to X it seems to be proved that they didn't make any difference.

In computer programming, a pure function is a function that has the following properties:

(1) the function return values are identical for identical arguments (no variation with local static variables, non-local variables, mutable reference arguments or input streams), and

(2) the function has no side effects (no mutation of local static variables, non-local variables, mutable reference arguments or input/output streams). https://en.wikipedia.org/wiki/Pure_function

Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithms, in the sense that a function is computable if there exists an algorithm that can do the job of the function, i.e. given an input of the function domain it can return the corresponding output. https://en.wikipedia.org/wiki/Computable_function#

Answer 1

Since main doesn't use the return value (and neither do the others) is it valid for the problem to replace the return types of X and Y with void (and remove the return statements)? This would be the first step in a proof (which I believe is possible). – Craig Estey

Yes that would be valid. – polcott

Caveat: I've never done a formal proof before, but I'll make an attempt using code equivalent substitutions that I understand.

---

Summary of steps:

1. original code
2. convert return types to void and remove return statements
3. because all calls to X use the same value for each argument, convert X to use a single argument
4. inline X into Y
5. replace all Y with X because they are the same
6. remove Y
7. since X is called (only in main) with argument X, replace the argument to X in X with X (i.e. P --> X)
8. since X no longer depends on its argument, remove the argument

---

// step1 -- original code

#include <stdint.h>
typedef int (*ptr) ();

int
X(ptr P, ptr I)
{
    P(I);
    return 0;
}

int
Y(ptr P)
{
    X(P, P);
    return 1;
}

int
main()
{
    X(Y, Y);
}

---

// step2 -- convert return types to void and remove return statements

#include <stdint.h>
typedef void (*ptr) ();

void
X(ptr P, ptr I)
{
    P(I);
}

void
Y(ptr P)
{
    X(P, P);
}

int
main()
{
    X(Y, Y);
}

---

// step3 -- because all calls to X use the same value for each argument,
// convert X to use a single argument

#include <stdint.h>
typedef void (*ptr) ();

void
X(ptr P)
{
    P(P);
}

void
Y(ptr P)
{
    X(P);
}

int
main()
{
    X(Y);
}

---

// step4 -- inline X into Y

#include <stdint.h>
typedef void (*ptr) ();

void
X(ptr P)
{
    P(P);
}

void
Y(ptr P)
{
    P(P);
}

int
main()
{
    X(Y);
}

---

// step5 -- replace all Y with X because they are the same

#include <stdint.h>
typedef void (*ptr) ();

void
X(ptr P)
{
    P(P);
}

void
Y(ptr P)
{
    P(P);
}

int
main()
{
    X(X);
}

---

// step6 -- remove Y

#include <stdint.h>
typedef void (*ptr) ();

void
X(ptr P)
{
    P(P);
}

int
main()
{
    X(X);
}

---

// step7 -- since X is called (only in main) with argument X, replace the
// argument to X in X with X (i.e. P --> X)

#include <stdint.h>
typedef void (*ptr) ();

void
X(ptr P)
{
    X(X);
}

int
main()
{
    X(X);
}

---

// step8 -- since X no longer depends on its argument, remove the argument

#include <stdint.h>
typedef void (*ptr) ();

void
X(void)
{
    X();
}

int
main()
{
    X();
}

---

In the final step, main calls X. And, X just calls itself [infinitely].

---

UPDATE:

The original X and Y are reduced to X calling itself, thus proving that Y calls X in infinite recursion. What I really need to know is whether or not it can be correctly determined that Y calls X in infinite recursion on the basis that Y is calling its caller with the same parameters as it caller. – polcott

I'm not totally sure I understand what you're requesting. But, I think it's implied by [or a byproduct of] the proof above.

Perhaps, if we redo step (5) as:

// alt5 -- replace X(Y) in main with Y(X)

#include <stdint.h>
typedef void (*ptr) ();

void
X(ptr P)
{
    P(P);
}

void
Y(ptr P)
{
    P(P);
}

int
main()
{
    Y(X);
}

Now, we can try:

// alt6 -- replace [undo] P(P) in Y with X(P)

#include <stdint.h>
typedef void (*ptr) ();

void
X(ptr P)
{
    P(P);
}

void
Y(ptr P)
{
    X(P);
}

int
main()
{
    Y(X);
}

We end up with a calling sequence:

1. main -> Y(X)
2. Y(X) -> X(X)
3. X(X) -> X(X)

I don't know, but it may be more clear if we branched off after step (3) and changed main from X(Y) to Y(X)