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:

      ∀
   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>

Agda Quellcode herunterladen