<p>I don't know if this is standard, but we can slightly modify the definition of subterm.</p>
<p>The definition for the set <span class="math-container">$S(T)$</span> of the subterms of a <span class="math-container">$\lambda$</span>-term <span class="math-container">$T$</span> is</p>
<ul>
<li>if <span class="math-container">$T=x$</span>, where <span class="math-container">$x$</span> is a variable, then <span class="math-container">$S(x)=\{x\}$</span></li>
<li>if <span class="math-container">$T=MN$</span>, where <span class="math-container">$M$</span> and <span class="math-container">$N$</span> are <span class="math-container">$\lambda$</span>-terms, then <span class="math-container">$S(MN)=\{MN\}\cup S(M)\cup S(N)$</span></li>
<li>if <span class="math-container">$T=\lambda x.T$</span>, where <span class="math-container">$x$</span> is a variable and <span class="math-container">$M$</span> is a <span class="math-container">$\lambda$</span>-term, then <span class="math-container">$S(\lambda x.T)=\{\lambda x.T\}\cup S(M)$</span></li>
</ul>
<p>By means of this definition we obtain</p>
<p><span class="math-container">$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\}$</span></p>
<p>Now, if in the definition we consider all the unions as <em>disjoint</em>, we obtain</p>
<p><span class="math-container">$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)\}$</span></p>
<p>and all the subterms are distinguishable.</p>

CC BY-SA 4.0
2023-07-18T07:03:29.327Z
In what way is this standard, and how is one supposed to efficiently decode the number to a position?
Andrej Bauer
CC BY-SA 4.0
2023-07-17T21:13:00.653Z
2023-07-17T21:13:00.653Z
Boso
<p>Let's say I have a lambda expression</p>
<p><span class="math-container">$$ (\lambda x . (\lambda w.ww)x) y $$</span></p>
<p>There are a bunch of subterms:</p>
<ul>
<li><span class="math-container">$(\lambda x . (\lambda w.ww)x) y$</span></li>
<li><span class="math-container">$\lambda x . (\lambda w.ww)x$</span></li>
<li><span class="math-container">$(\lambda w.ww)x$</span></li>
<li><span class="math-container">$\lambda w . ww$</span></li>
<li><span class="math-container">$ww$</span></li>
<li><span class="math-container">$w$</span> (the first one)</li>
<li><span class="math-container">$w$</span> (the second one)</li>
<li><span class="math-container">$x$</span></li>
<li><span class="math-container">$y$</span></li>
</ul>
<p>Is there a standard way to identify a particular subterm? (Let's say I want to be able to write down &quot;do a beta-reduction on this one particular subterm&quot;) 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.</p>

CC BY-SA 4.0
2022-05-20T22:02:30.483Z
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.
Natalie Clarius
CC BY-SA 4.0
2022-05-20T22:18:31.077Z
Yes. I think that makes sense as a solution. But I'm wondering if there is a standard approach that people already use. For instance, I spent a bunch of time thinking of indexing schemes for bound variables only to learn that DeBrujin indices were already invented and don't have any of the problems of my weird schemes. I'd like to avoid repeating that if possible.
azani
CC BY-SA 4.0
2022-05-21T08:29:48.547Z
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.
xavierm02
CC BY-SA 4.0
2022-05-21T13:54:35.620Z
You're looking for [zippers](https://www.cambridge.org/core/journals/journal-of-functional-programming/article/zipper/0C058890B8A9B588F26E6D68CF0CE204)
Andrej Bauer
CC BY-SA 4.0
2022-05-21T16:44:06.377Z
@lemontree It's really quite common, especially in older litterature, to refer to a subterm by a finite sequence of integers.
cody
CC BY-SA 4.0
2022-05-21T16:49:50.707Z
@cody Where the finite sequence of integer encodes the path somehow?
azani
CC BY-SA 4.0
2022-05-22T15:56:44.360Z
If you ignore alpha-equivalence, a lambda-term is a tree and you can use any of the many ways of pointing to a node in a tree. (Anecdote: when I wrote my first ever paper, I worried a great
deal about this kind of thing and I did in fact formalise a scheme of explicit encodings of a path to a node, to be super rigorous. My supervisor and coauthor removed all that with the 
words: *"don't put trivial stuff in a paper, the readers can be trusted to know how to fill in the missing details"*)

If you take lambda-terms up alpha-equivalence, things become more complex.
Martin Berger
CC BY-SA 4.0
2022-05-22T18:04:31.663Z
@azani yes, if $t\ u$ is a term and $s$ is a subterm of $u$ then $1.s$ is the corresponding subterm of $t\ u$ (and similarly for $0.s'$ for a subterm of $t$).
cody
<lambda-calculus>
Is there a standard way to "point" at subterms in a lambda expression?
azani
# Is there a standard way to "point" at subterms in a lambda expression?

(Asked by: username_0 on 2022-05-20)

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.

**Tags:** lambda-calculus
> **Comments:**
> **username_1**: 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.  
> **username_0**: Yes. I think that makes sense as a solution. But I'm wondering if there is a standard approach that people already use. For instance, I spent a bunch of time thinking of indexing schemes for bound variables only to learn that DeBrujin indices were already invented and don't have any of the problems of my weird schemes. I'd like to avoid repeating that if possible.  
> **username_2**: 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.  
> **username_3**: You're looking for [zippers](https://www.cambridge.org/core/journals/journal-of-functional-programming/article/zipper/0C058890B8A9B588F26E6D68CF0CE204)  
> **username_4**: @lemontree It's really quite common, especially in older litterature, to refer to a subterm by a finite sequence of integers.  
> **username_0**: @cody Where the finite sequence of integer encodes the path somehow?  
> **username_5**: If you ignore alpha-equivalence, a lambda-term is a tree and you can use any of the many ways of pointing to a node in a tree. (Anecdote: when I wrote my first ever paper, I worried a great deal about this kind of thing and I did in fact formalise a scheme of explicit encodings of a path to a node, to be super rigorous. My supervisor and coauthor removed all that with the  words: *"don't put trivial stuff in a paper, the readers can be trusted to know how to fill in the missing details"*)  If you take lambda-terms up alpha-equivalence, things become more complex.  
> **username_4**: @azani yes, if $t\ u$ is a term and $s$ is a subterm of $u$ then $1.s$ is the corresponding subterm of $t\ u$ (and similarly for $0.s'$ for a subterm of $t$).  

---

## 1 answers

### Answer by username_6 on 2023-07-17. Score: -1

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.

> **Comments:**
> **username_3**: In what way is this standard, and how is one supposed to efficiently decode the number to a position?  

---

