drocta comments on Research agenda: Formalizing abstractions of computations

[drocta]

Whoops, yes, that should have said $f\left(a\right){\to }_{B}f\left(a^{\prime }\right)$ , thanks for the catch! I’ll edit to make that fix.

Also, yes, what things between $a$ and $a^{\prime }$ should be sent to, is a difficulty..
A thought I had which, on inspection doesn’t work, is that (things between $a$ and $a^{\prime }$) could be sent to $f\left(a^{\prime }\right)$ , but that doesn’t work, because $a^{\prime }$ might be terminal, but (thing between $a$ and $a^{\prime }$) 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\left(a^{\prime }\right)$ (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^{\prime },{\to }_{B^{\prime }})$ defined as, $B^{\prime }:=\{b,pre(b)|b\in B\}$ and $\left(x{\to }_{B^{\prime }}y\right)\text{iff}\left(\right((x,y\in B)\wedge \left(x{\to }_B\right))\vee ((y\in B)\wedge (x=pre(y\left)\right)\left)\right)$
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\to B$ is partial and satisfies that condition.
Then, define $f^{\prime }:A\to B^{\prime }$ to agree with f on the domain of f, and for other $a$, pick an $a^{\prime }$ in the domain of f such that $a{\stackrel{\ast }{\to }}_A{a}^{\prime }$ , and define $f^{\prime }\left(a\right)=pre\left(f\right(a^{\prime }\left)\right)$
In a deterministic case, should pick $a^{\prime }$ 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\in A$, either it is in the domain of f, in which case we have the existence of $a^{\prime }\in A$ such that a${\stackrel{\ast }{\to }}_A{a}^{\prime }$ and where $f^{\prime }\left(a\right)=f\left(a\right){\to }_{B^{\prime }}f\left(a^{\prime }\right)=f^{\prime }\left(a^{\prime }\right)$, or it isn’t, in which case we have that there exists $a^{\prime }\in A$ such that a${\stackrel{\ast }{\to }}_A{a}^{\prime }$ and where $f^{\prime }\left(a\right)=pre\left(f\right(a^{\prime }\left)\right){\to }_{B^{\prime }}{f}^{\prime }\left(a^{\prime }\right)=f\left(a^{\prime }\right)$ , and so f’ satisfies the required condition.
On the other hand, if we have an $f^{\prime }:A\to B^{\prime }$ satisfying the required condition, we can co-restrict it to B, giving a partial function $f:A\to B$ , where, if $a$ isn’t in the domain of f, then, assuming a is non-terminal, we get some $a^{\prime \prime }\in A$ s.t. a${\stackrel{\ast }{\to }}_A{a}^{\prime \prime }$ and where $f^{\prime }\left(a\right){\to }_{B^{\prime }}{f}^{\prime }\left(a^{\prime \prime }\right)$ , 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^{\prime }\left(a\right)$ 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^{\prime }:A\to B^{\prime }$ satisfying appropriate conditions to partial function $f:A\to 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.