Reference request: running out of countably many variable names

In nearly every semantics paper I've seen - notably not Plotkin's Call-by-Name, Call-by Value and the Lambda Calculus - the semantics obtains a fresh variable name by simply declaring "x fresh". It's almost a joke, actually. The names come from a countable set, so they're practically inexhaustible, and we know we could either thread a counter (aka gensyms) or examine some term to find the lexically greatest and choose the next one. So we smirk and just write "x fresh".

This week, I decided to write the beta-substitution metafunction for an operational semantics, making sure every operation was explicitly defined. According to Plotkin, I can take a new name from the set of all names that aren't free in both the expression being substituted in, N, and the expression being substituted, M. Then I realized, because of how I defined the language, that either N or M could contain every name as a free variable!

The language contains infinite terms. It's a theoretical device, not intended to be implemented. An example of an expression that uses every name is the set of functions N = {(lambda x1 . x0), (lambda x0 . x1), (lambda x3 . x2), (lambda x2 . x3), ...}. If X = {x0, x1, x2, x3, ...} is the set of variable names, every name in X is free in N.

I might be able to find a tricky way around this or prove that it never happens (under some reasonable conditions). But I've settled on using De Bruijn indexes instead of names.

Here are my questions: Has anybody run out of variable names or heard of running out of variable names before? What did you or the other person do about it?

EDIT: I'm softening the question. Has "x fresh" ever not worked for you, for whatever reason?

EDIT (again): I'm not necessarily looking for new solutions, because I think I have a really good one. I'm looking more for analogies - other experience I can cite when I write about this. I also want to know whether this "x fresh doesn't work" problem is new.

Comment viewing options

Why don't you just start

Edit: That was a little terse, maybe. It sounds like the property you need is just that the set of names be well ordered, so that you can always ask for the "next" unused name. If you start from an uncountable well ordered set, does that satisfy your requirements?

The uncountable set of names can't be a set

I thought of addressing this in the OP, then thought "Oh, that's not bound to come up for a while..." Heh. Nicely done.

Short answer: That would probably work, but be harder than De Bruijn indexes. I'm asking for references or experience primarily so I can relate what I'm going to do to other work when I write about it. Also, I'm not completely settled on De Bruijn indexes yet, especially if there's an easier way.

Elaboration:

I think I can, but it can't be a hereditarily pure set. Generally, the terms in this language that denote set values can construct sets of any cardinality, so there is no set of variable names large enough. It would have to be a proper class. I think the ordinals would do fine. To get a fresh one, I'd just need the successor of the largest one representing a free variable in N and M if there is a largest, or the supremum in N and M if there isn't a largest. No need to even construct the class.

There are other issues, though. My terms are encoded syntactically as sets - that's the easiest way to make them compatible with ZFC. Defining recursive functions that operate on sets is very tricky, unless it's simple structural recursion on some well-founded structure. Beta substitution isn't simple structural recursion on encoded terms: there is a nested recursive call, and an auxiliary call to discover free variables. I think De Bruijn substitution is simple structural recursion, so I shouldn't need to go through all the tedious incantations that I would for subst and find-free-variables.

