Benutzer:Demon667/Agda (Programmiersprache)

Agda
Basisdaten
Paradigmen:	funktional
Designer:	Catarina Coquand und Makoto Takeyama (Agda 1), Ulf Norell (Agda 2)
Entwickler:	Andreas Abel, Guillaume Allais, Liang-Ting Chen, Jesper Cockx, Matthew Daggitt, Nils Anders Danielsson, Amélia Liao, Ulf Norell
Aktuelle Version:	2.7.0.1  (2024-09-12)
Aktuelle Vorabversion:	2.8.0  ()
Typisierung:	statisch, stark, Typinferenz, term-abhängig (engl. dependent)
Dialekte:	Cubical
Beeinflusst von:	Haskell
Betriebssystem:	plattformübergreifend
Lizenz:	Agda Lizenz
https://wiki.portal.chalmers.se/agda/Main/HomePage

Agda ist eine funktionale Programmiersprache, die sich durch ihr Typsystem auch als Beweisassistent eignet. Das Wort "funktional" bezieht sich hier auf die Verwendung von Funktionen als Objekte, die nicht nur definiert und aufgerufen werden, sondern auch als Variablen übergeben und als Wert zurückgegeben werden können. Es ist eine sog. totale Sprache, in der alle Funktionen terminieren und einen Wert des Ergebnistyps zurückgeben. Diese Eigenschaft ist notwendig, damit die Beweise, die man in Agda formuliert, stichhaltig sind. Das Typsystem basiert auf Arbeiten von Per Martin-Löf und kann über die Curry-Howard-Korrespondenz zur Formulierung logischer Aussagen genutzt werden. Dazu ist es notwendig, dass die Typen in Agda auch von Werten abhängen können (engl. dependently typed).

In Agda kann man einerseits klassische Programme schreiben, die zuerst in Haskell und über den Glasgow-Haskell-Compiler in eine ausführbare Datei übersetzt werden. Andererseits - und das ist eher die Regel - kann man auch Programme schreiben, bei denen der Typprüfer sämtliche zur Übersetzungszeit vorliegenden Informationen nutzt, um bestimmte Berechnungen durchzuführen. Das Programm braucht nicht in eine ausführbare Datei übersetzt zu werden und benötigt dementsprechend keinen Einsprungpunkt.

Weiterhin kann man in Agda mit einem leeren Quelltext beginnen und von Grund auf eigene Typen und Funktionen definieren, ohne dass man eine Standardbibliothek für Basisfunktionen nutzen muss. Es sind dann auch keine impliziten Typ- oder Funktionsdefinitionen vorhanden (ausser der Set-Hierarchie). Es gibt jedoch eine Standardbibliothek, die derzeit (Stand 2025) aktiv weiterentwickelt wird.

Der Quelltext in Agda kann an bestimmten Stellen Lücken (eingegeben durch ein ?) enthalten. Diese verhindern zwar die Erstellung eines ausführbaren Programms, gelten aber nicht als Fehler während der Kompilierung. Vielmehr meldet der Compiler, welchen Typ er an der entsprechenden Stelle erwartet. Dies wird üblicherweise als Ziel (engl. Goal) bezeichnet. Ist der Typ soweit eingeschränkt, dass der Compiler bestimmen kann, welcher Wert eingesetzt werden muss, kann dieser den fehlenden Wert automatisch einsetzen.

Agda wird normalerweise über Plug-ins in Emacs, Vim oder Visual Studio Code bedient. Hier werden bestimmte Tastenkombinationen genutzt, um den Quelltext auf Typ-Korrektheit zu prüfen, die Typziele der Lücken abzufragen, automatische Einsetzungen vorzunehmen, Typen abzufragen oder auch den vom Compiler berechneten Wert einer Variable zu ermitteln. Ist der Quelltext typkorrekt, dann wird er auch entsprechend der Syntax eingefärbt. Dies ist eine andere Reihenfolge als bei Programmiersprachen, bei denen die integrierte Entwicklungsumgebung den Quelltext zuerst eingefärbt (und eventuelle Syntaxfehler aufzeigt) und später bei der Kompilierung nachträglich noch eventuelle Typfehler aufdeckt.

Die Syntax von Agda basiert auf der Verwendung von Leerzeichen zur Trennung von Syntaxelementen oder zur Einrückung. Bezeichner können (fast) beliebige Unicode-Zeichen enthalten. Zum Beispiel ist 1≤2 (ohne Leerzeichen) ein gültiger Bezeichner, während 1 ≤ 2 (mit Leerzeichen) einen Ausdruck darstellt. Funktionen werden mit Hilfe von Pattern Matching definiert.

