# SKI Calculus

```
open import Relation.Binary.Construct.Closure.ReflexiveTransitive hiding (_>>=_; return)
open import Data.Product
```

## One-Step reduction
This assigns to K the semantics of the Λ-term λxy. x (known as `const` in Haskell)
S acts as λxyz. x z (y z) (less known as `(<*>)` for the `Applicative` instance of `((->) a)`)

```
module SKI where

infixl 5 _∙_
data SK : Set where
  S : SK
  K : SK
  _∙_ : SK → SK → SK

infix 4 _⟶_
data _⟶_ : SK → SK → Set where
  k : {x y : SK} →
    K ∙ x ∙ y ⟶ x
    
  s : {x y z : SK} →
    S ∙ x ∙ y ∙ z ⟶ x ∙ z ∙ (y ∙ z)

  appl : {x x' y : SK} →
    x ⟶ x' →
    x ∙ y ⟶ x' ∙ y

  appr : {x y y' : SK} →
    y ⟶ y' →
    x ∙ y ⟶ x ∙ y'
```

## Many-Step reduction

We define the many-step reduction as the
reflexive-transitive closure of the one-step reduction.
```
infix 4 _⟶*_
_⟶*_ : SK → SK → Set
_⟶*_ = Star _⟶_

infix 3 _∎

_∎ : (x : SK) → x ⟶* x
x ∎ = ε

infixr 2 _⟶⟨_⟩_
_⟶⟨_⟩_ : {x' y : SK} → (x : SK) → (x ⟶ x') → x' ⟶* y → x ⟶* y
_⟶⟨_⟩_ step = _◅_
```

## Combinators

