What is the subterms of $M\equiv (\lambda x\cdot yx)(\lambda z \cdot x(yx))$?

Question

Using this

Definition (Subterms): The subterms of a term M are defined by induction on $|M|$ as follows:

1. an atom is a subterm of itself;
2. if $M\equiv \lambda x \cdot P$, its subterms are $M$ and all subterms of $P$;
3. if $M \equiv P_1 P_2$, its subterms are all the subterms of $P_1$, all those of $P_2$, and $M$ itself.

Example: If $M\equiv (\lambda x\cdot yx)(\lambda z \cdot x(yx))$ its subterms are $x$, $y$, $yx$, $\lambda x \cdot yx$, $x(yx)$, $\lambda z \cdot x(yx)$ and M itself. (But not $z$.)

So, my question is: why $z$ is not a subterm in the given example?

Answer 1

It Depends on definition of set of Subterms, If you think $z$ should be a Subterm, you may change the definition as you like:

1. $\dots$;
2. $M \equiv \lambda x \cdot P$, its Subterms are $M$, $x$ and all Subterms of $P$;
3. $\dots$.

This may make sense to you as you want $z$ to be a subset of the term you mentioned, but with the definition you provided, it's simple to just go step by step and compute the set of Subterms.

$\text{sub}((\lambda x\cdot yx)(\lambda z\cdot x(yx)))$

(by rule 3.)

$=\{(\lambda x\cdot yx)(\lambda z\cdot x(yx))\} \cup \text{sub}(\lambda x\cdot yx) \cup \text{sub}(\lambda z\cdot x(yx))$

(by rule 2.) (Note here we loose $z$)

$=\{(\lambda x\cdot yx)(\lambda z\cdot x(yx))\} \cup \{\lambda x\cdot yx\} \cup \text{sub}(yx) \cup \{\lambda z\cdot x(yx)\} \cup \text{sub}(x(yx))$

(simplification)

$=\{(\lambda x\cdot yx)(\lambda z\cdot x(yx)), \lambda x\cdot yx, \lambda z\cdot x(yx)\} \cup \text{sub}(yx) \cup \text{sub}(x(yx))$

(by rule 3.)

$=\{(\lambda x\cdot yx)(\lambda z\cdot x(yx)), \lambda x\cdot yx, \lambda z\cdot x(yx)\} \cup \{yx\} \cup \text{sub}(y) \cup \text{sub}(x) \cup \{x(yx)\} \cup \text{sub}(x) \cup \{yx\} \cup \text{sub}(y) \cup \text{sub}(x)$

(simplification)

$=\{(\lambda x\cdot yx)(\lambda z\cdot x(yx)), \lambda x\cdot yx, \lambda z\cdot x(yx), yx\} \cup \text{sub}(y) \cup \text{sub}(x) \cup \text{sub}(x) \cup \text{sub}(y) \cup \text{sub}(x)$

(by rule 1.)

$=\{(\lambda x\cdot yx)(\lambda z\cdot x(yx)), \lambda x\cdot yx, \lambda z\cdot x(yx), yx\} \cup \{y\} \cup \{x\} \cup \{x\} \cup \{y\} \cup \{x\}$

(simplification)

$=\{(\lambda x\cdot yx)(\lambda z\cdot x(yx)), \lambda x\cdot yx, \lambda z\cdot x(yx), yx, y, x\}$