Es ist möglich und vorgesehen, dass man Agda-Quelltexte auch direkt in Dokumenten und Artikeln (engl. literate programming) verwendet. Die Quelltexte haben dann nicht mehr die Endung .agda, sondern z.B. .lagda.md für Markdown-Text oder .lagda.tex für LaTeX-Dokumente. Der Quelltext wird in entsprechende Blöcke im Dokument eingefasst.

Agda ist auf verschiedenen Plattformen verfügbar und kann mittels des Cabal-Paketsystems von Haskell installiert werden. Für die Benutzung ohne Installation steht das Onlinetool Agdapad zur Verfügung.

Compilerdialog und Programme ohne Einsprungpunkt

Ein sehr einfaches Agda-Programm, was einen Daten-Typ Bool definiert und das logische UND implementiert, könnte wie folgt aussehen:

module wiki-simple where -- jede Quelldatei ist ein Modul

data Bool : Set where -- Bool ist ein: 
  true  : Bool        -- entweder "true"
  false : Bool        -- oder "false"

_∧_ : Bool → Bool → Bool  -- logisch-UND ist eine Funktion, die zwei Bool-Argumente benötigt und einen Bool zurückgibt
true  ∧ b = b             -- 1. Fall: 1. Argument = true, 2. Argument beliebig: Rückgabe = 2. Argument.
false ∧ b = false         -- 2. Fall: 1. Argument = false, 2. Argument beliebig: Rückgabe = false

x : Bool  -- x ist vom Typ Bool
x = true  -- x ist "true"

y : Bool  -- y ist vom Typ Bool
y = false -- y ist "false"

z : Bool  -- z ist vom Typ Bool
z = x ∧ y -- z ist x UND y; C-n z ergibt false

Hierzu einige Bemerkungen:

• data ist notwendig, damit man mit einem leeren Quelltext starten kann. Es ist die Basis dafür, dass man "alles" selbst implementieren kann.
• In Agda wird durch den Doppelpunkt : ein Typurteil gekennzeichnet. Man sieht, dass Bool den Typ Set hat. Das bedeutet soviel wie, dass Bool ein "kleiner" Typ ist. Set (ist implizit Set 0) selbst hat den Typ Set 1. Somit wird eine unendliche Hierarchie an Typen aufgebaut. Dies vermeidet z.B. die Russelsche Antinomie.
• true und false nennt man Typkonstruktoren.
• Das logische UND wird durch _∧_ repräsentiert. Die zwei Unterstriche weisen ∧ als Infix-Funktion aus.
• Der Pfeil _→_ repräsentiert einen Funktionstyp. Verkettete Pfeile sind eine andere Schreibweise für Funktionen mit mehreren Eingaben. Der Pfeil ist rechtsassoziativ, d.h. Bool → Bool → Bool bedeutet eigentlich Bool → (Bool → Bool). Wenn man also das linke Argument in _∧_ einsetzt, erhält man eine Funktion, die einen Bool braucht (das rechte Argument) und daraus einen Bool macht. Siehe hierzu Currying oder Schönfinkeln.
• Die Definitionen von _∧_ decken alle Fälle ab, dafür sorgt der Typprüfer. Er prüft auch, ob die Funktion terminiert.
• Die Vorgaben von x und y zur Typprüfungszeit ermöglichen es, z bei der Typprüfung auszurechnen. Daher kann man z nach der Typprüfung abfragen.
• Ein Einsprungpunkt main ist in diesem Beispiel nicht vorhanden.

Definiert man nun eine Funktion für das logische ODER, sieht das so aus:

_∨_ : Bool → Bool → Bool  -- logisch-ODER ist eine Funktion, die zwei Bools als Argumente braucht und einen Bool zurückgibt
a ∨ b = {!!}              -- Definition mit Lücke

Die Lücke wird nach der Typprüfung mit { }0 bezeichnet und im Meldungsfenster wird

?0 : Bool

gezeigt. Das ist ein Hinweis darauf, dass noch offene Lücken existieren, die geschlossen werden müssen. Man kann die Ziele noch detaillierter anzeigen lassen. Die Ziel-Ansicht der Lücke { }0 zeigt

Goal: Bool
————————————————————————————————————————————————————————————
b : Bool
a : Bool

Dies besagt, dass hier ein Bool erwartet wird und dafür a und b, beide jeweils Bool, im Kontext verfügbar sind. Bool ist an dieser Stelle allerdings so unspezifisch, dass der Typprüfer nicht eindeutig ermitteln kann, was in die Lücke muss. Die Semantik muss also hier vom Programmierer festgelegt werden. Das weitere Vorgehen ist es, eine Fallunterscheidung für a nach true oder false vorzunehmen und dann die beiden Zeilen entsprechend auszufüllen:

_∨_ : Bool → Bool → Bool
true  ∨ b = true
false ∨ b = b

Programme mit Einsprungpunkt

