Index of /~oc45ujef/thprog/agda

[ICO]NameLast modifiedSizeDescription
[PARENTDIR]Parent Directory  -  
[TXT]ue7.agda2024-06-25 14:48 1.3K 
[TXT]ue5.agda2024-06-03 10:33 1.0K 
[TXT]more.agda2024-05-23 10:30 2.1K 
[TXT]klausur.agda2024-07-15 14:51 3.3K 
[TXT]intro.agda2024-05-16 14:03 2.3KEine erste Einführung
[TXT]bs.agda2024-10-09 20:53 1.6K 
The Agda logo

Da die reguläre Übung erst um anfängt, nutze ich die Zeit um wöchentliche Einführungen zur Programmiersprache Agda zu geben. Agda ist keine notwendige Voraussetzung für die ThProg-Vorlesung, wohl aber ein nützliches Werkzeug um Intuition für Induktion, Koinduktion und λ-Kalkül zu entwickeln

Agda-Einführung statt Übung

Da aufgrund der Bergkirchweih in dieser Woche kein Präsenzaufgabenblatt bereitgestellt wird, ist die Übung am vollends Agda gewidmet. Wen das interessiert kann gerne kommen (auch gerne Leute die regulär nicht in meine Übung gehen).

Wann?

Donnerstag, von

Wo?

02.133-113

Warum?

Agda ist eine funktionale Programmiersprache mit starken Ähnlichkeiten zu Haskell. Als solche basiert sie auf dem λ-Kalkül, was ja später ein größeres Thema in ThProg sein wird. Mit induktiven und koinduktiven Datentypen können auch die entsprechenden Kapitel der Vorlesung nachgebaut werden. Als stark normalisierendes λ-Kalkül mit Dependent Types kann Agda auch als Beweisassistent (ähnlich zu Coq) verwendet werden.

Ein Vorgeschmack

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

_+_ : Nat → Nat → Nat
zero + m = m
suc n + m = suc (n + m)

+-idₗ : ∀ (n : Nat) → n ≡ n + zero
+-idₗ zero = refl
+-idₗ (suc n) = cong suc (+-idₗ n)

+-suc : ∀ (n m : Nat) → n + (suc m) ≡ suc (n + m)
+-suc zero m = refl
+-suc (suc n) m = cong suc (+-suc n m)

+-commutative : ∀ (n m : Nat) → n + m ≡ m + n
+-commutative zero m = +-idₗ m
+-commutative (suc n) m =
  trans (cong suc (+-commutative n m))
        (sym (+-suc m n))

Ressourcen