3
$\begingroup$

In page 455, of Pierce´s TAPL and page 560, the single-step diamond property of reduction:

$S \Rrightarrow S' \land T \Rrightarrow T' \implies \exists V. T \Rrightarrow V \land U \Rrightarrow V$

is proved. The argument goes by induction on the total sizes of the given derivations, with a case analysis on the final rules of both. I think this is a bit of an overkill since I think I have a proof by induction on $S$.

If $S = X$ then $T=U=X$ and we can take $V = X$.

If $S = S_1 \to S_2$ then $T = T_1 \to T_2$ and $U = U_1 \to U_2$ where $S_1 \Rrightarrow T_1, S_2 \Rrightarrow T_2, S_1 \Rrightarrow U_1, S_2 \Rrightarrow U_2$. By induction hypothesis, $\exists V_1,V_2. T_1, U_1 \Rrightarrow V_1, T_2,U_2 \Rrightarrow V_2$ and by the rule QR-Arrow $T \Rrightarrow V_1 \to V_2, U \Rrightarrow V_1 \to V_2$.

The rest of the cases are similar with the help of lemma 30.3.7:

$S \Rrightarrow S', T \Rrightarrow T' \implies [Y \mapsto S]T \Rrightarrow [Y \mapsto S']T'$

for the case QR-AppAbs.

Could you help me understand what's wrong with my proofs?

$\endgroup$

0

Your Answer

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