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