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.

Improve this question
$\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$
    – Natalie Clarius
    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
    May 21, 2022 at 8:29
  • 1
    $\begingroup$ You're looking for zippers $\endgroup$
    – Andrej Bauer
    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
    May 21, 2022 at 16:44
  • 1
    $\begingroup$ @cody Where the finite sequence of integer encodes the path somehow? $\endgroup$
    – azani
    May 21, 2022 at 16:49

1 Answer 1

Reset to default
-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.

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

Your Answer

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

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