0

I see in a book on Type Theory the following definition of a subterm of a $λ$-term:

We call $L$ a subterm of $M$ if $L ∈ \mathrm{Sub}(M)$.

  • $\mathrm{Sub}(x) = \{x\}$, for each $x ∈ V. (V$ is the set of variables.)

  • $\mathrm{Sub}(MN) = \mathrm{Sub}(M) ∪ \mathrm{Sub}(N) ∪ {MN}$.

  • $\mathrm{Sub}(λx.M) = \mathrm{Sub}(M) ∪ {λx.M}$.

Well... it is as follows:

From the above definition, the properties below follow.

  1. (Reflexivity) For all $λ$-terms $M$, we have $M ∈ \mathrm{Sub}(M)$.

  2. (Transitivity) If $L ∈ \mathrm{Sub}(M)$ and $M ∈ \mathrm{Sub}(N)$, then $L ∈ \mathrm{Sub}(N)$.

Reflexivity is clear by definition, I think.

My question is how to prove transitivity.

I ask for help.

sparusaurata
  • 438
Paulo Argolo
  • 4,210

2 Answers2

1

By induction on $N$, let us show that $\forall M\in\mathrm{Sub}(N)$, $\forall L\in\mathrm{Sub}(M)$, $L \in\mathrm{Sub}(N)$:

  • If $N = x$ then $M = x$ and $L \in \mathrm{Sub}(M) = \mathrm{Sub}(N)$.
  • If $N = λx.N'$, take $M\in\mathrm{Sub}(N)$. Either $M = N$ or $M \in \mathrm{Sub}(N')$.
    In the first case the result is immediate again: $L \in \mathrm{Sub}(M) = \mathrm{Sub}(N)$.
    In the second case, by induction you have $L \in \mathrm{Sub}(N') \subset \mathrm{Sub}(N)$.
  • Similarly for the case of an application.

If it is not clear, please ask for details in the comments! :-)

sparusaurata
  • 438
  • I understood perfectly, but I don't know how to conclude. Is the procedure by induction endless? – Paulo Argolo Sep 05 '23 at 17:14
  • I can see, from the given definition, that if M is a subterm of N, then, necessarily, M "occurs in N" (M is a "part of N"), but I was wondering if it's possible to complete the proof, without use the intuitive notion of "M occurs in N". – Paulo Argolo Sep 05 '23 at 17:26
  • The induction is not endless, since the induction is on the structure of the finite term $N$ (if you want to change it to an induction on some $n \in \mathbb{N}$, you can make an induction on the depth of $N$). – sparusaurata Sep 06 '23 at 12:54
  • I don't know how to complete the proof by induction. I ask for help once again. – Paulo Argolo Sep 06 '23 at 14:15
  • I detailed the inductive argument. Is it ok like this? – sparusaurata Sep 06 '23 at 15:36
  • I didn't understand how to get the conclusion:

    "In the second case, by induction you have L ∈ Sub(N′) ⊂ Sub(N)."

    .

     – Paulo Argolo Sep 06 '23 at 16:45
  • The induction hypothesis is $\forall M'\in\mathrm{Sub}(N')$, $\forall L'\in\mathrm{Sub}(M')$, $L' \in\mathrm{Sub}(N')$. Just apply this to $M' := M$ and $L' := L$, you obtain $L \in\mathrm{Sub}(N')$ which is included in $\mathrm{Sub}(N')$ by definition. – sparusaurata Sep 06 '23 at 19:16
  • But I infer from your questions that you should (re)read something on structural induction. – sparusaurata Sep 06 '23 at 19:23
  • All good. Thank you very much! I already understood. – Paulo Argolo Sep 06 '23 at 19:29
-1

The given definition allows us to conclude that M is a subterm of N if M "occurs" in N.

Therefore, we can say:

-- M is a subterm of M.

-- If L is a subterm of M and M is a subterm of N, then L is a subterm of N.

(I'm using as intuitive the notion of "M occurs in N".)

Paulo Argolo
  • 4,210
  • This is more an intuition than a proof (“occurs in” is a synonym for “is a subterm of”), but this is indeed exactly what is to be formalised. – sparusaurata Sep 06 '23 at 12:53
  • I don't know how to complete the proof by induction, so I'm resorting to an intuitive notion. – Paulo Argolo Sep 06 '23 at 14:17