patternMinor
Nominal unification: How this lemma is proved?
Viewed 0 times
thisunificationlemmahowprovednominal
Problem
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.
$\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.
Solution
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:
-
Show that it suffices to prove:
$$\nabla\vdash \sigma(\pi^{-1}.t) \approx \sigma(X) $$
-
Show that the above derivation is implied by
$$\nabla\vdash \sigma(t)\approx\pi.\sigma(X) $$
-
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.
The proof proceeds in 3 steps:
-
Show that it suffices to prove:
$$\nabla\vdash \sigma(\pi^{-1}.t) \approx \sigma(X) $$
-
Show that the above derivation is implied by
$$\nabla\vdash \sigma(t)\approx\pi.\sigma(X) $$
-
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.
Context
StackExchange Computer Science Q#71663, answer score: 3
Revisions (0)
No revisions yet.