# Exercise Sheet 07

Discussion: 6 July 2026.
```
{-# OPTIONS --allow-unsolved-metas #-}

open import Data.Product
open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (Star ; ε ; _◅_ ; _◅◅_)
open import Relation.Binary using (_⇔_)

module _ where

open import SKI

private
  variable
    x y z x' y' z' w : SK
```

## Confluence of SKI
We show that SKI is confluent, that is, whenever there are multiple reduction options, they
can be merged again:
```text
      ∀
   x --->* y
 ∀ |       |
   V*      V*
   z -->* ∃w
```
Some helper definitions for later:
```
⟦K⟧ : (x y : SK) → SK
⟦K⟧ x y = x

⟦S⟧ : (x y z : SK) → SK
⟦S⟧ x y z = (x ∙ z) ∙ (y ∙ z)
```
If we try to prove confluence directly, we get stuck, because any one-step reduction
of `y` in `S x y z` amounts to two steps in `⟦S⟧ x y z`.
As a solution, we consider a new reduction relation that allows parallel reduction:
```
infixl 4 _⇉_
infixl 2 _∙'_
data _⇉_ : SK → SK → Set where
  ε : {x : SK} → x ⇉ x
  k : {x y : SK} → K ∙ x ∙ y ⇉ ⟦K⟧ x y
  s : {x y z : SK} → S ∙ x ∙ y ∙ z ⇉ ⟦S⟧ x y z
  _∙'_ : {x x' y y' : SK} → x ⇉ x' → y ⇉ y' → x ∙ y ⇉ x' ∙ y'
```

### Confluence for `K`
Show that any `K`-step allows confluence
```
K-confl : (K ∙ x ∙ y ⇉ w)
        → ∃[ w' ] (⟦K⟧ x y ⇉ w') × (w ⇉ w')
K-confl = -- <LSG>
  solution
  where
  solution : (K ∙ x ∙ y ⇉ w) → ∃[ w' ] (⟦K⟧ x y ⇉ w') × (w ⇉ w')
  solution ε = _ , ε , k
  solution k = _ , (ε , ε)
  solution (ε ∙' y⇉y') = _ , (ε , k)
  solution (ε ∙' x⇉x' ∙' y⇉y') = _ , (x⇉x' , k)
  -- </LSG>
```

### Confluence for `S`
Show that any `S`-step allows confluence; use the following helper first:
```
⟦S⟧-map : x ⇉ x' → y ⇉ y' → z ⇉ z'
        → ⟦S⟧ x y z ⇉ ⟦S⟧ x' y' z'
⟦S⟧-map x⇉x' y⇉y' z⇉z' = -- <LSG>
  (x⇉x' ∙' z⇉z') ∙' (y⇉y' ∙' z⇉z')
  -- </LSG>

S-confl : {x y z w : SK}
        → (S ∙ x ∙ y ∙ z ⇉ w)
        → ∃[ w' ] (⟦S⟧ x y z ⇉ w') × (w ⇉ w')
S-confl = -- <LSG>
  solution
  where
  solution : {x y z w : SK} → (S ∙ x ∙ y ∙ z ⇉ w) → ∃[ w' ] (⟦S⟧ x y z ⇉ w') × (w ⇉ w')
  solution ε = _ , (ε , s)
  solution s = _ , (ε , ε)
  solution (ε ∙' z⇉z') = _ , (⟦S⟧-map ε ε z⇉z' , s)
  solution (ε ∙' y⇉y' ∙' z⇉z') = _ , (⟦S⟧-map ε y⇉y' z⇉z' , s)
  solution (ε ∙' x⇉x' ∙' y⇉y' ∙' z⇉z') = _ , (⟦S⟧-map x⇉x' y⇉y' z⇉z' , s)
  -- </LSG>
```

