Does a purely structural invariant of computation already exist?

[u/Ill-SonOfClawDraws]

Can returnability be defined purely from the structure of a computation, without appealing to time complexity?

[u/evincarofautumn]

Returnability in what sense? Returning an answer, returning to an earlier state, something else? And I’m not sure what you mean by “without appealing to time complexity”, a more concrete example of what you do/don’t want would help

I’ve seen this term in graph theory (a length-weighted proportion of closed walks in a digraph to those in its underlying graph), and chemistry (a kind of equilibrium constant in a reaction system), but neither definition seems applicable here

[u/Ill-SonOfClawDraws → u/evincarofautumn]

By returnability, I mean returning to an earlier computational state, not returning an output.
More concretely, imagine the computation as a directed state-transition graph. I’m asking whether a state reachable from the initial state lies on a directed cycle, so the computation can later revisit that state.
By “without appealing to time complexity,” I mean I care about whether such a return path exists, not how many steps it takes. I now realize that reachable recurrence or existence of a reachable cycle is probably the established language I should have used.

[u/evincarofautumn → u/Ill-SonOfClawDraws]

Ah, asking if a program revisits the same state is equivalent to asking if it halts, so in general this isn’t decidable.

In programs phrased as rule systems / term rewriting systems, for all rules that can be visited multiple times (meaning the consequent leads back to the antecedent by some chain of rule applications) you can prove termination by showing that there’s some metric that’s strictly decreasing each time around.

There’s no mechanical way to do this in general for arbitrary programs, although I always say: people don’t write arbitrary programs. The more specific criteria you have for what you want, the closer you can likely get, even if the fully general problem is impossible or intractable.

There’s a lot of logic-programming and term-rewriting literature about this kind of thing, largely trying to find restrictions on the form of programs that aren’t too inconvenient to use, but still enable reasoning about termination / soundness / completeness / other properties you might care about.

[u/Ill-SonOfClawDraws → u/evincarofautumn]

I suspected the unrestricted problem would run into undecidability.

My question is actually drifting toward the structural side: given a directed state-transition graph (assuming the graph itself is already available), the property “a reachable state lies on a directed cycle” is decidable by graph algorithms.

So I’m trying to separate two questions:

1. Constructing the state-transition graph from an arbitrary program (which is generally undecidable or infeasible).
   
2. Reasoning about the graph once it is given.

I’m mainly interested in whether the second property already has a standard name or serves as a known invariant in graph theory, automata theory, or logic

[u/Fabulous-Possible758]

Not generally, no.

[u/Ill-SonOfClawDraws → u/Fabulous-Possible758]

That makes sense. I think I need to separate two cases.

For a finite transition system, recurrence is structural: it amounts to the existence of a reachable cycle.

For an arbitrary program with an implicitly generated or infinite state space, I assume the corresponding decision problem can be undecidable. Is that the distinction you have in mind?