SKI with Variables
{-# OPTIONS --allow-unsolved-metas --without-K #-} open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (Star ; ε ; _◅_ ; _◅◅_; gmap) open import Data.Product using (_,_ ; ∃ ; ∄) open import Data.Sum using (_⊎_ ; inj₁ ; inj₂) open import Data.Empty using (⊥-elim) open import Relation.Nullary open import Data.Nat using (ℕ; suc) import Data.Nat.Properties as ℕ import Data.Nat as ℕ open import Relation.Binary.Definitions using (DecidableEquality; tri<; tri≈; tri>) open import Relation.Binary.PropositionalEquality hiding (subst) open import Function.Base using (case_of_; id) module SKIx where private variable V : Set variable W : Set
Syntax
module SKx (V : Set) where infixl 5 _∙_ data SK : Set where ′_ : V → SK K : SK S : SK _∙_ : SK → SK → SK module SKx⟶ {V : Set} where open SKx V 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' infix 2 _⟶*_ _⟶*_ : 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 = _◅_ infixr 2 _⟶*⟨_⟩_ _⟶*⟨_⟩_ : {x' y : SK} → (x : SK) → (x ⟶* x') → x' ⟶* y → x ⟶* y _⟶*⟨_⟩_ step = _◅◅_ _⟩∙⟨_ : {x x' y y' : SK} → (x ⟶* x') → (y ⟶* y') → (x ∙ y ⟶* x' ∙ y') _⟩∙⟨_ {x' = x'} {y = y} xs ys = gmap (_∙ y) appl xs ◅◅ gmap (x' ∙_) appr ys module SK-subst where open SKx subst : (V → SK W) → SK V → SK W subst f (′ x) = f x subst f K = K subst f S = S subst f (t ∙ r) = subst f t ∙ subst f r
Variable Binding
module bind (V : Set) (_≟_ : DecidableEquality V) where open SK-subst open SKx⟶ open SKx V replace_by_ : V → SK → (V → SK) replace_by_ v r x with (v ≟ x) ... | yes _ = r ... | no _ = ′ x _[_/_] : SK → SK → V → SK _[_/_] t r v = subst (replace v by r) t _↦_ : V → SK → SK v ↦ (′ x) with (v ≟ x) ... | yes v≡x = S ∙ K ∙ K ... | no v≢x = K ∙ ′ x v ↦ K = K ∙ K v ↦ S = K ∙ S v ↦ (f ∙ p) = S ∙ (v ↦ f) ∙ (v ↦ p) β-step : {v : V} {t x : SK} → (v ↦ t) ∙ x ⟶* t [ x / v ] β-step {v} {t = ′ x} with (v ≟ x) ... | yes v≡x = s ◅ (k ◅ ε) ... | no v≢x = k ◅ ε β-step {t = K} = k ◅ ε β-step {t = S} = k ◅ ε β-step {v} {t = f ∙ p} {x} = (v ↦ (f ∙ p)) ∙ x ⟶*⟨ ε ⟩ S ∙ (v ↦ f) ∙ (v ↦ p) ∙ x ⟶⟨ s ⟩ ((v ↦ f) ∙ x ∙ ((v ↦ p) ∙ x)) ⟶*⟨ β-step {t = f} ⟩∙⟨ β-step {t = p} ⟩ (f [ x / v ] ∙ p [ x / v ]) ⟶*⟨ ε ⟩ ((f ∙ p) [ x / v ]) ∎
Lambda Calculus
Instead of using variables, de Bruijn (pronounced like the colour) indices count how many binders are between a variable and its corresponding binder.
module LT where infixl 5 _∙_ data LT : Set where ′_ : ℕ → LT _∙_ : LT → LT → LT Λ_ : LT → LT K : LT -- λ x λ y . x K = Λ (Λ ′ 1) S : LT -- λ x λ y λ z . (x ∙ z) ∙ (y ∙ z) S = Λ Λ Λ (′ 2 ∙ ′ 0 ∙ (′ 1 ∙ ′ 0)) Example : LT -- λ x . x ∙ (λ y . x ∙ y) ∙ x Example = Λ ((′ 0) ∙ (Λ (′ 1 ∙ ′ 0)) ∙ (′ 0)) inj : ℕ → LT → LT inj n (′ x) with (n ℕ.≤? x) ... | yes n≤x = ′ suc x ... | no n>x = ′ x inj n (t ∙ t') = inj n t ∙ inj n t' inj n (Λ t) = Λ inj (suc n) t _[_/_] : LT → LT → ℕ → LT _[_/_] (′ x) r v with (ℕ.<-cmp x v) ... | tri< x<v _ _ = ′ x -- Fix ... | tri≈ _ x≡v _ = r ... | tri> _ _ v<x = ′ ℕ.pred x _[_/_] (f ∙ p) r v = f [ r / v ] ∙ p [ r / v ] _[_/_] (Λ t) r v = Λ (t [ inj 0 r / (suc v) ]) infix 4 _⟶_ data _⟶_ : LT → LT → Set where β-step : {f p : LT} → (Λ f) ∙ p ⟶ f [ p / 0 ] appl : {x x' z : LT} → x ⟶ x' → x ∙ z ⟶ x' ∙ z appr : {x x' z : LT} → x ⟶ x' → z ∙ x ⟶ z ∙ x' Λ_ : {x y : LT} → x ⟶ y → Λ x ⟶ Λ y
Ende der Vorlesung am 29.06.2026
module translation where open LT open SKx ℕ open bind ℕ ℕ._≟_ module wrong-definition where F : LT → SK F (′ x) = ′ x F (t ∙ s) = F t ∙ F s F (Λ t) = 0 ↦ F t -- only works for lambda terms without free variables F : ℕ → LT → SK F d (′ x) = ′ (d ℕ.∸ (suc x)) F d (t ∙ s) = F d t ∙ F d s F d (Λ t) = d ↦ F (suc d) t B : SK → LT B (′ x) = ′ x B K = LT.K B S = LT.S B (t ∙ s) = B t ∙ B s
Ende der Vorlesung am 02.07.2026