There's a quantifier ("binder", whatever), call it $\alpha$, defined as follows: $\alpha x.\tau$ is the (usually infinite) expression obtained by applying the substitution $\{x \mapsto \tau\}$ to the expression $x$ an infinite number of times. Its probably a bit unclear what I mean here, so let me give some intuition and a couple of examples.

The idea is to read $\alpha x.(x+1)$ as denoting an infinite syntactic expression corresponding to the equation $x=x+1$. In particular, suppose $x=x+1$. Then we can write: $$x = x+1 = (x+1)+1 = ((x+1)+1)+1) = \cdots$$

We think of $\alpha x.(x+1)$ as the 'limit' of this process. So: $$\alpha x.(x+1) = ((...)+1)+1,$$

Notice there's no $x$ in the 'expression' $((...)+1)+1$; once we've passed to infinity, all our variables disappear. So $x$ is 'bound' in the expression $\alpha x.(x+1).$ Its not free. In some sense, we might say: there's no $x$ in $\alpha x.(x+1).$

More generally, we're meant to think of $\alpha x.\tau$ as the infinite expression corresponding to the assumption $x=\tau$. For instance:

$$\alpha x.(x+x) = ((...)+(...))+((...)+(...))$$

etc.

Question. What do we call this 'quantifier' and where can I learn more about it?

I'm also interested in variants and generalizations, so don't be hesitant to post an answer even if it doesn't quite answer the question.

There's a quantifier ("binder", whatever), call it $\alpha$, defined as follows: $\alpha x.\tau$ is the (usually infinite) expression obtained by applying the substitution $\{x \mapsto \tau\}$ to the expression $x$ an infinite number of times. Its probably a bit unclear what I mean here, so let me give some intuition and a couple of examples.

The idea is to read $\alpha x.(x+1)$ as denoting an infinite syntactic expression corresponding to the equation $x=x+1$. In particular, suppose $x=x+1$. Then we can write: $$x = x+1 = (x+1)+1 = ((x+1)+1)+1) = \cdots$$

We think of $\alpha x.(x+1)$ as the 'limit' of this process. So: $$\alpha x.(x+1) = ((...)+1)+1.$$

Notice there's no $x$ in the 'expression' $((...)+1)+1$; once we've passed to infinity, all our variables disappear. So $x$ is 'bound' in the expression $\alpha x.(x+1).$ Its not free. In some sense, we might say: there's no $x$ in $\alpha x.(x+1).$

More generally, we're meant to think of $\alpha x.\tau$ as the infinite expression corresponding to the assumption $x=\tau$. For instance:

$$\alpha x.(x+x) = ((...)+(...))+((...)+(...))$$

etc.

Question. What do we call this 'quantifier' and where can I learn more about it?

I'm also interested in variants and generalizations, so don't be hesitant to post an answer even if it doesn't quite answer the question.