We define some commonly used terms. The ornithological names a due to
[To Mock a Mockingbird](https://en.wikipedia.org/wiki/To_Mock_a_Mockingbird)

### Identity

```
I : SK
I = S ∙ K ∙ K

I-steps : {x : SK} → I ∙ x ⟶* x
I-steps {x} =
  I ∙ x ⟶⟨ s ⟩
  (K ∙ x ∙ (K ∙ x)) ⟶⟨ k ⟩
  x ∎
```

### Bluebird

```
B : SK
B = S ∙ (K ∙ S) ∙ K

B-steps : {f g x : SK} → B ∙ f ∙ g ∙ x ⟶* f ∙ (g ∙ x)
B-steps {f} {g} {x} =
  B ∙ f ∙ g ∙ x ⟶⟨ appl (appl s) ⟩
  (K ∙ S ∙ f ∙ (K ∙ f) ∙ g ∙ x) ⟶⟨ appl (appl (appl k)) ⟩
  (S ∙ (K ∙ f) ∙ g ∙ x) ⟶⟨ s ⟩
  (K ∙ f ∙ x ∙ (g ∙ x)) ⟶⟨ appl k ⟩
  f ∙ (g ∙ x) ∎
```

```
appl* : {x x' y : SK} → x ⟶* x' → x ∙ y ⟶* x' ∙ y
appl* ε = ε
appl* (step ◅ steps) = (appl step) ◅ appl* steps

appr* : {x y y' : SK} → y ⟶* y' → x ∙ y ⟶* x ∙ y'
appr* ε = ε
appr* (step ◅ steps) = (appr step) ◅ appr* steps

infixr 2 _⟶*⟨_⟩_
_⟶*⟨_⟩_ : {x' y : SK} → (x : SK) → (x ⟶* x') → x' ⟶* y → x ⟶* y
_⟶*⟨_⟩_ step = _◅◅_
```

### Mockingbird
We want to define a term with an infinite reduction sequence.
For convenience, we first prove that ⟶* is again a congruence

```
M : SK
M = S ∙ I ∙ I

M-steps : {x : SK} → M ∙ x ⟶* x ∙ x
M-steps {x} =
  M ∙ x ⟶⟨ s ⟩
  (I ∙ x ∙ (I ∙ x)) ⟶*⟨ appl* I-steps ⟩
  (x ∙ (I ∙ x)) ⟶*⟨ appr* I-steps ⟩
  x ∙ x ∎

loop : M ∙ M ⟶* M ∙ M
loop = M-steps {M}
```

## Typing
```
infixr 5 _⇒_
data type : Set where
  ⋆ : type
  _⇒_ : type → type → type

infix 3 _∶_
data _∶_ : SK → type → Set where
  k   : {α β : type} → K ∶ α ⇒ β ⇒ α
  s   : {α β γ : type} → S ∶ (α ⇒ β ⇒ γ) ⇒ (α ⇒ β) ⇒ α ⇒ γ
  app : {x y : SK} {α β : type} →
    x ∶ α ⇒ β →
    y ∶ α →
    (x ∙ y) ∶ β
```

```
I-types : {α : type} → I ∶ α ⇒ α
I-types = app (app s k) (k {β = ⋆})

B-types : {α β γ : type} → B ∶ (β ⇒ γ) ⇒ (α ⇒ β) ⇒ α ⇒ γ
B-types = app (app s (app k s)) k

M-does-not-type : ∄ λ α → M ∶ α
M-does-not-type
  (α , app (app s (app (app s ()) k)) (app (app s k) k))
```

We can interpret typed combinator terms as Agda functions.
We define the semantics of a combinator type:
```
⟦_⟧ : type → Set → Set
⟦ ⋆ ⟧ base = base
⟦ α ⇒ β ⟧ base = ⟦ α ⟧ base → ⟦ β ⟧ base

interpret : {x : SK} {α : type} → (base : Set) →
            x ∶ α → ⟦ α ⟧ base
interpret base k = λ x y → x
interpret base s = λ x y z → x z (y z)
interpret base (app x y) = interpret base x (interpret base y)
```
[Ende der Vorlesung am 18.Juni 2026]

## Preservation

```
preservation : {x y : SK} {a : type}
             → x ∶ a
             → x ⟶ y
             → y ∶ a
preservation {x = .(K ∙ y ∙ _)} {y} (app (app k v) u) k = v
preservation {x = S ∙ u ∙ v ∙ w} {y = .(u ∙ w ∙ (v ∙ w))} (app (app (app s u∶) v∶) w∶) s = app (app u∶ w∶) (app v∶ w∶)
preservation (app t t') (appl x⟶y) = app (preservation t x⟶y) t'
preservation (app t t') (appr x⟶y) = app t (preservation t' x⟶y)

```

## Progress
```
data normal : SK → Set where
  k : normal K
  k' : ∀ {x} → normal x → normal (K ∙ x)

  s : normal S
  s' : ∀ {x} → normal x → normal (S ∙ x)
  s'' : ∀ {x y} → normal x → normal y → normal (S ∙ x ∙ y)


four-step : ∀ {a b c d : SK} → ∃[ y ]  (a ∙ b ∙ c ∙ d) ⟶ y
four-step {S} = _ , s
four-step {K} = _ , appl k
four-step {a ∙ a'} {b} {c} =
  let y , aa'bc⟶y = four-step {a} {a'} {b} {c} in
  _ , appl aa'bc⟶y

open import Data.Empty
open import Data.Sum
open import Function.Base
open import Relation.Nullary using (¬_)
normal⇒¬step : {x : SK} → normal x → (∃[ y ] x ⟶ y) → ⊥
normal⇒¬step (k' x) (y , appr x⟶y) = normal⇒¬step x (_ , x⟶y)
normal⇒¬step (s' x) (y , appr x⟶y) = normal⇒¬step x (_ , x⟶y)
normal⇒¬step (s'' x x') (y , appl (appr x⟶y)) = normal⇒¬step x (_ , x⟶y)
normal⇒¬step (s'' x x') (y , appr x'⟶y) = normal⇒¬step x' (_ , x'⟶y)

DecProg : SK → Set
DecProg x = normal x ⊎ ∃[ y ] x ⟶ y

prog-map : {x : SK}
         → DecProg x
         → {f : SK → SK}
         → (∀ {y} → x ⟶ y
                  → f x ⟶ f y)
         → (normal x → DecProg (f x))
         → DecProg (f x)
prog-map (inj₁ x-normal) _ rule = (rule x-normal)
prog-map (inj₂ (y , x⟶y)) {f = f} rule _ = inj₂ ((f y) , (rule x⟶y))

progress : ∀ x → normal x ⊎ (∃[ y ] x ⟶ y)
progress S = inj₁ s
progress K = inj₁ k
-- progress (S ∙ y) with (progress y)
-- ... | inj₁ y-normal = inj₁ (s' y-normal)
-- ... | inj₂ (z , y⟶z) = inj₂ (_ , (appr (y⟶z)))
progress (S ∙ y) = prog-map (progress y)   appr (inj₁ ∘ s')
--                  {f = S ∙_} ----------^
progress (K ∙ y) = prog-map (progress y) appr (inj₁ ∘ k')
-- Langversion
-- progress (S ∙ x ∙ y) with (progress x)
-- ... | inj₁ x-normal =
--     prog-map (progress y) {f = λ - → S ∙ x ∙ - } appr (inj₁ ∘ s'' x-normal)
-- ... | inj₂ (x' , x⟶x') = inj₂ ((S ∙ x' ∙ y) , (appl (appr x⟶x')))
-- Kurzversion:
progress (S ∙ x ∙ y) =
  prog-map (progress x) (appl ∘ appr) λ x-normal →
  prog-map (progress y) appr (inj₁ ∘ s'' x-normal)
progress (K ∙ x ∙ y) = inj₂ (x , k)
progress (w ∙ x ∙ y ∙ z) = inj₂ four-step

module Langversion where
  ¬step⇒normal : {x : SK} → ¬ (∃[ y ] x ⟶ y) → normal x
  ¬step⇒normal {x} ¬∃ with (progress x)
  ... | inj₁ x₁ = x₁
  ... | inj₂ y = ⊥-elim (¬∃ y)

¬step⇒normal : {x : SK} → ¬ (∃[ y ] x ⟶ y) → normal x
¬step⇒normal {x} ¬∃y = fromInj₁ (⊥-elim ∘ ¬∃y) (progress x)

```
[Ende der Vorlesung am 22. Juni 2026]

## Normalization
```
module SKI-Normalizing where
  open import Data.Unit
  open import Data.Nat
  open import Function.Base using (case_of_; _∋_)

  normalize : SK → Set
  normalize x = ∃[ b ] (x ⟶* b × normal b)

  already-normal : ∀ {x} → normal x → normalize x
  already-normal {x} nx = x , (ε , nx)

  S-normal : normalize S
  S-normal = already-normal s


  -- Failed Attempt:
  -- types⇒normalize : ∀ {x} {t} → x ∶ t → normalize x
  --  ....
  -- types⇒normalize {S ∙ x ∙ y ∙ z} (app (app (app s x∶α) y∶β⇒a) z∶α⇒β⇒t) = {!x∶t₃!}
  --   where
  --     IH-Sxy : normalize (S ∙ x ∙ y)
  --     IH-Sxy = types⇒normalize (app (app s x∶α) y∶β⇒a)

  --     IH : normalize ((x ∙ z) ∙ (y ∙ z))
  --     IH = types⇒normalize (app (app x∶α z∶α⇒β⇒t) (app y∶β⇒a z∶α⇒β⇒t))
  --     -- ^-- argument nicht strukturell kleiner

  module apply-f-do where
    _>>=_ : {X Y : Set} → (X → Y) → (X → Y)
    _>>=_ f = f
    return = already-normal

  map-normalize : {f : SK → SK}
                → (∀ {x y : SK} → x ⟶ y → f x ⟶ f y)
                → {a : SK}
                → normalize a
                → (∀ {x : SK} → normal x → normalize (f x))
                → normalize (f a)
  map-normalize {f} f-step (b , a⟶*b , normal-b) f-normal =
    let c , f[b]⟶*c , normal-c = f-normal normal-b in
    c , gmap f f-step a⟶*b ◅◅ f[b]⟶*c , normal-c

  Sx-normal : {x : SK} → normalize x → normalize (S ∙ x)
  Sx-normal nx = map-normalize {f = S ∙_} appr nx (already-normal ∘ s')

  Sxy-normal : {x y : SK} → normalize x → normalize y → normalize (S ∙ x ∙ y)
  Sxy-normal {x} nx ny = do
    ny' ← map-normalize {f = S ∙ x ∙_} appr ny
    nx' ← map-normalize {f = λ x' → S ∙ x' ∙ _} (appl ∘ appr) nx
    return (s'' nx' ny')
    where open apply-f-do

  _∈ₜ_ : SK → type → Set
  x ∈ₜ ⋆ = normalize x
  f ∈ₜ (t ⇒ u) = normalize f × (∀ {x} → x ∈ₜ t → (f ∙ x) ∈ₜ u)

  ∈ₜ⇒normalize : ∀ {t : type} {x}→ x ∈ₜ t → normalize x
  ∈ₜ⇒normalize {t = ⋆} n = n
  ∈ₜ⇒normalize {t = t ⇒ u} (n , _) = n

  ⟶ₙ-prep : ∀ {x} {y} → x ⟶ y → normalize y → normalize x
  ⟶ₙ-prep x⟶y (z , y⟶*z , z-normal) = z , ((x⟶y ◅ y⟶*z) , z-normal)

  ⟶ₙ-prep' : ∀ {x} {y} {t : type} → x ⟶ y → y ∈ₜ t  → x ∈ₜ t 
  ⟶ₙ-prep' {t = ⋆} x⟶y yₙ = ⟶ₙ-prep x⟶y yₙ
  ⟶ₙ-prep' {t = t ⇒ u} x⟶y yₙ = (⟶ₙ-prep x⟶y (yₙ .proj₁)) ,
    λ {p} pₙ → ⟶ₙ-prep' (appl x⟶y) (proj₂ yₙ pₙ) 

  _∙ₙ_ : ∀ {f x} {t u : type} → f ∈ₜ (t ⇒ u) → x ∈ₜ t → (f ∙ x) ∈ₜ u
  _∙ₙ_ f x = proj₂ f x

  Sxyz-normal : {a b c : type} → S ∈ₜ ((a ⇒ b ⇒ c) ⇒ (a ⇒ b) ⇒ a ⇒ c)
  Sxyz-normal {a} {b} {c} = S-normal , λ {x} xₙ →
    (Sx-normal (∈ₜ⇒normalize {a ⇒ b ⇒ c} xₙ)) , (λ {y} yₙ →
    Sxy-normal (∈ₜ⇒normalize {a ⇒ b ⇒ c} xₙ) (∈ₜ⇒normalize {a ⇒ b} yₙ) , λ {z} zₙ →
    ⟶ₙ-prep' s ((_∙ₙ_ {u = b ⇒ c} xₙ zₙ) ∙ₙ (yₙ ∙ₙ zₙ)))

  Kxy-normal : {a b : type} → K ∈ₜ (a ⇒ b ⇒ a)
  Kxy-normal = (K , ε , k) , λ xₙ →
    map-normalize appr (∈ₜ⇒normalize xₙ) (already-normal ∘ k')
    , λ {y} yₙ →
    ⟶ₙ-prep' k xₙ

  types⇒normalize* : ∀ {x} {t} → x ∶ t → x ∈ₜ t
  types⇒normalize* k = Kxy-normal
  types⇒normalize* s = Sxyz-normal
  types⇒normalize* {f ∙ x} (app f∶t⇒u x∶t) =
    proj₂ (types⇒normalize* f∶t⇒u) (types⇒normalize* x∶t)


  types⇒normalize : ∀ {x} {t} → x ∶ t → normalize x
  types⇒normalize = ∈ₜ⇒normalize ∘ types⇒normalize*
```
[Ende der Vorlesung am 25. Juni 2026]