Why not Takahashi‘s method to prove confluence?

[L-TChen]

I was also trying to prove confluence using Takahashi’s approach, and with the sigma-algebra developed in the section on substitution I am able to prove the following par-complete-dev by a simple induction on the derivation of parallel reduction.

_⁺ : Γ ⊢ A → Γ ⊢ A
(` x) ⁺       =  ` x
(λ̇ M) ⁺       = λ̇ (M ⁺)
((λ̇ M) · N) ⁺ = M ⁺ [ N ⁺ ]
(M · N) ⁺     = M ⁺ · (N ⁺)

par-complete-dev : M =⇒ N → N =⇒ M ⁺

Then the confluence property follows easily.

But, in the development version of plfa, I noticed the following paragraph

We opted not to use the “complete developments” approach of Takahashi (1995) because we felt that the proof was simple enough based solely on parallel reduction.

If the proof can be made even simpler, then why not?

[jsiek]

Dear Liang-Ting Chen,

That's great that you've given this approach a try. My concern with Takahashi's method for this section is that I believe there is a trade-off: one defines a second notion of parallel reduction (an increase in complexity) in exchange for a proof that includes one less case (decrease in complexity). So it was not obvious to me that Takahashi's method would lead to a simpler development all things considered.

But now that you have done this alternative proof, we can compare the two developments to see which is really simpler. Would you be willing to share your Agda code?

Best regards, Jeremy

[L-TChen]

Sorry for my late reply. I don't bring my work laptop home (even though I still cannot resist thinking about it and working from a tablet), but my formalisation needs to be polished in the style of plfa.

Here is the core part of my formalisation:

_⁺ : ∀ {Γ A}
  → Γ ⊢ A → Γ ⊢ A
(` x) ⁺       =  ` x
(ƛ M) ⁺       = ƛ (M ⁺)
((ƛ M) · N) ⁺ = M ⁺ [ N ⁺ ]
(M · N) ⁺     = M ⁺ · (N ⁺)

par-dev : ∀ {Γ A} {M N : Γ ⊢ A}
  → M ⇛ N
    -------
  → N ⇛ M ⁺
par-dev pvar = pvar
par-dev (pbeta M⇛M′ N⇛N′) =
  sub-par (par-dev M⇛M′) (par-dev N⇛N′) 
par-dev (pabs M⇛M′) = pabs (par-dev M⇛M′)
par-dev (papp {ƛ _} (pabs M⇛M′) N⇛N′) =
  pbeta (par-dev M⇛M′) (par-dev N⇛N′)
par-dev (papp {` x} pvar N) =
  papp (par-dev pvar) (par-dev N)
par-dev (papp {L · M} LM⇛M′ N) =
  papp (par-dev LM⇛M′) (par-dev N)

strip : ∀{Γ A} {M N N′ : Γ ⊢ A}
  → M ⇛ N
  → M ⇛* N′
    ------------------------------------
  → Σ[ L ∈ Γ ⊢ A ] (N ⇛* L)  ×  (N′ ⇛ L)
strip mn (M ∎) = ⟨ _ , ⟨ _ ∎ , mn ⟩ ⟩
strip mn (M ⇛⟨ mm' ⟩ m'n')
  with strip (par-dev mm') m'n'
... | ⟨ L , ⟨ ll' , n'l' ⟩ ⟩ =
      ⟨ L , ⟨ (_ ⇛⟨ par-dev mn ⟩ ll') , n'l' ⟩ ⟩

The main difference is that

1. par-diamond is replaced by the complete development _⁺ and par-dev and
2. the strip lemma has only one with abstraction.

Each inductive case of par-dev either follows from induction hypothesis or from the substitution lemma sub-par. The complete development is intuitive. Although the original proof of par-diamond is not complicated, it is rather messy in my opinion.

[jsiek]

The Takahashi version uses 32 lines in total to prove the strip lemma, whereas the existing proof based on the diamond property uses 47 lines. Also, just eye-balling the two proofs, I agree that the Takahashi version is simpler.

Would you like to do a pull request for this? If not, my plan will be to update this chapter to use Takahashi's method when I find the time to write the necessary text to explain it.

[L-TChen]

I can give it a try (when I find the time as well)!

[L-TChen]

Thanks for pinging me. It has been on my to-do list for a while. I just need to finish a few more things (review, summer school organisation, etc.) before getting back to this.

[iwilare]

Hello! I've been following this discussion and would like to suggest some improvements that could be made. I've also proven this lemma as follows:

par-triangle : ∀ {Γ A} {M N : Γ ⊢ A}
  → M ⇛ N
    --------
  → N ⇛ M ⁺
par-triangle {M = ` x} pvar = pvar
par-triangle {M = ƛ M} (pabs M⇛N) = pabs (par-triangle M⇛N)
par-triangle {M = (ƛ M) · N} (pbeta M⇛M′ N⇛N′)       = sub-par (par-triangle M⇛M′) (par-triangle N⇛N′)
par-triangle {M = (` _) · N} (papp  M⇛M′ N⇛N′)       = papp  (par-triangle M⇛M′) (par-triangle N⇛N′)
par-triangle {M = _ · _ · N} (papp  M⇛M′ N⇛N′)       = papp  (par-triangle M⇛M′) (par-triangle N⇛N′)
par-triangle {M = (ƛ _) · N} (papp (pabs M⇛M′) N⇛N′) = pbeta (par-triangle M⇛M′) (par-triangle N⇛N′)

However, I would argue that still showing the diamond lemma as an intermediate step is a clearer and easier to understand choice:

par-diamond : ∀ {Γ A} {M A B : Γ ⊢ A}
  →           M ⇛ A  →  M ⇛ B
    ----------------------------
  → ∃[ N ] ((A ⇛ N) × (B ⇛ N))
par-diamond {M = M} M⇛A M⇛B = ⟨ M ⁺ , ⟨ par-triangle M⇛A , par-triangle M⇛B ⟩ ⟩

This shows more clearly that the confluent term is precisely M ⁺ with the explicit Takahashi translation applied. The strip lemma then requires no modification, and proceeds as usual (with its two intrinsic commutating squares).

• The name par-triangle seemed to me more appropriate because it is quoted as such in "Term Rewriting Systems" (Terese, 2003) and in "Autosubst: Reasoning with de Bruijn Terms and Parallel Substitution" (Schäfer-Tebbi-Smolka, 2015), also quoted in PLFA in the Substitution chapter. And especially because of its graphical form:

  M
  ︲\
  ︲ \
  ︲  \
  ︲   N
  ︲  /
  ︲ /
  ︲/
  M⁺

• Using * instead of ⁺ might also be a clearer choice, in terms of being easier to see (the unicode apex looks a bit small? Unfortunately there is no easy to type version with , which is already somewhat lifted) and also because of the fact that Takahashi uses in the original 1995 revised version instead.
• I then tried @L-TChen's version but the implicit arguments didn't work with me, could it be because of another order in the implicit arguments?

I hope this helps! If there's anything I can do I will gladly try to be of help!

[jsiek]

Thanks Andrea, that sounds quite helpful!