Um ein Programm mit Einsprungpunkt in Agda zu erstellen, empfiehlt es sich, die Standardbibliothek zu nutzen.

{-# OPTIONS --guardedness #-}
module wiki-hello where

open import IO
-- notwendig für "Main", "putStrLn", "getLine", alle Ein-/Ausgabeoperationen
open import Data.String using (_++_)
-- notwendig für Stringoperationen: _++_ = Stringverkettung

main : Main                          -- Einsprungspunkt
main = run do                        -- do-Notation wie in Haskell
  putStrLn "Gib Deinen Namen ein: "  -- putStrLn kann nur innerhalb von "do" verwendet werden
  name ← getLine                     -- "Zuweisung" des Outputs von getLine an "name"
  putStrLn ("Hallo, " ++ name)       -- Verwendung von "name" in putStrLn

Hier muss man auch noch ein paar Bemerkungen machen:

• --guardedness ist notwendig für z.B. unendliche Listen (Streams) oder allgemein coinduktive Daten, wie sie von IO genutzt werden.
• import importiert aus einem Modul alles oder mit using nur die spezifizierten (vollständig qualifizierten) Bezeichner in das aktuelle Modul.
• open entfernt den vorderen Teil des vollständigen Bezeichners (also statt IO.Main nur Main).
• Main ist eine Abkürzung für den Typen IO ⊤, wobei ⊤ für den sog. Einheitstyp steht.
• Die do-Notation funktioniert wie in Haskell. IO ist eine Monade und do ist nur syntaktischer Zucker für eine monadische Verkettung von Operationen wie putStrLn und getLine.

Mit Hilfe der hier genannten Mittel kann man ein ausführbares Programm in Agda erzeugen, welches Terminaleingaben entgegennimmt und -ausgaben erzeugt.

Unendliche, indizierte und parametrisierte Datentypen

Oben wurde der einfache Datentyp Bool eingeführt. Mit endlichen "ist ein"-Datentypen kann man genauso verfahren, also die Konstruktoren einfach aufzählen. Bei "unendlichen" Datentypen hingegen, sind meistens Argumente der Konstruktoren durch den Datentyp selbst gegeben. Daneben unterstützt das data-Schlüsselwort noch Typindizes (rechts vom Doppelpunkt) und Typparameter (links vom Doppelpunkt).

Natürliche Zahlen

Für die natürlichen Zahlen funktioniert die endliche Aufzählung der Konstruktoren nicht mehr. Hier behilft man sich mit den Peano-Axiomen, unter anderem:

• Null ist eine natürliche Zahl und
• jede andere natürliche Zahl ist Nachfolger einer natürlichen Zahl.

Das wird in Agda wie folgt dargestellt:

data ℕ : Set where
  zero : ℕ     -- Null: kann direkt konstruiert werden
  suc  : ℕ → ℕ -- Nachfolger: braucht ein Argument vom Typ ℕ

Hier kommt neu hinzu, dass der Konstruktor suc (für Nachfolger) eine natürliche Zahl als Parameter braucht, um ein gültiges Element des Typs zu erzeugen. Dann ist z.B. one = suc zero und two = suc (suc zero) usw..

Nun kann man noch eine Addition natürlicher Zahlen definieren, die sich die Formulierung in Form von Null und Nachfolger zunutze macht:

_+_ : ℕ → ℕ → ℕ
zero  + m = m           -- 0 + m = m (aber NICHT m + 0 = m!)
suc n + m = suc (n + m) -- suc n + m = suc (n + m)

Hier gibt es eine Fallunterscheidung im ersten Argument. Die Addition wird rekursiv definiert und zwar so, dass für den Fall "Null" rechts keine Rekursion mehr steht (Basisfall) und für den Fall "Nachfolger" rechts "strukturell kleinere" Argumente für _+_ stehen (insbesondere kein suc mehr).

Typindizes als Relationen

Will man nun natürliche Zahlen mit Hilfe der Kleiner-Gleich-Beziehung vergleichen, hat man mehrere Möglichkeiten. Die erste ist, dass man eine Funktion schreibt, die den Typ ℕ → ℕ → Bool hat. Die zweite Möglichkeit ist, dass man einen Typen anlegt, der das leistet. Gemäß der Curry-Howard-Korrespondenz sind Typen auch als Aussagen zu verstehen. Dazu braucht man eine sog. (homogene, zweistellige) Relation. Mathematisch ist das eine Teilmenge des kartesischen Produkts der Ausgangsmenge mit sich selbst, also $\leq \,\subset \,\mathbb {N} \times \mathbb {N}$. In Agda modelliert man das mit sog. indizierten Datentypen (hier mit zwei Indizes):

data _≤_ : ℕ → ℕ → Set where              -- jeder Konstruktor braucht zwei Argumente
  z≤n : {n : ℕ}   →          zero ≤ n     -- z≤n kann direkt generiert werden 
  s≤s : {n m : ℕ} → m ≤ n → suc m ≤ suc n -- s≤s braucht als Argument einen Beweis, dass die beiden Vorgänger auch die Relation erfüllen

Am Ende heisst das, dass jeder Typkonstruktor mit zwei natürlichen Zahlen parametrisiert wird. Im vorliegenden Fall braucht aber nur zwei Konstruktoren:

• Null ist immer kleiner oder gleich einer beliebigen natürlichen Zahl (z≤n) und
• Falls n ≤ m dann gilt das auch für ihre Nachfolger (s≤s).
• Die Argumente in geschweiften Klammern sind implizit und werden von Agda ausgefüllt.

Das kann man z.B. zum Beweis nutzen, dass 2 ≤ 4 ist:

2-kleiner-gleich-4 : (suc (suc zero)) ≤ (suc (suc (suc (suc zero))))
2-kleiner-gleich-4 = s≤s (s≤s z≤n)

data definiert einen Typen. Daher ist die Aussage 2 ≤ 4 als Typ der Variable 2-kleiner-gleich-4 implementiert. Nun hat man links und rechts des ≤ jeweils einen Nachfolger stehen, daher kann nur der Konstruktor s≤s in Frage kommen. Das Argument von s≤s ist aber vom Typ her nicht mehr die ursprüngliche Ungleichung sondern beide Seiten um eins vermindert (1 ≤ 3). Nun kann man noch einmal s≤s einsetzen. Dessen inneres Argument ist aber vom Typ (0 ≤ 2). Das entspricht aber dem Konstruktor z≤n, welcher keine weiteren Argumente hat und damit die Rekursion beendet. Die Aussage ist durch den Typen repräsentiert und der Beweis durch eine Variable diesen Typs.

Um natürliche Zahlen nicht nur als zero oder suc zu erzeugen, kann man auch ein sog. Pragma (eine Compiler-Anweisung) verwenden, hier

{-# BUILTIN NATURAL ℕ #-}

Damit könnte man die Variable 2-kleiner-gleich-4 von oben auch wie folgt definieren:

2-kleiner-gleich-4' : 2 ≤ 4
2-kleiner-gleich-4' = s≤s (s≤s z≤n)

Ein anderes Beispiel für eine Aussage in Form eines indizierten Datentyps ist das aller geraden natürlichen Zahlen $\subset \mathbb {N}$. Da man hier nur eine Teilmenge der natürlichen Zahlen anschaut, braucht man nur einen Typindex:

data IsEven : ℕ → Set where
  zeroIsEven   : IsEven zero
  sucsucIsEven : {n : ℕ} → IsEven n → IsEven (suc (suc n))

Auch hier kann man wieder einen Beweis dafür, dass 4 gerade ist, führen

4-iseven : IsEven 4
4-iseven = sucsucIsEven (sucsucIsEven zeroIsEven)

Die Argumentation läuft ähnlich wie oben: 4 ist der Nachfolger-Nachfolger von 2, daher muss man mit dem Konstruktor sucsucIsEven starten. Das Argument von sucsucIsEven ist dann aber vom Typ IsEven 2. 2 ist aber Nachfolger-Nachfolger von 0 und daher muss man wieder sucsucIsEven verwenden. Dessen Argument hat aber dann den Typ IsEven 0, was nur durch den Konstruktor zeroIsEven abgedeckt wird. Dieser hat keine Argumente mehr und beendet die Rekursion. Versucht man das mit einer ungeraden Zahl, landet man irgendwann beim Typ IsEven 1. Den kann man aber nicht konstruieren.

Typindizes zur Präzisierung von Daten

Typindizes benutzt man auch, um Datentypen zu präzisieren. Hier ein Beispiel über Speisen und ihren Zuckergehalt.

data ZuckerSalz : Set where
  zucker : ZuckerSalz
  salz   : ZuckerSalz

data Speise : ZuckerSalz → Set where
  kuchen     : Speise zucker
  butterbrot : Speise salz
  dessert    : Speise zucker

data Gewicht : Set where
  _g : ℕ → Gewicht

zuckergehalt : Speise zucker → Gewicht
zuckergehalt kuchen  = 100 g
zuckergehalt dessert = 20 g

Speisen werden durch Zucker oder Salz präzisiert. Während Kuchen und Dessert Zucker enthalten, wird das Butterbrot mit Salz gereicht. Die Funktion zuckergehalt bekommt dann nur eine Speise mit dem Typindex zucker übergeben (daher wird das butterbrot im Patternmatching gar nicht abgefragt) und gibt ein Gewicht zurück. (In Gewicht könnte man noch mehr Konstruktoren bereitstellen und so auch das Thema Maßeinheiten mit Hilfe von Typdefinitionen angehen. Auch hier könnte man durch einen Typindex präzisieren z.B. zwischen metrischen und anderen Einheiten.)

Typparameter

Eine andere Typkonstruktion ist eine (typ-)homogene Liste. Eine Liste ist entweder eine leere Liste oder eine Zusammensetzung von erstem Element und hinterer Liste:

data List (A : Set) : Set where
  []  : List A                   -- leere Liste: kann direkt angelegt werden
  _∷_ : A → List A → List A      -- sog. Cons-Liste: braucht als Argument ein vorderes Listenelement (head) und eine hintere Liste (tail)

infixr 2 _∷_                     -- _∷_ ist rechtsassoziativ mit Priorität 2  

liste1 : List ℕ
liste1 = 3 ∷ 4 ∷ 1 ∷ 0 ∷ []

liste2 : List Bool
liste2 = true ∷ false ∷ false ∷ []

Der Typparameter A (hier der Typ der Listenelemente) ist eine globale Konstante in der data-Definition. im Beispiel wurde _∷_ rechtsassoziativ gemacht. Damit ist 3 ∷ 4 ∷ 1 ∷ 0 ∷ [] eigentlich (3 ∷ (4 ∷ (1 ∷ (0 ∷ [])))). Andersherum (also linksassoziativ) ergäbe keinen Sinn, da 3 ∷ 4 keine sinnvolle Liste wäre.

Typparameter und Typindizes gemeinsam

Will man nun das erste Element einer Liste erhalten, kann es passieren, dass die Liste aber leer ist. In dem Fall muss man sich um das Abfangen von Fehlern kümmern. Agda bietet aber die Möglichkeit, eine Liste zu definieren, die in ihrer Typdefinition ihre Länge mitführt. Hier wird dann eine Mischung aus Typparameter (für den homogenen Typ) und Typindex (für die Länge) genutzt:

data Vec (A : Set) : ℕ → Set where
  []  :                         Vec A 0
  _∷_ : {n : ℕ} → A → Vec A n → Vec A (suc n)

vec1-len3 : Vec ℕ 3
vec1-len3 = 3 ∷ 1 ∷ 4 ∷ []

vec2-len5 : Vec Bool 5
vec2-len5 = true ∷ false ∷ false ∷ true ∷ true ∷ []

head : {A : Set} → {n : ℕ} → Vec A (suc n) → A
head (x ∷ xs) = x

Man sieht, dass Vec entsprechend seiner Definition immer zwei Parameter hat, nämlich A, was innerhalb des data-Blocks gleich bleibt und n, was sich ändern kann. vec1-len3 und vec2-len5 haben definierte Typen und Längen. Alle Abweichungen davon bei der Zuweisung würden Typfehler nach sich ziehen. head zeigt in seiner Typsignatur, dass der Vektor auf den es angewandt wird, die Länge suc n hat und dementsprechend nicht Null sein kann. Daher hat die Fallunterscheidung in der Definition auch keinen Fall, wo der leere Vektor [] auftaucht. Demzufolge muss head keinen Fehler abfangen, wenn der Vektor leer ist.

Π- und Σ-Typen

Π-Typen sind Funktionstypen, bei denen der Typ des Ergebnisses von der Eingabe abhängt. Im Grunde benutzt man solche Konstruktionen in Agda dauernd, entweder implizit oder explizit, auf jeden Fall aber in Beweisen. Der Π-Typ (für Set) ist wie folgt definiert:

Π : (A : Set) → (A → Set) → Set  -- Π ist eine Funktion, die einen Typen und eine Typfunktion aus diesem Typen in Set nach Set abbildet (also einen Typen erzeugt) 
Π A B = (x : A) → B x            -- Der erzeugte Typ ist ein Funktionstyp dessen benanntes Argument (x : A) in einen Typen, der vom Argument abhängt (B x) abgebildet wird

Π-Typen sind fest in Agda verankert und der Kern der Programmierung mit Typen, die von Werten abhängen. Das Π spielt hier darauf an, dass man informell von einem unendlichen kartesischen Produkt reden könnte. Nutzt man für B eine Funktion, die für true einen Typen A zurückgibt und für false einen Typen B, erhält man das klassische kartesiche Produkt $A\times B$.

_×'_ : Set → Set → Set                      -- Das kartesische Produkt ist eine Abbildung von Set und Set nach Set
A ×' B = Π Bool λ { true → A ; false → B }  -- Der unabhängige Teil ist Bool und der abhängige Teil macht aus dem Bool zwei verschiedene Typen (A und B)

bsp1 : Bool ×' ℕ                            -- bsp1 ist ein kartesisches Produkt aus Bool und ℕ
bsp1 true = true                            -- mit "true" im Argument spricht man den ersten "Faktor" an und setzt ihn auf "true" (Typ Bool)
bsp1 false = 5                              -- mit "false" im Argument spricht man den zweiten "Faktor" an und setzt ihn auf "5" (Typ ℕ)

Das λ { true → A ; false → B } steht hier für eine anonyme Funktion, in der die beiden Fälle für true und false verschiedene Ergebnisse nach sich ziehen. Im vorliegenden Fall liefert diese Funktion allerdings keine Werte zurück, sondern Typen.

Σ-Typen sind (geordnete) Paare, in denen der Typ des zweiten Elements vom ersten Element abhängt. In Agda wird das mit einem record modelliert.

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_                            -- Konstruktor durch _,_ (etwa: 1 , 2 oder true , 2)
  field
    proj₁ : A                                -- erstes Feld hat Typ A
    proj₂ : B proj₁                          -- zweites Feld hat Typ (B proj₁)

_×_ : Set → Set → Set                        -- kartesisches Produkt
A × B = Σ A λ _ → B                          -- ist ein Σ-Typ in dem der rechte Teil unabhängig vom linken ist 

bsp2 : Bool × ℕ
bsp2 = true , 5

Das λ _ → B steht hier für eine anonyme Funktion, deren einziger Parameter unberücksichtigt bleibt, was durch einen Unterstrich _ angezeigt wird. Die Felder proj₁ und proj₂ werden Projektionen genannt. Das hier definierte kartesische Produkt modelliert in der Curry-Howard-Korrespondenz die Konjunktion.

Während Π-Typen kartesische Produkte verallgemeinern, verallgemeinern Σ-Typen Summentypen bzw. disjunkte Vereinigungen.

data _⊎_ (A B : Set) : Set where -- disjunkte Vereinigung (oder Summe von A und B)
  inj₁ : A → A ⊎ B               -- A ⊎ B "ist ein" inj₁ mit Argument aus A oder 
  inj₂ : B → A ⊎ B               -- ein inj₂ mit Argument aus B

bsp1sum : Bool ⊎ ℕ
bsp1sum = inj₂ 5

bsp2sum : Σ Bool λ { true → Bool ; false → ℕ }
bsp2sum = false , 5

Die beiden Konstruktoren in _⊎_ werden Injektionen genannt. Die disjunkte Vereinigung modelliert in der Curry-Howard-Korrespondenz die Disjunktion oder das ausschließende Oder.

Π-Typen werden in der Curry-Howard-Korrespondenz für All-Quantoren verwendent und Σ-Typen für Existenzquantoren (wobei aber das was existiert auch tatsächlich angegeben werden muss).

ex-n-kleiner-gleich-3 : Σ ℕ (λ n → n ≤ 3)
ex-n-kleiner-gleich-3 = 2 , (s≤s (s≤s z≤n))

Hier steht im linken Teil des abhängigen Paares die Zahl deren Existenz man angenommen hat und im rechten Teil des Paares der Beweis, dass diese auch tatsächlich die Forderung erfüllt. Also "Es existiert eine natürliche Zahl n ≤ 3. Beweis: n = 2 mit (s≤s (s≤s z≤n)).".

alle-n-groesser-gleich-0 : Π ℕ (λ n → 0 ≤ n)  -- eigentlich (n : ℕ) → 0 ≤ n
alle-n-groesser-gleich-0 n = z≤n              -- wird schon durch einen Konstruktor abgedeckt

Hier steht eigentlich "Für alle $n\in \mathbb {N}$ gilt $0\leq n$. Beweis: durch Konstruktor z≤n."

Logik

In der Logik wird zur Definition der Negation der leere Typ (engl. Bottom) benötigt:

data ⊥ : Set where  -- keine Konstruktoren vorhanden

Dann kann man die Negation wie folgt als Abbildung einer Aussage auf Bottom auffassen. Denn falls man eine solche Abbildung findet, muss die Aussage A auch leer sein:

¬ : Set → Set  -- Negation macht aus einem Typ einen anderen Typen
¬ A = A → ⊥    -- Negation ist zu verstehen als "aus A folgt der leere Typ" (dann ist auch A leer und demzufolge logisch falsch)
infix 20 ¬     -- Negation hat Priorität 20

Nun kann man zur Formulierung logischer Aussagen entsprechend der Curry-Howard-Korrespondenz den Folgepfeil als Funktionspfeil definieren:

_⇒_ : Set → Set → Set
A ⇒ B = A → B          -- Folgepfeil = Funktionspfeil

Ein "genau dann, wenn" wird als kartesisches Produkt (UND-Verknüpfung) zweier Folgepfeile aufgefasst:

_⇔_ : Set → Set → Set
A ⇔ B = (A ⇒ B) × (B ⇒ A)  -- A gdw. B = (aus A folgt B) und (aus B folgt A)

Nun kann man logische Aussagen beweisen, denn Typen sind Aussagen und Beweise sind "Programme" (oder hier Funktionen):

id : {A : Set} → A ⇒ A  -- aus A folgt A
id = λ a → a            -- anonyme Funktion mit a : A als Parameter gibt a zurück

trivial : {A : Set} → A ⇔ A  -- (aus A folgt A) und (aus A folgt A)
trivial = id , id            -- Beweis durch Paar von id-Funktionen

aussage1 : {A B : Set} → (A ⇒ B) ⇒ (¬ B ⇒ ¬ A) -- (aus A folgt B) daraus folgt (aus nicht B folgt nicht A)
aussage1 A→B ¬B = λ a → ¬B (A→B a)

Man sieht, dass die Beweise durch typpolymorphe Funktionen gegeben sind. Implizit steht bei jeder Funktion dabei: Für alle Aussagen A bzw. für alle Aussagen A und B folgt .... id ist der Beweis der Aussage (des Funktionstyps) "Aus A folgt A". trivial ist durch den Pfeil in beide Richtungen ein kartesisches Produkt und muss in jedem Eintrag id enthalten. aussage1 ist interessanter: Hier wird ein logischer Schluss für beliebige Aussagen A und B bewiesen. Alle Argumente der Funktion aussage1 sind Voraussetzungen, um die man sich nicht kümmern muss. Aus diesen muss man den geforderten Ergebnistyp (hier Bottom) konstruieren.

• Zuerst kann man durch die Rechtsassoziativität des Folgepfeils die Klammern rechts weglassen.
• Dann kann man den mittleren Folgepfeil nach den Klammern von (A ⇒ B) als UND lesen (Beweis durch Schönfinkeln).
• Nun steht nur noch ein Folgepfeil da, nämlich der zwischen ¬ B und ¬ A.
• D.h. die Funktion (Schlussfolgerung) A→B und die Funktion ¬ B sind beide gegeben. Gesucht ist ein Element des Typs ¬ A.
• ¬ A ist eine Funktion von A auf ⊥, demzufolge muss man mit einer anonymen Funktion starten, die ein a : A als Argument hat.
• Nun muss man einen leeren Typen erzeugen. Die einzige Möglichkeit dazu ist, ¬ B zu nutzen.
• Das Argument von ¬ B ist vom Typ B, man hat allerdings nur ein a : A im Kontext.
• Demzufolge muss man die Funktion A→B mit a als Argument innerhalb von ¬ B aufrufen.

Beweise

Mit den vorhandenen Mitteln kann man zeigen, dass ≤ von oben eine Halbordnung ist:

refl≤ : (x : ℕ) → x ≤ x        -- Für alle x aus ℕ folgt x ≤ x  
refl≤ zero    = z≤n            -- Null: 0≤0 folgt aus z≤n 
refl≤ (suc x) = s≤s (refl≤ x)  -- Nachfolger: suc x ≤ suc x geht durch s≤s in x ≤ x über, wo man einfach refl≤ einsetzt  

trans≤ : {x y z : ℕ} → x ≤ y → y ≤ z → x ≤ z      -- Für alle x, y, z aus ℕ folgt aus x ≤ y und y ≤ z, dass x ≤ z  
trans≤       z≤n       y≤z = z≤n                  -- Fallunterscheidung in x ≤ y (Ziel: 0 ≤ z)
trans≤ (s≤s x≤y) (s≤s y≤z) = s≤s (trans≤ x≤y y≤z) -- Fallunterscheidung auch in y ≤ z (Ziel: suc x ≤ suc z)

In der zweiten Zeile bei trans≤ müssen die suc durch Verwendung von s≤s beseitigt werden, wobei x und z nur implizit in den Variablen x≤y und y≤z vorkommen. Ein erneuter Aufruf von trans≤ x≤y y≤z (Induktionsschritt) löst das Problem.

Damit ist gezeigt, dass ≤ erst einmal reflexiv und transitiv ist. Die Verwendung von s≤s im Nachfolger-Fall zusammen mit der Anwendung der Funktion (des Beweises) auf ein Argument ohne suc entspricht dem Induktionsschritt in der vollständigen Induktion. Es fehlt noch die Antisymmetrie. Diese braucht aber die Gleichheit zweier Ausdrücke.

Um Gleichheitsbeweise führen zu können, braucht man einen Gleichheitsbegriff. Die sog. propositionale Äquivalenz wird wie folgt definiert:

data _≡_ {A : Set} : A → A → Set where  -- homogene, zweistellige Relation
  refl : {a : A} → a ≡ a                -- ein Konstruktor, wenn links und rechts "das Gleiche" steht

Sie ist per Definition eine homogene, zweistellige Relation, reflexiv (Konstruktor) aber auch symmetrisch und transitiv:

sym≡ : {A : Set} {x y : A} → x ≡ y → y ≡ x  -- Für alle A und für alle x, y : A folgt aus x ≡ y, dass y ≡ x 
sym≡ refl = refl                            -- Einsetzen von refl macht aus x ≡ y ein x ≡ x und wird durch refl gelöst

trans≡ : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z  -- Für alle x, y, z aus A folgt aus x ≡ y und y ≡ z, dass x ≡ z
trans≡ refl y≡z = y≡z                                   -- Einsetzen von refl im ersten Argument fordert y ≡ z als Ziel

Daher ist sie eine Äquivalenzrelation und man kann mit ihr Gleichheitsbeweise führen (engl. equational reasoning). Einfaches Beispiel: Gesucht wird eine natürliche Zahl deren Nachfolger 3 ist:

n+1≡3 : Σ ℕ (λ n → suc n ≡ 3)
n+1≡3 = 2 , refl

Oder man kann das Assoziativgesetz der Addition natürlicher Zahlen beweisen. Dazu braucht man zuerst aber die Funktion cong (für engl. congruence) mit welcher man schlussfolgern kann, dass wenn x = y dann auch f x = f y.

cong : {A B : Set} {x y : A} → (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl

assoc-+ : (n m p : ℕ) → (n + m) + p ≡ n + (m + p)
assoc-+ zero m p = refl                             -- Ziel: m + p ≡ m + p Lösung: refl, weil 0 + n per Definition ≡ n ist
assoc-+ (suc n) m p = cong suc (assoc-+ n m p)      -- Ziel: suc ((n + m) + p) ≡ suc (n + (m + p)) Lösung: "cong suc"

Der Beweis erfolgt wieder durch Fallunterscheidung zwischen Null und Nachfolger. Im ersten Schritt kann man den Beweis per Reflexivität erbringen. Im zweiten Schritt in assoc-+ erfolgt der Beweis per Induktionsschritt. In beiden Fällen ist die Lösung deshalb so einfach, weil die Definition von _+_ einfach von Agda eingesetzt werden kann und zu den beiden einfachen Zielen führt. Hätte man eine Fallunterscheidung im zweiten oder dritten Argument vorgenommen, hätten etliche sym≡ und trans≡ miteinander "verschaltet" werden müssen.

Nun kann man auch die Antisymmetrie von ≤ zeigen:

antisym≤ : {n m : ℕ} → n ≤ m → m ≤ n → n ≡ m  -- Für alle n, m aus ℕ folgt aus n ≤ m und m ≤ n, dass n ≡ m 
antisym≤       z≤n       z≤n = refl
antisym≤ (s≤s n≤m) (s≤s m≤n) = cong suc (antisym≤ n≤m m≤n)

Hier wird der s≤s-Konstruktor auf der rechten Seite im Nachfolgerschritt durch cong suc ersetzt, da man eine Gleichung bekommt in der auf beiden Seiten suc steht.

Gleitkommazahlen, gebrochen rationale Zahlen und reelle Zahlen

In Agda gibt es auch die Möglichkeit mit Gleitkommazahlen zu arbeiten, die über die Standardbibliothek eingebunden werden können:

{-# OPTIONS --guardedness #-}
module wiki-floats where
open import IO
open import Data.Float using (Float ; _*_ ; _+_; atan2) renaming (show to showFloat)

x : Float
y : Float

x = 1.2
y = 5.7

main : Main
main = run do
  putStrLn ("Die Werte von x = " ++ (showFloat x) ++ " und y = " ++ (showFloat y))
  putStrLn ("ergeben die Summe x + y = " ++ (showFloat (x + y)))
  putStrLn ("und das Produkt x * y = " ++ (showFloat (x * y)) ++ ".")
  putStrLn ("Der Arcustangens von y/x = " ++ (showFloat (atan2 y x)) ++ ".")

Mit und über Gleitkommazahlen beweisbare Aussagen zu treffen ist aus verschiedenen Gründen schwierig. Als Beispiel sei nur genannt, dass sie weder Distributiv- noch Assoziativgesetz für Multiplikation und Addition erfüllen.

Agda bietet jedoch Implementierungen der ganzen Zahlen $\mathbb {Z}$ und der rationalen Zahlen $\mathbb {Q}$ über die Standardbibliothek an. Die Implementierung reeller Zahlen $\mathbb {R}$ erweist sich durch die intuitionistische Logik auch als schwierig.

Literatur

• Sandy Maguire (2023). Certainty by Construction
• Phil Wadler, Wen Kokke, and Jeremy G. Siek (2019). Programming Languages Foundations in Agda