What do we call this quantifier ("binder")?

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.

Answer 1

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.