Lambda the Ultimate

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

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

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.

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.

There are all your names!

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.

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.

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?

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.

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!