Signed-off-by: Jim Pryor <profjim@jimpryor.net>
A third way to think is to identify the lambda formula not with classes of alphabetic sequences, but rather with abstract structures that we might draw like this:
<pre><code>
- (λ. λ. z x) y
- ^ ^ | |
- | |__| |
- |_______|
+ (λ. λ. _ _) y
+ ^ ^ | |
+ | |__| |
+ |_______|
</code></pre>
Here there are no bound variables, but there are *bound positions*. We can regard formula like (a) and (b) as just helpfully readable ways to designate these abstract structures.