5
$\begingroup$

I was reading nominal unification paper. I could not understand the proof of a lemma. The paper is here nominal unification. The lemma is following. $\sigma$ is a substitution, $\pi$ is a permutation (swapping of atoms).

Lemma 3.3. if $\Delta \vdash \sigma(\pi .X) \approx \sigma(t)$, then $\sigma.[X:=\pi^{-1}.t] = \sigma $.

The paper said, to prove the lemma, need to show that $\Delta \vdash \sigma(\pi^{-1}.t) \approx \sigma(X)$. It first showed $\Delta \vdash \sigma(t) \approx \pi.\sigma(X)$, from which, then the paper finished the proof by saying the following.

The case the follows from the assumptions by symmetry and commuting the permutation inside the substitution.

I could not imagine how $\sigma.[X:=\pi^{-1}.t] = \sigma $ is obtained from $\Delta \vdash \sigma(\pi^{-1}.t) \approx \sigma(X)$. what does that "assumptions by symmetry" mean?

Could anyone point out what proof technique is used here?

Thanks.

$\endgroup$
2
  • $\begingroup$ You've mis-tokenized the sentence. The tokens are "follows from assumptions" and "by symmetry", not "follows from" and "assumptions by symmetry". $\endgroup$ Mar 20, 2017 at 10:54
  • $\begingroup$ @DavidRicherby I see, thanks. but I still don't understand the proof. $\endgroup$
    – alim
    Mar 20, 2017 at 11:15

2 Answers 2

3
+50
$\begingroup$

chi's answer is mostly correct, but I've poured through the paper, and can probably fill in the gaps a bit:

The proof proceeds in 3 steps:

  1. Show that it suffices to prove: $$\nabla\vdash \sigma(\pi^{-1}.t) \approx \sigma(X) $$

  2. Show that the above derivation is implied by $$\nabla\vdash \sigma(t)\approx\pi.\sigma(X) $$

  3. Show that in turn this is implied by the assumptions of the theorem.

The structure of the proof is a bit confusing, since it proceeds "backwards", from the conclusion of the theorem to the hypothesis.

The first step involves mostly unpacking the definition of substitutions and the notation $\sigma\ \circ\ [X:=t]$.

The second step is handled by lemmas in the paper (lemmas 2.14 and 2.12 if we're reading the same version). This step is the most complex of the proof.

The last part is performed by changing $\nabla\vdash \sigma(t)\approx\pi.\sigma(X)$ to $\nabla\vdash \pi.\sigma(X)\approx\sigma(t)$ by applying symmetry and once again applying using lemma 2.14 to move $\pi$ "inside" the permutation to get $$\nabla\vdash \sigma(\pi.X)\approx\sigma(t) $$

which is exactly the assumption!

Again, the only real difficulty is that the proof is working backwards, starting from the conclusion and finding stronger and stronger statements until you get the hypothesis.

$\endgroup$
1
  • $\begingroup$ Thanks for your answer. It is much clear to me now. Just one question about "The first step involves mostly unpacking the definition of substitutions and the notation σ ∘ [X:=t]". Could you explain to me the unpacking the definition of substitutions? This has been one point I did not understand clearly. $\endgroup$
    – alim
    Apr 8, 2017 at 17:18
2
$\begingroup$

My guess is that, once you have proved $\Delta \vdash \sigma(t) \approx \pi.\sigma(X)$ you can derive, applying $\pi^{-1}$ on both sides, the relation $\Delta \vdash \pi^{-1} . \sigma(t) \approx \pi^{-1}.\pi.\sigma(X)$, which simplifies to $\Delta \vdash \pi^{-1} . \sigma(t) \approx \sigma(X)$. This is the "symmetry" step the paper mentions.

Then, if we can commute $\pi^{-1}$ with the substitution, we can rewrite $\Delta \vdash \pi^{-1} . \sigma(t) \approx \sigma(X)$ as $\Delta \vdash \sigma(\pi^{-1} . t) \approx \sigma(X)$.

This implies that $\sigma$ does not distinguish between $X$ and $\pi^{-1} . t$: in both cases it produces the same result (modulo $\approx$). Hence, performing substitution $\sigma$ is equivalent to first replacing $X$ with $\pi^{-1} . t$ and then applying $\sigma$.

Note -- I have not checked the paper in detail, so I can't guarantee this fits the paper exactly, but it looks plausible to me.

$\endgroup$

Your Answer

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

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