5
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ Do you need to use a hole punch before using a binder? $\endgroup$ – Asaf Karagila Jun 22 '16 at 18:01
  • $\begingroup$ It's unclear to me why you'd want to give it a name. Why not use standard $\lim$ notation? Discrete dynamical system is another standard name for the kind of thing you're doing. $\endgroup$ – Ryan Budney Jun 22 '16 at 18:02
  • 2
    $\begingroup$ @RyanBudney, well, I suspect it has a name. And I like knowing the names of things that I'm interested in when they have names. Further to that, I'd like to use it in a foundational context in which topology/order theory 'isn't yet available'. That being said, I'd be interested to know whether this can indeed be interpreted as a limit in an appropriately chosen topological space. $\endgroup$ – goblin Jun 22 '16 at 18:06
  • 3
    $\begingroup$ This seems to be an iterator rather than a quantifier. Anyway, while it is fairly unclear to me what want to do with the thing, you probably want to look at corecursion. $\endgroup$ – Emil Jeřábek Jun 22 '16 at 18:09
  • 1
    $\begingroup$ You might be thinking of the idea of a fixed-point combinator from computer science. $\endgroup$ – user94221 Jun 22 '16 at 19:41
15
$\begingroup$

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):

enter image description here

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.

$\endgroup$
  • $\begingroup$ A small addendum: these structures have very close connections with the Anti-Foundation Axiom (en.wikipedia.org/wiki/Aczel%27s_anti-foundation_axiom) which essentially posits that any such system has a solution. $\endgroup$ – Steven Stadnicki Jun 22 '16 at 21:52
  • $\begingroup$ Right, I think the Wikipedia page I linked to mentions these things. $\endgroup$ – Andrej Bauer Jun 22 '16 at 23:32
  • $\begingroup$ Do you know if this have anything to do with domain theory? $\endgroup$ – goblin Jun 24 '16 at 16:07
  • $\begingroup$ Well, not really, unless you have something particular in mind. $\endgroup$ – Andrej Bauer Jun 24 '16 at 22:06
  • $\begingroup$ Just that we should be able to define $\mu x.(x+1)$ as the join of a chain of expression in an appropriate poset; I thought maybe domain theory was kind of about this. (I don't have a CS background, as you can probably tell.) $\endgroup$ – goblin Jun 25 '16 at 8:54

Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.