4
$\begingroup$

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.

$\endgroup$
8
  • 2
    $\begingroup$ 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. $\endgroup$ Commented May 20, 2022 at 22:02
  • 5
    $\begingroup$ 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. $\endgroup$
    – xavierm02
    Commented May 21, 2022 at 8:29
  • 1
    $\begingroup$ You're looking for zippers $\endgroup$ Commented May 21, 2022 at 13:54
  • 1
    $\begingroup$ @lemontree It's really quite common, especially in older litterature, to refer to a subterm by a finite sequence of integers. $\endgroup$
    – cody
    Commented May 21, 2022 at 16:44
  • 1
    $\begingroup$ @cody Where the finite sequence of integer encodes the path somehow? $\endgroup$
    – azani
    Commented May 21, 2022 at 16:49

1 Answer 1

-1
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ In what way is this standard, and how is one supposed to efficiently decode the number to a position? $\endgroup$ Commented Jul 18, 2023 at 7:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.