Representing bound variables with a function from uses to binders The problem of representing bound variables in syntax, and in particular that of capture-avoiding substitution, is well-known and has a number of solutions: named variables with alpha-equivalence, de Bruijn indices, locally namelessness, nominal sets, etc.

But there seems to be another fairly obvious approach, which I have nevertheless not seen used anywhere.  Namely, in the basic syntax we have only one "variable" term, written say $\bullet$, and then separately we give a function that maps each variable to a binder in whose scope it lies.  So a $\lambda$-term like

$$ \lambda x. (\lambda y. x y)$$

would be written $\lambda. (\lambda. \bullet\bullet)$, and the function would map the first $\bullet$ to the first $\lambda$ and the second $\bullet$ to the second $\lambda$.  So it's kind of like de Bruijn indices, only instead of having to "count $\lambda$s" as you back out of the term to find the corresponding binder, you just evaluate a function.  (If representing this as a data structure in an implementation, I would think of equipping each variable-term object with a simple pointer/reference to the corresponding binder-term object.)

Obviously this is not sensible for writing syntax on a page for humans to read, but then neither are de Bruijn indices.  It seems to me that it makes perfect sense mathematically, and in particular it makes capture-avoiding substitution very easy: just drop in the term you are substituting and take the union of the binding functions.  It's true that it doesn't have a notion of "free variable", but then (again) neither do de Bruijn indices really; in either case a term containing free variables is represented a term with a list of "context" binders in front.

Am I missing something and there is some reason this representation doesn't work?  Are there problems that make it so much worse than the others that it's not worth considering?  (The only problem I can think of right now is that the set of terms (together with their binding functions) is not inductively defined, but that doesn't seem insurmountable.)  Or are there actually places where it has been used?
Andrej's and Łukasz's answers make good points, but I wanted to add additional comments.

To echo what Damiano said, this way of representing binding using pointers is the one suggested by proof-nets, but the earliest place where I saw it for lambda terms was in an old essay by Knuth:


Donald Knuth (1970). Examples of formal semantics. In Symposium on Semantics of Algorithmic Languages, E. Engeler (ed.), Lecture Notes in Mathematics 188, Springer.


On page 234, he drew the following diagram (which he called an "information structure") representing the term $(\lambda y.\lambda z.yz)x$:



This kind of graphical representation of lambda terms was also studied independently (and more deeply) in two theses in the early 1970s, both by Christopher Wadsworth (1971, Semantics and Pragmatics of the Lambda-Calculus) and by Richard Statman (1974, Structural Complexity of Proofs). Nowadays, such diagrams are often referred to as "λ-graphs" (see for example this paper).

Observe that the term in Knuth's diagram is linear, in the sense that every free or bound variable occurs exactly once -- as others have mentioned, there are non-trivial issues and choices to be made in trying to extend this kind of representation to non-linear terms.

On the other hand, for linear terms I think it's great! Linearity precludes the need for copying, and so you get both $\alpha$-equivalence and substitution "for free". These are the same advantages as HOAS, and I actually agree with Rodolphe Lepigre that there is a connection (if not exactly an equivalence) between the two forms of representation: there is a sense in which these graphical structures may be naturally interpreted as string diagrams, representing endomorphisms of a reflexive object in a compact closed bicategory (I gave a brief explanation of that here).