2
$\begingroup$

Before I will ask my question, I would refer you to the relevant information in the 1998 version of the book "Lectures on the Curry-Howard Isomorphism" (https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf), which you can find in page 9, but I will also put here:

$1.4.1.$ Definition. A relation $>$ on $\Lambda$ satisfies the diamond property if, for all $M_1, M_2, M_3 \in \Lambda$, if $M_1 > M_2$ and $M_1 > M_3$, then there exists an $M_4 \in \Lambda$ such that $M_2 > M_4$ and $M_3 > M_4$.

$1.4.2.$ Lemma. Let $>$ be a relation on $\Lambda$ and suppose that its transitive closure is $\twoheadrightarrow_\beta$. If $>$ satisfies the diamond property, then so does $\twoheadrightarrow_\beta$.

Proof. First show by induction on $n$ that $M_1 > N_1$ and $M_1>\cdots>M_n$ implies that there are $N_2, \dots, N_n$ such that $N_1 > N_2 > \cdots > N_n$ and $M_n>N_n.$

Using this property, show by induction on $m$ that if $N_1 > \cdots > N_m$ and $N_1 >^* M_1$, then there are $M_2, \dots, M_m$ such that $M_1 > M_2 > \cdots > M_m$ and $N_m>^*M_m.$

The proof continues on page 10. Usually, I like to verify everything by myself to see that it makes sense, so I proved the first induction in the first paragraph.

Now, I want to write the induction proof of the second paragraph, but I have a problem. According to the footnote in this page (which you can read through the link to the book), the uppercase star symbol on a relation is the transitive closure of the relation (e.g. $R^*$ is the transitive closure of $R$). So does it mean that $>^*$ is the transitive closure of $>$? If so, then why not just use the symbol $\twoheadrightarrow_\beta$, which is defined exactly like that? And could you show me how to prove this paragraph? If that's not the meaning of this symbol, then what does mean?

$\endgroup$

1 Answer 1

1
$\begingroup$

Lemma 1.4.2 and its proof use two different symbols, $>^*$ and $↠_\beta$ to represent the transtive closure of the relation $>$.

Note that in the sequel of the section, for instance in lemma 1.4.6 and in theorem 1.4.7, the symbol $↠_\beta$ represent a specific relation on the set $\Lambda$ of $\lambda$-terms, i.e. the so called multi-step $\beta$-reduction (which is the reflexive-transitive closure of $\beta$-reduction $\to_\beta$).

The use of the symbol $↠_\beta$ in lemma 1.4.2 is misleading because it clashes with the interpretation of that symbol in the sequel of the section, but strickly speaking it is not an error.


The statement in the second paragraph in the proof of lemma 1.4.2 is

if $N_1 > \cdots > N_m$ and $N_1 >^* M_1$, then there are $M_2, \dots, M_m$ such that $M_1 > M_2 > \cdots > M_m$ and $N_m>^*M_m.\qquad$ (*)

The proof of (*) is by induction on $m \geq 1$.

The base case is for $m = 1$. We have to show that if $N_1 >^* M_1$ then $N_1 >^* M_1$, which is trivially true.

For the inductive case, we suppose that the property ( * ) is true for some $m \geq 1$ (this is the inductive hypothesis), and we want to prove that it is true for $m +1$. So, suppose $N_1 > \cdots > N_m > N_{m+1}$ and $N_1 >^* M_1$. By induction hypothesis applied to $N_1 > \cdots > N_m$, we know that there exist $M_2, \dots, M_m$ such that $M_1 > M_2 > \cdots > M_m$ and $N_m>^*M_m$. Thus, we have $N_m > N_{m+1}$ and $N_m >^* M_m$: by property stated in the first paragraph of the proof of lemma 1.4.2, there exists $M_{m+1}$ such that $N_{m+1} >^* M_{m+1}$ and $M_m > M_{m+1}$. Thereofore, $M_1 > M_2 > \cdots > M_m > M_{m+1}$ and $N_{m+1}>^*M_{m+1}$, and so the property (*) holds for $m+1$.

$\endgroup$
5
  • $\begingroup$ Thanks a lot! Could you add the induction proof of the second paragraph to your answer? For some reason, I straggle with it. $\endgroup$ Dec 7, 2019 at 13:20
  • 1
    $\begingroup$ @MichaelNovak - Done. Note that in the statement you wrote and want to prove there was a typo (absent in the original pdf), I fixed it. $\endgroup$ Dec 7, 2019 at 21:20
  • $\begingroup$ What I don't understand is how can you apply the property from the first paragraph of the proof? I mean, $N_m >^* M_m$ doesn't imply $N_m > M_m$, right? $\endgroup$ Dec 8, 2019 at 0:33
  • 1
    $\begingroup$ @MichaelNovak - Of course, $N_m>^∗M_m$ doesn't imply $N_m>M_m$, but you don't need it. The property in the first paragraph of the proof of lemma 1.4.2 is: if $T_1 > S_1$ and $T_1 >^* T_n$ then there is $S_n$ such that $S_1 >^* S_n$ and $T_n>S_n$. I applied this property to $T_1 = N_m$ and $S_1 = N_{m+1}$ and $T_n = M_m$, so I get $S_n = M_{m+1}$ such that $S_1 = N_{m+1} >^* M_{m+1} = S_n$ and $T_n = M_m > M_{m+1} = S_n$. $\endgroup$ Dec 8, 2019 at 6:39
  • $\begingroup$ Oh, now I understand. Thank you very much for your patience! $\endgroup$ Dec 8, 2019 at 12:22

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .