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?



Your Answer

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