4
$\begingroup$

I'm trying to prove the following reduction: $$ t\{x:=u\}\{y:=v\} = t\{y:=v\}\{x:=u\{y:=v\}\} $$ under the following assumptions:

  1. $x \neq y$
  2. $x$ is not a free variable of $v$ (in symbols, $x \notin \operatorname{fv}(v)$).

My idea is to do it by induction, but I'm a bit stuck with the base case. I would appreciate if someone can explain to me how to write such a proof. I'm including what I tried, which is wrong or incomplete.

Base case: $t = m$ is just a variable.

On the left side we have:

if m = x ⟹ u{y:=v} (if u=y then v else u)
else     ⟹ m{y:=v} (if m=y then v else m)

On the right side we have:

if m=y ⟹ v{x:=u{y:=v}} (if u=y then v{x:=v} else u{x:=u}
  so we get either (v=x ⟹ v else v) or (u=x ⟹ u else u) 
else   ⟹ m{x:=u{y:=v}} (if m=y then m{x:=v} else m{x:=u}
  so we get either v or m

I understand we end up getting the same four branches, but is that considered really a proof? Is this the proper way to write such a proof and conclude the base case? Also, the given assumptions didn't help much here, so I think I'm missing the part where I need to use those assumptions...

I think once the base case is proven, we can do the following:

Case $t = t_1t_2$:

$$t\{x:=u\}\{y:=v\} \Longrightarrow t_1t_2\{x:=u\}\{y:=v\} \Longrightarrow \\ t_1\{x:=u\}\{y:=v\} t_2\{x:=u\}\{y:=v\},$$ and we have just proven in the base case that $t_1\{x:=u\}\{y:=v\} = t_1\{y:=v\}\{x:=u\{y:=v\}\}$ and $t_2\{x:=u\}\{y:=v\} = t_2\{y:=v\}\{x:=u\{y:=v\}\}$, so \begin{align} &t_1\{x:=u\}\{y:=v\} t_2\{x:=u\}\{y:=v\} \\ =& t_1\{y:=v\}\{x:=u\{y:=v\}\} t_2\{y:=v\}\{x:=u\{y:=v\}\} \\ = &t_1t_2\{x:=u\}\{y:=v\} \\ = &t_1t_2\{y:=v\}\{x:=u\{y:=v\}\}. \end{align}

Now only case left is $t= \lambda m . t$. So we have $(\lambda m . t)\{x:=u\}\{y:=v\}$, which can be directly re-written as $\lambda m . t\{x:=u\}\{y:=v\}$, which is the base case again...

Could someone please help me finish this proof correctly and explain to me the right way to do it?

$\endgroup$
2
  • $\begingroup$ Your text is impossible to read. This is not how one would write a proof. I started rewriting your proof, but since your question is about how to write proofs, I abandoned my attempt. Consult some lecture notes to see how proofs are usually written. $\endgroup$ – Yuval Filmus Jan 13 at 8:48
  • $\begingroup$ @YuvalFilmus thx for taking the time to rewrite my question and answer me with such clear explanation ! $\endgroup$ – user206904 Jan 13 at 11:30
4
$\begingroup$

First, let us show that the two assumptions are necessary. Here is an example showing what goes wrong when $x = y$. Take $t = x$, $u = 1$, $v = 2$. We have $$ x\{x := 1\}\{x := 2\} = 1\{x := 2\} = 1, $$ whereas $$ x\{x := 2\}\{x := 1\{x := 2\}\} = 2\{x := 1\} = 2. $$

Next, here is an example showing what goes wrong when $x$ is not free in $v$. Take $t = y$, $x = 1$, $y = x$. We have $$ y \{x := 1\}\{y := x\} = y\{y := x\} = x, $$ whereas $$ y \{y := x\}\{x := 1\{y := x\}\} = x\{x := 1\} = 1. $$

Now let's do the base case more carefully. The term $t$ is just a variable. We have to consider three possibilities: $t=x$, $t=y$, $t \neq x,y$.

If $t=x$ then $t\{x := u\} = u$, and so the left-hand side is $u\{y := v\} = u\{y := v\}$. On the other hand, $t\{y := v\} = x$ (since $x \neq y$), and so the right-hand side is $x\{x := u\{y := v\}\} = u \{y := v\}$.

If $t=y$ then $t\{x := u\} = y$ (since $y \neq x$), and so the left-hand side is $y\{y := v\} = v$. On the other hand, $t\{y := v\} = v$, and so the right-hand side is $v\{ x:= u\{y := v\} \} = v$, since $x$ doesn't appear freely in $v$.

Finally, if $t \neq x,y$ then both sides are just equal to $t$, since the substitutions have no effect.

Next, the rest of the proof. The proof for function application is essentially as you wrote it. Let us denote the left-hand side by $L(t)$ and the right-hand side by $R(t)$. If $t = t_1t_2$ then $$ L(t) = L(t_1) L(t_2) \stackrel{(\ast)}= R(t_1) R(t_2) = R(t), $$ where $(\ast)$ is due to the induction hypothesis.

Finally, we need to handle abstraction. Let $t = \lambda m.s$. Applying $\alpha$-conversion, we can assume without loss of generality that $m \neq x,y$. This implies that $$ L(t) = \lambda m.L(s) = \lambda m.R(s) = R(t). $$ To see why $\alpha$-conversion is necessary, try doing the proof when $m=x$ or $m=y$. The case $m=x$ works out fine, but you will encounter a problem when $m=y$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.