# Is there a standard way to "point" at subterms in a lambda expression?

Let's say I have a lambda expression

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

There are a bunch of subterms:

• $$(\lambda x . (\lambda w.ww)x) y$$
• $$\lambda x . (\lambda w.ww)x$$
• $$(\lambda w.ww)x$$
• $$\lambda w . ww$$
• $$ww$$
• $$w$$ (the first one)
• $$w$$ (the second one)
• $$x$$
• $$y$$

Is there a standard way to identify a particular subterm? (Let's say I want to be able to write down "do a beta-reduction on this one particular subterm") Naively, it seems like you could just write down the specific term you're referring to, but then you still have the issue of some subterms being identical. Another option would be to define an iteration order (say, DFS left-first) and then index into that. I'm wondering if there is a technique or standard way to do this.

• You could identify them in terms of a (number or whatever) encoded path on the syntax tree. But it's not "standard" in the sense that I've ever seen it being done. May 20, 2022 at 22:02
• To represent a term and one of its subterm, it is common to use a context (i.e. term with a hole) to represent what remains of the term once the subterm is removed. May 21, 2022 at 8:29
• You're looking for zippers May 21, 2022 at 13:54
• @lemontree It's really quite common, especially in older litterature, to refer to a subterm by a finite sequence of integers.
– cody
May 21, 2022 at 16:44
• @cody Where the finite sequence of integer encodes the path somehow? May 21, 2022 at 16:49

I don't know if this is standard, but we can slightly modify the definition of subterm.

The definition for the set $$S(T)$$ of the subterms of a $$\lambda$$-term $$T$$ is

• if $$T=x$$, where $$x$$ is a variable, then $$S(x)=\{x\}$$
• if $$T=MN$$, where $$M$$ and $$N$$ are $$\lambda$$-terms, then $$S(MN)=\{MN\}\cup S(M)\cup S(N)$$
• if $$T=\lambda x.T$$, where $$x$$ is a variable and $$M$$ is a $$\lambda$$-term, then $$S(\lambda x.T)=\{\lambda x.T\}\cup S(M)$$

By means of this definition we obtain

$$S((\lambda x.(\lambda w.ww)x)y)=\{(\lambda x.(\lambda w.ww)x)y\}\cup (\{\lambda x.(\lambda w.ww)x\}\cup (\{\lambda x.(\lambda w.ww)\}\cup (\{\lambda w.ww\}\cup (\{ww\}\cup\{w\}\cup\{w\})))\cup\{x\})\cup\{y\}$$

Now, if in the definition we consider all the unions as disjoint, we obtain

$$S((\lambda x.(\lambda w.ww)x)y)=\{((\lambda x.(\lambda w.ww)x)y,1), (\lambda x.(\lambda w.ww)x,2), (\lambda x.(\lambda w.ww),3), (\lambda w.ww,4), (ww,5), (w,6), (w,7), (x,8), (y,9)\}$$

and all the subterms are distinguishable.

• In what way is this standard, and how is one supposed to efficiently decode the number to a position? Jul 18 at 7:03