You are describing the [regular tree grammars](https://en.wikipedia.org/wiki/Regular_tree_grammar). Here is the basic idea.

It is useful to think if syntactic expressions as [abstract syntax trees](https://en.wikipedia.org/wiki/Abstract_syntax_tree). In our case we are looking for a tree $\alpha$ which satisfies the equation
$$\alpha = \alpha + 1$$
The tree is infinite, but it is also regular (both intuitively and in a precise formal sense):

[![enter image description here][1]][1]

In general you might want to solve a *system* of such equations, for instance
\begin{align*}
\alpha &= \beta + \gamma \\
\beta &= 1 + \beta \\
\gamma &= (\gamma + \beta)
\end{align*}
gives the infinite epression $\alpha$ indicated by
$$
(1 + (1 + (1 + \cdots))) + ((\cdots + (1 + (1 + (1 + \cdots)))) + (1 + (1 + (1 + \cdots)))).
$$

Regarding the question "What is this binder called?" the answer is **a (least) fixed-point operator**. It is usually written as $\mu$ or $\mathsf{fix}$ and its defining equation is, unsurprisingly,
$$\mu x \,.\, \phi(x) = \phi(\mu x \,.\, \phi(x).$$
Your fixed-point operator works at the level of syntax as it is building an infinite syntactic tree. There are other fixed point operators. For instance, given a monotone map $f : L \to L$ on a complete lattice, $\mu f$ would be the least fixed point of $f$. Such operators are the basis of recursive and inductive definitions in programming languages, and have many other uses as well.

  [1]: https://i.sstatic.net/hOv1m.png