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 = {!!}

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' = {!!}

S-confl : {x y z w : SK}
        → (S ∙ x ∙ y ∙ z ⇉ w)
        → ∃[ w' ] (⟦S⟧ x y z ⇉ w') × (w ⇉ w')
S-confl = {!!}

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 = {!!}

Confluence of ⇉*

infixl 4 _⇉*_
_⇉*_ : SK → SK → Set
_⇉*_ = Star _⇉_

confluence-⇉-⇉* : x ⇉ y → x ⇉* z → ∃[ w ] (y ⇉* w) × (z ⇉ w)
confluence-⇉-⇉* = {!!}

confluence-⇉*-⇉* : x ⇉* y → x ⇉* z → ∃[ w ] (y ⇉* w) × (z ⇉* w)
confluence-⇉*-⇉* = {!!}

Equivalence of _⇉*_ and _⟶*_

⇉*<==>⟶* : _⇉*_ ⇔ _⟶*_
⇉*<==>⟶* = {!!}

⟶* 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 = {!!}

Agda Quellcode herunterladen