(At this point, I expect the Coq, Isabelle/ZF, and HOL peeps to ask why I'm defining a reduction semantics for impossibly large programs instead of just using a proof assistant's language. I have answers.

1. I'm defining this language as a target for an exact, uncomputable, denotational semantics. I'll be implementing approximations in Racket. To keep the path "exact semantics -> approximating semantics -> compiler (macros)" as clear as possible, I need a target language similar to Racket. A call-by-value lambda calculus with infinite sets is just the thing.

2. I would rather not be forced into assuming the existence of a large cardinal by using HOL or Coq. I want to stick to ZFC if I can, because almost all the existing domain knowledge explicitly assumes ZFC.

3. I'll probably define the language in Coq eventually, anyway.)

Clarification

Are terms in your language countable (or at least, does each term have cardinality < k for some cardinal k)? If so, then I don't see why the fact that your terms can denote sets of arbitrary cardinality precludes having a set of variable names. For example, if you have only countable terms, then I don't see why you need names outside the set of countable ordinals. More generally, assuming that terms have cardinality < k, where k is a regular cardinal, we should be able to draw our ordinals from k (I'm guessing that you have term constructors that are going to need k to be regular, but that may not be the case).

Tuples?

As your language contains infinite terms how are you actually expressing them syntactically? Your definition of N looks like a version aimed at a human reader. Can't you use names that are tuples of elements from a countable set, so assuming that all of your x_0,x_1... names are derived from a symbol x couldn't you generate names in (x,0), (x,1)... etc where you can then enumerate a successor for x and thus generate fresh names (x',0), (x',1) ... etc?

The "names don't have to be strings of symbols" idea

I hadn't thought of that. I was going to retort that I can almost as easily construct a term that contains all of the finite tuples of names as free variables.

But that doesn't necessarily hold if I allow names to be infinite structures. For example, I could collect all the free names in N and M, and call the set of them a fresh name. If names can be any hereditary set, I'd be fine.

Interesting. It'd be a lot like the idea of using ordinals as names, but with less... order. :) And definitely easier to work with. I think I'll make this my "Plan B". Thanks!

EDIT: You're right: the example is a schema aimed at human readers. Terms in the language are encoded as pure sets (the empty set, or sets containing nothing but sets), so it doesn't matter how readable they are after that. Though there isn't a direct finite representation of the example, it is a definable term.

conway

One quick aside and then a pointer to some neat stuff that might help or inspire you. The quick aside is that you are obviously making some mistake if you think that your countably infinite set of terms is going to exhaust your countably infinite set of variable names. Any two countably infinite sets can be set in 1:1 correspondence -- you just haven't figured out how to conveniently express that correspondence. The earlier suggestion that you use an uncountable set is a red herring, in that regard.

That's the negative, here's the positive:

This is starting to remind me of the "Appendix to Part Zero" of Conway's "On Numbers and Games". It might be interesting to see your formalism. (That and the first parts of Part 0 are recommended strongly.)

You can define your variable names and your lambda terms in a parallel induction. If you look at Conway's definitions of numbers and then games, the "heriditary set" hack is well applied.

Perhaps you can define some operator "make_distinct_name" in such a way that, as you say, make_distinct_name(M,N) where M and N are sets of earlier constructed names yields a name distinct from all members of M and N. Add an axiom that the empty set is itself a name - the only finite name you have to otherwise explicitly assert, perhaps.

You apparently also want an axiom of at least countable infinity added to your inductive definitions. So, {} is a a name, and make_distinct_name(A,B) is a name for all earlier constructed A and B. But you also want an additional induction axiom gives you the countable but non-finite compositions of make_distinct_name.

Now you have two problems, though.

If you define a general class of names along those lines, right away you will find that you can not define an effective equivalence relation. I can generally describe two constructions of infinite names and, if your name class is roughly as general as Conway's games -- you can't compute, generally, whether or not two name-defining constructions are equal. Equivalence between constructible reals isn't decidable for a similar reason.

Maybe you don't care for your purposes, although it seems odd for a semantics to not want effective equivalence between names. Or... maybe you don't need quite that general a name construction and the parallel construction of terms will simplify the construction of names and thereby simplify the equivalence relation for names.

Inside the model or outside of it?

The quick aside is that you are obviously making some mistake if you think that your countably infinite set of terms is going to exhaust your countably infinite set of variable names.

Not enough nuance! We are philosophers, sir!

When I wrote that I might be able to "prove that [running out of names] never happens (under some reasonable conditions)," the "reasonable conditions" I had in mind were "using only encodings of a finite terms, or reductions of them." So I get you.

Thinking about it now, though, I'm not sure the conditions are so reasonable. I encode finite terms as sets, then do reductions on them that ZFC guarantees yield sets. I ensure that they conform to a structure - they're "well-formed" - allowing me to claim that they correspond with terms in a larger language. But that's not the only way to generate infinite terms. I can easily do it outside of the language, in first-order logic with the ZFC axioms.

(In fact, no matter what awesome way I come up with to get names, there's probably a way, outside the language, to construct an infinite term that exhausts them - unless the names form a proper class. Now that's interesting.)

So I have a decision: do I assume that all infinite terms are reductions from encodings of finite ones, or not? For the most generality, I would rather assume they can come from any formal system that is capable of defining them.

(This decision reminds me strongly of the decision that resolves Skolem's paradox: are you reasoning "inside" the countable model, or "outside" of it?)

I've wanted to check out "On Numbers and Games" for a while. I'm going to have to do it, now. People made it sound as nifty as all get-out before, and now you've told me it might be related to my research.

As far as effective equivalence between names: that would be nice, but if I stay inside the model, I can't have it. Of course, I can't actually compute the reduction relation, either, so that's not such a big loss. Still, it's an issue I hadn't thought of, and it might get in the way later. More points in favor of De Bruijn indexes, then.

Hilbert's hotel

As a follow-up to Thomas Lord's comment, to show how little I understand the problem: Obviously you are concerned in this setting with theoretical correctness, rather than efficiency. Could you not, at every (or at least every ‘dangerous’) occasion of variable allocation, simply double the indices of all old variables and then use, say, 1 for your new index? (As the title suggests, I think of this as basically a version of Hilbert's hotel.) It would obviously be both slow and unwieldy, but it would also obviously prevent you from ever running out of terms.

(EDIT: Come to think of it, if you only need 1 (or even finitely many) new names at a time, then it's even easier: you can replace the doubling by mere incrementing.)

Perhaps this runs into the problem that it's not just inefficient but non-halting to find all the variable names in an infinite term; so maybe terms could be wrapped when necessary with an instruction to double all indices found therein?

re: Not enough nuance! We are philosophers, sir!

I don't understand why you aren't simply doing something along these lines (with apologies(?) to Conway):

As we know,

If A and B are lambda terms, then AB is a lambda term of the variety called an application. This is the only way an application may be formed.

If X is a variable and A is a lambda term, then \X.A is a lambda term of the variety called an abstraction. This is the only way an abstraction may be formed.

If V is a variable, then V is also a lambda term of the variety called a "constant". This is the only way that constants may be formed.

The free variables of \X.A, namely FV(\X.A), are the set of free variables of A, with X excluded: FV(\X.A) = FV(A) - X

The free variables of AB, namely FV(AB), are simply the set FV(A) union FV(B).

If V is a variable and thus a constant lambda term, FV(V) is V.

If VS is a set of variables, then New(VS) is a variable distinct from the members of VS, characterized by definition as having the distinction set VS. That is to say that Distinctions(New(VS)) := VS This is the only way that variables may be formed.

Lambda terms may only be applications, abstractions, or constants.

===========================

That gives us all of our lambda terms as far as we wish to take them.

As Conway does with numbers we can ask, how does such a system ever get off the ground?

The empty set, {}. is a (vacuous) set of variables.

Therefore, New({}) is a variable which we might as well call, x0.

Since a variable is a constant lambda expression, New({}) is our first lambda expression. Call that (in the manner of Conway) "lambda expressions created on day 0".

The next day we can create three new lambda expressions, perhaps deserving of names:

(x0)(x0) Self application
\x0.x0 Identity Function
x1 Other

In the customary ways we can define alpha and beta substitution and the interesting equivalence relations.

We can say that after all of the days we can count to ... there comes the day "omega" -- that would be the addition of an axiom of transfinite induction of a certain sort. Now we have infinite lambda terms, our rules for alpha and beta reduction should be adaptable without much fuss.... and fear of running out of variable names isn't on the map. Moreover the whole theory has a pretty trivial ZF model, I think.

Perhaps the confusion about "running out variable names" comes from the syntactic habit of writing variables with integer indexes in expositinoal pieces. Using variable names like x0, x1, x2, .... or more normally a, b, c, ..... creates a kind of superstitious belief that those integer indexes (explicit or implied) add rigor when, well, they are really just a distraction.

Again, I suggest looking at that "Appendix to Part 0" where Conway talks about induction rules.

POPLmark

Binding/names is a non-trivial part of the POPLmark challenge.

One solution that may be of particular interest to you is that of cofinite quantification, as discussed in "Engineering Formal Metatheory", by Aydemir et al..

Locally nameless

Cool, it's the mixed names + De Bruijn representation. I first encountered this in the catchily-named "I am not a number: I am a free variable" by McBride and McKinna. I'm not clear on how cofinite quantification works yet, but it's an alternative to "x fresh," which is precisely what I was asking for.

And the Aydemir paper has a survey of binding representations! You get two Internet cookies. Thanks!

Infinite width or infinite depth ?

Are you terms infinitely large, or even infinitely deep ? If you start from a closed term, then go under some binders (a finite number of times), then try to reason about the subterms in depth, you will only have a finite number of variables in the context, hence a finite number of free variables in the subterms.

Vicious Circles

I've been reading Vicious Circles by Barwise and Moss (thanks to frequent recommendation by Dan Piponi's blog). They encounter and address just this issue. To do the sorts of things they want with sets, they need a vastly infinite supply of fresh variables from outside of the universe of sets. They do so by extending set theory with urelements (http://en.wikipedia.org/wiki/Urelement) and an axiom of plenitude that essentially just promises that urelements are inexhaustible.

This struck me as sort of kludgy, so I went and looked for work since then. Sure enough, since the book, Moss produced a new treatment of the core material that deals with pure set theory with no extensions. I'm not going to claim to fully follow what's going on. But the core idea is, I think, that rather than studying set theory in set theory, he studies set theory in category theory, and deals with corecursion via coalgebras. See "Parametric Corecursion" http://www.indiana.edu/~iulg/moss/aarticles.htm#REC (2001).

And while I'm only some of the way through Vicious Circles, I can't recommend it enough -- the amount of different material it draws together from different fields, both in and out of computer science on (co)recursion, self-referentiality, etc. is very impressive, and the exposition is as clear as I've seen.

Expressions vs. Terms

On another note, I'm not sure if your problem is as real as you imagine at all, or at least in the way you imagine. The example doesn't really make sense to me.

You give an expression: N = {(lambda x1 . x0), (lambda x0 . x1), (lambda x3 . x2), (lambda x2 . x3), ...}

But that's not an expression, that's a description of an expression. The actual expression is infinite and can't be written. Unless you have a metalanguage for some form of code generation, that seems to be a nonissue to me. Meanwhile, what it is certainly not is a term, which by definition does not contain free variables. If your language is an algebra on terms, your concern should be whether your terms can produce such an expression, which I would suspect they can't. If it can, I'd be very curious to see how!

By rough analogy, I think that you might as well ask why Haskell can't run out of variable names due to the expression [\x -> a, \x -> b, \x -> ab...].

Nominal sets

Another theory you may want to consider is the theory of nominal sets, by Murdoch J. Gabbay and Andy Pitts. In this theory, the set M in your question is definable and has empty support (i.e., no free names), since it is invariant under all name transpositions.

To answer your question, you may want to look at "How to Prove False using the Variable Convention" by Christian Urban.