You are describing the regular tree grammars. Here is the basic idea.

It is useful to think if syntactic expressions as abstract syntax trees. 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):

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.

You are describing the regular tree grammars. Here is the basic idea.

It is useful to think of syntactic expressions as abstract syntax trees. 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):

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.

You are looking for regular tree grammars. Here is the basic idea.

It is useful to think if syntactic expressions as abstract syntax trees. 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):

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)))). $$

You are describing the regular tree grammars. Here is the basic idea.

It is useful to think if syntactic expressions as abstract syntax trees. 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):

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.