### Diamond-Property
Show that any two reduction steps can be merged in one step:
```
confluence : {x y z : SK}
           → x ⇉ y
           → x ⇉ z
           → ∃[ w ] (y ⇉ w) × (z ⇉ w)
confluence = -- <LSG>
  solution
  where
  solution : {x y z : SK} → x ⇉ y → x ⇉ z → ∃[ w ] (y ⇉ w) × (z ⇉ w)
  solution ε x⇉z = _ , (x⇉z , ε)
  solution k x⇉z = K-confl x⇉z
  solution s x⇉z = S-confl x⇉z
  solution x⇉y ε = _ , ε , x⇉y
  solution x⇉y k = map₂ swap (K-confl x⇉y)
  solution x⇉y s = map₂ swap (S-confl x⇉y)
  solution (r1 ∙' r2) (r3 ∙' r4) =
    let w , r1→r13 , r3→r13 = solution r1 r3 in
    let w' , r2→r24 , r4→r24 = solution r2 r4 in
    (w ∙ w') , ((r1→r13 ∙' r2→r24) , (r3→r13 ∙' r4→r24))
  -- </LSG>
```
### Confluence of ⇉*
```
infixl 4 _⇉*_
_⇉*_ : SK → SK → Set
_⇉*_ = Star _⇉_

confluence-⇉-⇉* : x ⇉ y → x ⇉* z → ∃[ w ] (y ⇉* w) × (z ⇉ w)
confluence-⇉-⇉* = -- <LSG>
  solution
  where
  solution : {x y z : SK} → x ⇉ y → x ⇉* z → ∃[ w ] (y ⇉* w) × (z ⇉ w)
  solution x⇉y ε = _ , (ε , x⇉y)
  solution x⇉y (x⇉z₁ ◅ z₁⇉*z) =
    let w₁ , y⇉w₁ , z₁⇉w₁ = confluence x⇉y x⇉z₁ in
    let w  , w₁⇉*w , z⇉w  = solution z₁⇉w₁ z₁⇉*z in
    w , ((y⇉w₁ ◅ w₁⇉*w) , z⇉w)
  -- </LSG>

confluence-⇉*-⇉* : x ⇉* y → x ⇉* z → ∃[ w ] (y ⇉* w) × (z ⇉* w)
confluence-⇉*-⇉* = -- <LSG>
  solution
  where
  solution : {x y z : SK} → x ⇉* y → x ⇉* z → ∃[ w ] (y ⇉* w) × (z ⇉* w)
  solution ε x⇉*z = _ , (x⇉*z , ε)
  solution (x⇉y₁ ◅ y₁⇉*y) x⇉*z =
    let w₁ , y₁⇉*w₁ , z⇉w₁ = confluence-⇉-⇉* x⇉y₁ x⇉*z in
    let w  , y⇉*w   , w₁⇉*w = solution y₁⇉*y y₁⇉*w₁ in
    w , (y⇉*w , (z⇉w₁ ◅ w₁⇉*w))
  -- </LSG>
```

### Equivalence of `_⇉*_` and `_⟶*_`
```
⇉*<==>⟶* : _⇉*_ ⇔ _⟶*_
⇉*<==>⟶* = -- <LSG>
  ⇉*⇒⟶* , ⟶*⇒⇉*
  where
  ⟶⇒⇉ : {x y : SK} → x ⟶ y → x ⇉ y
  ⟶⇒⇉ k = k
  ⟶⇒⇉ s = s
  ⟶⇒⇉ (appl r) = ⟶⇒⇉ r ∙' ε
  ⟶⇒⇉ (appr r) = ε ∙' ⟶⇒⇉ r
  
  ⟶*⇒⇉* : {x y : SK} → x ⟶* y → x ⇉* y
  ⟶*⇒⇉* ε = ε
  ⟶*⇒⇉* (r ◅ rs) = ⟶⇒⇉ r ◅ ⟶*⇒⇉* rs

  ⇉⇒⟶* : {x y : SK} → x ⇉ y → x ⟶* y
  ⇉⇒⟶* ε = ε
  ⇉⇒⟶* k = k ◅ ε
  ⇉⇒⟶* s = s ◅ ε
  ⇉⇒⟶* (r ∙' r') = appl* (⇉⇒⟶* r) ◅◅ appr* (⇉⇒⟶* r')
  
  ⇉*⇒⟶* : {x y : SK} → x ⇉* y → x ⟶* y
  ⇉*⇒⟶* ε = ε
  ⇉*⇒⟶* (r ◅ rs) = ⇉⇒⟶* r ◅◅ ⇉*⇒⟶* rs
  
  -- </LSG>
```

### `⟶*` is confluent
Wire all above lemmas together:
```
⟶*-confluent : {x y z : SK}
             → x ⟶* y
             → x ⟶* z
             → ∃[ w ] (y ⟶* w) × (z ⟶* w)
⟶*-confluent x⟶*y x⟶*z = -- <LSG>
  let w , y⇉*w , z⇉*w = confluence-⇉*-⇉* (⟶to⇉ x⟶*y) (⟶to⇉ x⟶*z) in
  w , (⇉to⟶ y⇉*w , ⇉to⟶ z⇉*w)
  where
    ⇉to⟶ = proj₁ ⇉*<==>⟶*
    ⟶to⇉ = proj₂ ⇉*<==>⟶*
  -- </LSG>
```