# Blatt 07

Besprechung am 06.07.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 = {!!}
```

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