Notion of "quotient" or "inverse" for recognizable tree languages?

Question

Related to my previous question but this time I have a better idea of what I'm actually asking.

I'm looking at the following operation on recognizable tree languages (i.e. regular tree grammars, bottom-up automata etc.):

$f^{-i}(L) = \{ t \mid \exists s_1 \ldots s_n \ldotp f(s_1, \ldots, s_{i-1}, t, s_{i+1} \ldots, s_n) \in L \}$.

That is, if $f$ is a symbol in our ranked alphabet, we take the $i$th component of all trees in $L$ that have $f$ as their root.

This seems reminiscent of the notion of quotient in formal language theory, or of projections in the set-constraint literature. Notably, it's not a homomorphism, since we're only applying it at the root, not over the entire tree.

I'm wondering:

1. Does this operation have a name already? Has it been studied?
2. If so, are recognizable tree languages closed under this operation?

It seems like a simple-enough property, but I'd rather not have to figure out all the theory myself if it's already been studied. I've found some things about projection in the TATA book, but they seem to be more about projecting out the nth tuple of a relation, not about projecting to the $i$th argument of a symbol.

Answer 1

The Myhill-Nerode theorem characterizes regular/recognizable languages as those that have finitely many "quotients", and it works for trees — more precisely, a tree language is regular iff there are finitely many languages of the form $\{t \mid C[t/x] ∈ L\}$ where the "context" $C$ is like a tree over the same ranked alphabet, except that exactly one of its leaves is the free variable $x$.

Your $f^{-1}(L)$ can be written as a union of quotients of a regular tree language, which is therefore a finite union of regular tree languages, so it is regular. I don't know about the name of the operation though.