A thought on the “but what if multiple steps in the actual-algorithm correspond to a single step in an abstracted form of the algorithm?” thing : This reminds me a bit of, in the topic of “Abstract Rewriting Systems”, the thing that the ∗→ vs → distinction handles. (the asterisk just indicating taking the transitive reflexive closure)
Suppose we have two abstract rewriting systems (A,→A) and (B,→B). (To make it match more closely what you are describing, we can suppose that every node has at most one outgoing arrow, to make it fit with how you have timesteps as functions, rather than being non-deterministic. This probably makes them less interesting as ARSs, but that’s not a problem) Then, we could say that f:A→B is a homomorphism (I guess) if,
for all a∈A such that a has an outgoing arrow, there exists a′∈A such that a∗→Aa′ and f(a)→Bf(a′) .
These should compose appropriately [err, see bit at the end for caveat], and form the morphisms of a category (where the objects are ARSs).
I would think that this should handle any straightforward simulation of one Turing machine be another.
As for whether it can handle complicated disguise-y ones, uh, idk? Well, if it like, actually simulates the other Turing machine, in a way where states of the simulated machine have corresponding states in the simulating machine, which are traversed in order, then I guess yeah. If the universal Turing machine instead does something pathological like, “search for another Turing machine along with a proof that the two have the same output behavior, and then simulate that other one”, then I wouldn’t think it would be captured by this, but also, I don’t think it should be?
This setup should also handle the circuits example fine, and, as a bonus(?), can even handle like, different evaluation orders of the circuit nodes, if you allow multiple outgoing arrows.
And, this setup should, I think, handle anything that the “one step corresponds to one step” version handles?
It seems to me like this set-up, should be able to apply to basically anything of the form “this program implements this rough algorithm (and possibly does other stuff at the same time)”? Though to handle probabilities and such I guess it would have to be amended.
I feel like I’m being overconfident/presumptuous about this, so like, sorry if I’m going off on something that’s clearly not the right type of thing for what you’re looking for?
__________
Checking that it composes:
suppose A, B, C, f:A→B,g:B→C then for any a∈A which has an outgoing arrow and where f(a) has an outgoing arrow, g(f(a))→Cb′ where f(a)∗→Bb′ so either b’ = f(a) or there is some sequence b0=f(a),b1,...,bn=b′ where bi→Bbi+1 , and so therefore, Ah, hm, maybe we need an additional requirement that the maps be surjective? or, hm, as we have the assumption that a has an outward arrow, then we get that there is an a′ s.t.a∗→Aa′ and s.t. f(a)=b0→Bb1=f(a′)
ok, so, I guess the extra assumption that we need isn’t quite “the maps are surjective”, so much as, “the maps f are s.t. if f(a) is a non-terminal state, then f(a) is a non-terminal state”, where “non-terminal state” means one with an outgoing arrow. This seems like a reasonable condition to assume.
for all a∈A such that a has an outgoing arrow, there exists a′∈A such that a∗→Aa′ and f(a)→Bf(b)
Should it be f(a)→Bf(a′) at the end instead? Otherwise not sure what b is.
I think this could be a reasonable definition but haven’t thought about it deeply. One potentially bad thing is that f would have to be able to also map any of the intermediate steps between a an a’ to f(a). I could imagine you can’t do that for some computations and abstractions (of course you could always rewrite the computation and abstraction to make it work, but ideally we’d have a definition that just works).
What I’ve been imagining instead is that the abstraction can specify a function that determines which are the “high-level steps”, i.e. when f should be applied. I think that’s very flexible and should support everything.
But also, in practice the more important question may just be how to optimize over this choice of high-level steps efficiently, even just in the simple setting of circuits.
Whoops, yes, that should have said f(a)→Bf(a′) , thanks for the catch! I’ll edit to make that fix.
Also, yes, what things between a and a′ should be sent to, is a difficulty.. A thought I had which, on inspection doesn’t work, is that (things between a and a′) could be sent to f(a′) , but that doesn’t work, because a′ might be terminal, but (thing between a and a′) isn’t terminal. It seems like the only thing that would always work would be for them to be sent to something that has an arrow (in B) to f(a′) (such as f(a), as you say, but, again as you mention, it might not be viable to determine f(a) from the intermediary state).
I suppose if f were a partial function, and one such that all states not in its domain have a path to a state which is in its domain, then that could resolve that?
I think equivalently to that, if you modified the abstraction to get, (B′,→B′) defined as, B′:={b,pre(b)|b∈B} and (x→B′y) iff (((x,y∈B)∧(x→B))∨((y∈B)∧(x=pre(y)))) so that B’ has a state for each state of B, along with a second copy of it with no in-going arrows and a single arrow going to the normal version, uh, I think that would also handle it ok? But this would involve modifying the abstraction, which isn’t nice. At least the abstraction embeds in the modified version of it though. Though, if this is equivalent to allowing f to be partial, with the condition that anything not in its domain have arrows leading to things that are in its domain, then I guess it might help to justify a definition allowing f to be partial, provided it satisfies that condition.
Are these actually equivalent?
Suppose f:A→B is partial and satisfies that condition. Then, define f′:A→B′ to agree with f on the domain of f, and for other a, pick an a′ in the domain of f such that a∗→Aa′ , and define f′(a)=pre(f(a′)) In a deterministic case, should pick a′ to be the first state in the path starting with a to be in the domain of f. (In the non-deterministic case, this feels like something that doesn’t work very well...) Then, for any non-terminal a∈A, either it is in the domain of f, in which case we have the existence of a′∈A such that a∗→Aa′ and where f′(a)=f(a)→B′f(a′)=f′(a′), or it isn’t, in which case we have that there exists a′∈A such that a∗→Aa′ and where f′(a)=pre(f(a′))→B′f′(a′)=f(a′) , and so f’ satisfies the required condition. On the other hand, if we have an f′:A→B′ satisfying the required condition, we can co-restrict it to B, giving a partial function f:A→B , where, if a isn’t in the domain of f, then, assuming a is non-terminal, we get some a′′∈A s.t. a∗→Aa′′ and where f′(a)→B′f′(a′′) , and, as the only things in B’ which have any arrows going in are elements of B, we get that f’(a″) is in B, and therefore that a″ is in the domain of f. But what if a is terminal? Well, if we require that f′(a) non-terminal implies a non-terminal, then this won’t be an issue because pre(b) is always non-terminal, and so anything terminal is in the domain. Therefore the co-restriction f of f’, does yield a partial function satisfying the proposed condition to require for partial maps.
So, this gives a pair of maps, one sending functions f′:A→B′ satisfying appropriate conditions to partial function f:A→B satisfying other conditions, and one sending the other way around, and where, if the computations are deterministic, these two are inverses of each-other. (if not assuming deterministic, then I guess potentially only a one-sided inverse?)
So, these two things are equivalent.
uh… this seems a bit like an adjunction, but, not quite. hm.
A thought on the “but what if multiple steps in the actual-algorithm correspond to a single step in an abstracted form of the algorithm?” thing :
This reminds me a bit of, in the topic of “Abstract Rewriting Systems”, the thing that the ∗→ vs → distinction handles. (the asterisk just indicating taking the transitive reflexive closure)
Suppose we have two abstract rewriting systems (A,→A) and (B,→B).
(To make it match more closely what you are describing, we can suppose that every node has at most one outgoing arrow, to make it fit with how you have timesteps as functions, rather than being non-deterministic. This probably makes them less interesting as ARSs, but that’s not a problem)
Then, we could say that f:A→B is a homomorphism (I guess) if,
for all a∈A such that a has an outgoing arrow, there exists a′∈A such that a∗→Aa′ and f(a)→Bf(a′) .
These should compose appropriately [err, see bit at the end for caveat], and form the morphisms of a category (where the objects are ARSs).
I would think that this should handle any straightforward simulation of one Turing machine be another.
As for whether it can handle complicated disguise-y ones, uh, idk? Well, if it like, actually simulates the other Turing machine, in a way where states of the simulated machine have corresponding states in the simulating machine, which are traversed in order, then I guess yeah. If the universal Turing machine instead does something pathological like, “search for another Turing machine along with a proof that the two have the same output behavior, and then simulate that other one”, then I wouldn’t think it would be captured by this, but also, I don’t think it should be?
This setup should also handle the circuits example fine, and, as a bonus(?), can even handle like, different evaluation orders of the circuit nodes, if you allow multiple outgoing arrows.
And, this setup should, I think, handle anything that the “one step corresponds to one step” version handles?
It seems to me like this set-up, should be able to apply to basically anything of the form “this program implements this rough algorithm (and possibly does other stuff at the same time)”? Though to handle probabilities and such I guess it would have to be amended.
I feel like I’m being overconfident/presumptuous about this, so like,
sorry if I’m going off on something that’s clearly not the right type of thing for what you’re looking for?
__________
Checking that it composes:
suppose A, B, C, f:A→B,g:B→C
then for any a∈A which has an outgoing arrow and where f(a) has an outgoing arrow, g(f(a))→Cb′ where f(a)∗→Bb′
so either b’ = f(a) or there is some sequence b0=f(a),b1,...,bn=b′ where bi→Bbi+1 , and so therefore,
Ah, hm, maybe we need an additional requirement that the maps be surjective?
or, hm, as we have the assumption that a has an outward arrow,
then we get that there is an a′ s.t.a∗→Aa′ and s.t. f(a)=b0→Bb1=f(a′)
ok, so, I guess the extra assumption that we need isn’t quite “the maps are surjective”, so much as, “the maps f are s.t. if f(a) is a non-terminal state, then f(a) is a non-terminal state”, where “non-terminal state” means one with an outgoing arrow. This seems like a reasonable condition to assume.
Should it be f(a)→Bf(a′) at the end instead? Otherwise not sure what b is.
I think this could be a reasonable definition but haven’t thought about it deeply. One potentially bad thing is that f would have to be able to also map any of the intermediate steps between a an a’ to f(a). I could imagine you can’t do that for some computations and abstractions (of course you could always rewrite the computation and abstraction to make it work, but ideally we’d have a definition that just works).
What I’ve been imagining instead is that the abstraction can specify a function that determines which are the “high-level steps”, i.e. when f should be applied. I think that’s very flexible and should support everything.
But also, in practice the more important question may just be how to optimize over this choice of high-level steps efficiently, even just in the simple setting of circuits.
Whoops, yes, that should have said f(a)→Bf(a′) , thanks for the catch! I’ll edit to make that fix.
Also, yes, what things between a and a′ should be sent to, is a difficulty..
A thought I had which, on inspection doesn’t work, is that (things between a and a′) could be sent to f(a′) , but that doesn’t work, because a′ might be terminal, but (thing between a and a′) isn’t terminal. It seems like the only thing that would always work would be for them to be sent to something that has an arrow (in B) to f(a′) (such as f(a), as you say, but, again as you mention, it might not be viable to determine f(a) from the intermediary state).
I suppose if f were a partial function, and one such that all states not in its domain have a path to a state which is in its domain, then that could resolve that?
I think equivalently to that, if you modified the abstraction to get, (B′,→B′) defined as, B′:={b,pre(b)|b∈B} and (x→B′y) iff (((x,y∈B)∧(x→B))∨((y∈B)∧(x=pre(y))))
so that B’ has a state for each state of B, along with a second copy of it with no in-going arrows and a single arrow going to the normal version,
uh, I think that would also handle it ok? But this would involve modifying the abstraction, which isn’t nice. At least the abstraction embeds in the modified version of it though.
Though, if this is equivalent to allowing f to be partial, with the condition that anything not in its domain have arrows leading to things that are in its domain, then I guess it might help to justify a definition allowing f to be partial, provided it satisfies that condition.
Are these actually equivalent?
Suppose f:A→B is partial and satisfies that condition.
Then, define f′:A→B′ to agree with f on the domain of f, and for other a, pick an a′ in the domain of f such that a∗→Aa′ , and define f′(a)=pre(f(a′))
In a deterministic case, should pick a′ to be the first state in the path starting with a to be in the domain of f. (In the non-deterministic case, this feels like something that doesn’t work very well...)
Then, for any non-terminal a∈A, either it is in the domain of f, in which case we have the existence of a′∈A such that a∗→Aa′ and where f′(a)=f(a)→B′f(a′)=f′(a′), or it isn’t, in which case we have that there exists a′∈A such that a∗→Aa′ and where f′(a)=pre(f(a′))→B′f′(a′)=f(a′) , and so f’ satisfies the required condition.
On the other hand, if we have an f′:A→B′ satisfying the required condition, we can co-restrict it to B, giving a partial function f:A→B , where, if a isn’t in the domain of f, then, assuming a is non-terminal, we get some a′′∈A s.t. a∗→Aa′′ and where f′(a)→B′f′(a′′) , and, as the only things in B’ which have any arrows going in are elements of B, we get that f’(a″) is in B, and therefore that a″ is in the domain of f.
But what if a is terminal? Well, if we require that f′(a) non-terminal implies a non-terminal, then this won’t be an issue because pre(b) is always non-terminal, and so anything terminal is in the domain.
Therefore the co-restriction f of f’, does yield a partial function satisfying the proposed condition to require for partial maps.
So, this gives a pair of maps, one sending functions f′:A→B′ satisfying appropriate conditions to partial function f:A→B satisfying other conditions, and one sending the other way around, and where, if the computations are deterministic, these two are inverses of each-other. (if not assuming deterministic, then I guess potentially only a one-sided inverse?)
So, these two things are equivalent.
uh… this seems a bit like an adjunction, but, not quite. hm.