Intro

{-# OPTIONS --allow-unsolved-metas --without-K #-}

Curry-Howard-Korrespondenz

Beweis-Regeln und Regeln von Typsystemen stehen in Korrespondenz zueinander:

Logik Programme
vgl. GLoIn vgl. ThProg
Logische Formeln A ∧ B → A Typen von Programmen A × B → A
Beweise Γ ⊢ A ∧ B → A Typisierung: Γ ⊢ (λ p. p λ x y. x) : A × B → A
Implikation A → B Funktionstyp A → B
Konjunktion A ∧ B Produkt-Typ A × B
Disjunktion A ∨ B Union-Typ A + B
Allquantor ∀x.φ(x) Polymorphismus ∀ x.φ(x)

⇒ Wir beweisen mathematische Aussagen, indem wir Programme mit dem passenden Typ konstruieren.

Syntax

  • Haskell-artig
  • Identifier: UTF-8-Zeichenkennten getrennt durch Leerzeichen und .;{}()@"

Funktionstypen

Agda ist dependently-typed, das bedeutet, dass Typen von Werten abhängen können. Da 'Set' ist selbst ein Typ, lässt sich damit Polymorphismus, implementieren:

id : ∀ (S : Set) → S → S
id S x = x

Hier ist S ein Wert vom Typ Set.

id' : ∀ (S : Set) → (S → S)
id' = λ S → λ x → x

Der Funktionstyp S → S selbst liegt auch in Set:

Endofunction : Set → Set
Endofunction S = S → S

-- Definition mittels Endofunction:
id₂ : ∀ (S : Set) → Endofunction S
id₂ S x = x

Holes

Statt von oben nach unten schreibt man Agda-Programme von außen nach innen:

id₃ : ∀ (S : Set) → Endofunction S
id₃ S x = x -- Ersetzen Sie x durch ? um ein Hole zu erzeugen

Operatoren

_∨_ : Set → Set → Set₁
A ∨ B = ∀ (C : Set) → (A → C) → (B → C) → C

_∧_ : Set → Set → Set₁
A ∧ B = ∀ (C : Set) → (A → B → C) → C
  • Funktion X -> Y und X und Y auf level ℓ, dann ist (X → Y) auch auf Level ℓ
  • Funktion X -> Y bedeutet: ∀ (x : X) → Y
  • Parameter C ist vom Typ Set
  • => Set → Set ∈ Set₁

Modules

module Logic-Examples (A : Set) (B : Set) where
  ∨-comm : (A ∨ B) → (B ∨ A)
  ∨-comm A∨B C B→C A→C = A∨B C A→C B→C

Datentypen

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ


_+_ : ℕ → ℕ → ℕ
zero + b = b
suc a + b = suc (a + b)

open import Data.Bool using (Bool; true; false)

_≡?_ : ℕ → ℕ → Bool
zero ≡? zero      = true
zero ≡? suc b     = false 
suc a ≡? zero     = false
suc a ≡? suc b    = a ≡? b

data _≡_ {ℓ} {X : Set ℓ} : X → X → Set ℓ where
  refl : ∀ (x : X) → x ≡ x

infix 4 _≡_

zero+a≡a : ∀ (a : ℕ) → zero + a ≡ a
zero+a≡a a = refl a
Ende der Vorlesung am 13. April 2026

Implizite Argumente

  • Funktionsargumente können weggelassen werden, wenn sich diese durch die Unifikation automatisch ergeben.
  • Syntax:
  • {…} um in der Funktionsdefinition ein Argument als implizit zu markieren
  • _ um beim Funktionsaufruf ein explizites Argument von Agda finden zu lassen.
-- Funktionen erhalten Gleichheit:
cong : ∀ {a b : ℕ} → (f : ℕ → ℕ) → a ≡ b → f a ≡ f b
cong f (refl a) = refl (f a)

-- Wenn wir cong aufurufen, dann ergeben sich die Werte für
-- a und b automatisch aus `a ≡ b`
a+zero≡a : ∀ (a : ℕ) → a + zero ≡ a
a+zero≡a zero = refl zero
a+zero≡a (suc a) =
  cong {a + zero} {a} suc (a+zero≡a a)
  -- identisch zu: cong {a + zero} {a} suc (a+zero≡a a)

Weiteres Beispiel: Implizite Grundmenge bei _≡_ oben. In der stdlib ist der Parameter an refl implizit, da er sich meist aus dem Kontext ergibt, wie z. B. in der Definition von sym:

sym : ∀ {X : Set} {a : X} {b} → a ≡ b → b ≡ a
sym (refl _) = refl _
--        ^         ^--- Agda leitet den Parameter aus dem Kontext ab
--        '----  Der Wert bekommt keinen Namen, steht aber trotzdem zur Verfügung:
--               a : ℕ   (not in scope)

trans : ∀ {X : Set} {a b c : X} → a ≡ b → b ≡ c → a ≡ c
trans (refl x) eq = eq

+-suc : ∀ a b → suc (a + b) ≡ (a + suc b)
+-suc zero b = refl (suc b)
+-suc (suc a) b = cong suc (+-suc a b)

+-comm₀ : ∀ a b → a + b ≡ b + a
+-comm₀ zero b = sym (a+zero≡a b)
+-comm₀ (suc a) b = trans (cong suc IH) (+-suc b a)
  where
    IH = +-comm₀ a b


subst : ∀ {a b : ℕ} → (P : ℕ → Set) → a ≡ b → P a → P b
subst P (refl a) = id (P a)

+-comm : ∀ a b → _≡_ (a + b) (b + a)
+-comm zero b = sym (a+zero≡a b)
+-comm (suc a) b = trans (cong suc (+-comm a b)) (+-suc b a)

Gleichungsketten

_∎ : ∀ {X : Set} (n : X) → n ≡ n
_∎ = refl
infix 3 _∎

_≡⟨_⟩_ : ∀ {X : Set} n {m} → n ≡ m → {ℓ : X} → m ≡ ℓ → n ≡ ℓ
n ≡⟨ n≡m ⟩ m≡ℓ = trans n≡m m≡ℓ 
infixr 2 _≡⟨_⟩_

+-comm' : ∀ a b → _≡_ (a + b) (b + a)
+-comm' zero b = sym (a+zero≡a b)
+-comm' (suc a) b =
        (suc a + b) ≡⟨ cong suc (+-comm' a b) ⟩
        suc (b + a) ≡⟨ +-suc b a ⟩
        (b + suc a) ∎

Warnung: die Gleichungsketten in der stdlib beginnen mit begin_

Entscheidungsprozeduren

  • Einbettung Bool ↪ Set
  • Korrektheitsbeweis von _≡?_
  • Dot-Pattern
-- import Data.Empty
data ⊥ : Set where

-- import Data.Unit
data ⊤ : Set where
  tt : ⊤

Truth : Bool → Set
Truth false = ⊥
Truth true = ⊤

≡?-⇐ : ∀ a b → a ≡ b → Truth (a ≡? b)
≡?-⇐ zero a (refl a) = tt
≡?-⇐ (suc a) (suc a) (refl (suc a)) = ≡?-⇐ a a (refl _)
Ende der Vorlesung am 16. April 2026

In ≡?-⇐ nutzen wir das Prinzip des "Fordings".

Rückrichtung:

≡?-⇒ : ∀ a b → Truth (a ≡? b) → a ≡ b
≡?-⇒ zero zero t = refl _
≡?-⇒ zero (suc b) ()   -- hier kein '=', () ≡ "unmögliches pattern"
≡?-⇒ (suc a) (suc b) t = cong suc (≡?-⇒ a b t)

Level

import Level as L
open import Level using (Level)

weak-initial : {ℓ : Level} (X : Set ℓ) → Set (L.suc ℓ)
weak-initial {ℓ} X = ∀ (Y : Set ℓ) → (X → Y)

Funktionen

_∘_ : ∀ {ℓ₁ ℓ₂ ℓ₃} {X : Set ℓ₁} {Y : Set ℓ₂} {Z : Set ℓ₃} →
        (Y → Z) → (X → Y) → (X → Z)
(g ∘ f) x = g (f x)

∘-assoc : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} {W : Set ℓ₁} {X : Set ℓ₂} {Y : Set ℓ₃} {Z : Set ℓ₄}
          (f : W → X) (g : X → Y) (h : Y → Z) → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
∘-assoc f g h = refl _

Records

module Non-Dependent-Product where

Das übliche Produkt ist ein record:

  record _×_ {ℓ ℓ' : Level} (X : Set ℓ) (Y : Set ℓ') : Set (ℓ L.⊔ ℓ') where
    constructor _,_
    field
      fst : X
      snd : Y

  module ×-properties {ℓ ℓ' : Level} (X : Set ℓ) (Y : Set ℓ') where
    swap : X × Y → Y × X
    swap (x , y) = y , x

    swap' : X × Y → Y × X
    swap' p =
      record
      { fst = p.snd
      ; snd = p.fst
      }
      where
        module p = _×_ p

Dependent-Product:

record Σ {ℓ ℓ' : Level} (X : Set ℓ) (P : X → Set ℓ') : Set (ℓ L.⊔ ℓ') where
  constructor _,_
  field
    fst : X
    snd : P fst

syntax Σ A (λ x → B) = Σ[ x ∈ A ] B

_×_ : {ℓ ℓ' : Level} (X : Set ℓ) (Y : Set ℓ')
      → Set (ℓ Level.⊔ ℓ')
X × Y = Σ X (λ x → Y)

∃ : {ℓ ℓ' : Level} {X : Set ℓ} (P : X → Set ℓ') → Set (ℓ L.⊔ ℓ')
∃ = Σ _
syntax ∃ (λ x → B) = ∃[ x ] B

Currying des Dependent-Products = Dependent Functions:

module Dependent-Currying (X : Set) (P : X → Set) (Y : Set) where
  curry : (Σ[ x ∈ X ] (P x) → Y) → (∀ (x : X) → P x → Y)
  curry f x Px = f (x , Px)

  uncurry : (∀ (x : X) → P x → Y) → (Σ[ x ∈ X ] (P x) → Y)
  uncurry f (x , Px) = f x Px

  _⇔_ : Set → Set → Set
  X ⇔ Y = (X → Y) × (Y → X)

  [un]curry : (∀ (x : X) → P x → Y) ⇔ (∃[ x ] (P x) → Y)
  [un]curry = uncurry , curry

  uncurry∘curry≡id : uncurry ∘ curry ≡ id _
  uncurry∘curry≡id = refl (uncurry ∘ curry)

  curry∘uncurry≡id : curry ∘ uncurry ≡ id (∀ (x : X) → P x → Y)
  curry∘uncurry≡id = refl _

Funktionen

Die Relation f ≐ g beschreibt, dass die Funktionen f und g Punktweise identisch sind:

_≐_ : ∀ {ℓ₁ ℓ₂} {X : Set ℓ₁} {Y : Set ℓ₂} (f g : X → Y) → Set (ℓ₁ L.⊔ ℓ₂)
f ≐ g = ∀ x → f x ≡ g x

Stdlib

import Function.Base using (_∘_) -- ∘ allows composition of dependent functions

Agda Quellcode herunterladen