Funktionale Programmierung und Verifikation - Cheatsheet.pdf

Erstklassige Bürger in funktionalen Programmiersprachen

Definition:

Erstklassige Bürger (First-Class Citizens) sind Entitäten, die in der Sprache wie jede andere behandelt werden.

Details:

• Können als Argumente an Funktionen übergeben werden
• Können von Funktionen zurückgegeben werden
• Können in Variablen gespeichert werden
• Häufige Anwendung: Funktionen als erstklassige Bürger

Immutabilität und ihre Bedeutung

Definition:

Unveränderlichkeit von Datenstrukturen nach ihrer Erzeugung.

Details:

• Sicherstellung der Zustandskonsistenz
• Einfachere Nebenläufigkeit und Parallelität
• Erleichtert Debugging und Testen
• Reduziert Seiteneffekte
• -Funktionale Programmierung: Unveränderliche Datenstrukturen und reine Funktionen fördern

Rekursionsprinzip und seine Anwendungen

Definition:

Rekursionsprinzip ist eine Methode, bei der eine Funktion sich selbst aufruft, um Probleme zu lösen.

Details:

• Basisfall: \textit{stoppt die Rekursion} und gibt ein direktes Ergebnis zurück.
• Rekursiver Fall: Funktion löst ein kleineres Teilproblem und verwendet dessen Lösung zur Lösung des Gesamtproblems.
• Anwendungsbeispiele:
  • Summe einer Liste: \textit{sum(lst) = lst[0] + sum(lst[1:])}
  • Fakultät: \textit{n! = n * (n-1)!}
  • Fibonacci-Folge: \textit{fib(n) = fib(n-1) + fib(n-2)}

Musterabgleich (Pattern Matching) in funktionalen Datenstrukturen

Definition:

Technik zur Analyse und Dekonstruktion von Datenstrukturen durch direktes Vergleichen ihrer Form und Werte.

Details:

• Ermöglicht sauberes und prägnantes Kodieren komplexer Anweisungen.
• Wird oft in Funktionsdefinitionen eingesetzt: funktionsname x :: xs = ...
• Kann einfache Werte, Listen, und komplexe Datentypen handhaben.
• Vermeidet explizite Umkehrungen und Abfragen durch If-/Else-Konstrukte.
• Beeinhaltet Wildcards und Named Patterns für flexible Muster.

Höhere Ordnungsfunktionen (Map, Filter, Reduce)

Definition:

Höhere Ordnungsfunktionen sind Funktionen, die andere Funktionen als Argumente nehmen oder zurückgeben.

Details:

• Map: Wendet eine gegebene Funktion auf jedes Element einer Liste an und gibt eine neue Liste zurück. Beispiel: \texttt{map(f, [x1, x2, ..., xn])} ergibt \texttt{[f(x1), f(x2), ..., f(xn)]}.
• Filter: Wendet eine Bedingungsfunktion auf eine Liste an und gibt eine Liste derjenigen Elemente zurück, die die Bedingung erfüllen. Beispiel: \texttt{filter(p, [x1, x2, ..., xn])} ergibt \texttt{[x_i | p(x_i)]}.
• Reduce (Fold): Aggregiert die Elemente einer Liste mittels einer binären Funktion und einem Anfangswert. Beispiel: \texttt{reduce(f, [x1, x2, ..., xn], init)} ergibt \texttt{f(...f(f(init, x1), x2)..., xn)}.

Lambda-Kalkül: Alpha-Konversion und Beta-Reduktion

Definition:

Alpha-Konversion: Umbenennung gebundener Variablen um Namenskonflikte zu vermeiden. Beta-Reduktion: Anwendung von Funktionen auf Argumente, d.h. Substitution der Argumente in den Funktionsterm.

Details:

• Alpha-Konversion: \(\lambda x. f(x) \, \rightarrow \, \lambda y. f(y)\)
• Beta-Reduktion: \( (\lambda x. x^2)(3) \, \rightarrow \, 3^2 \, \rightarrow \, 9 \)
• Reduktionsstrategie wählbar: normal-order oder applicative-order
• Konversion und Reduktion sind essenziell für die Evaluation in funktionalen Programmiersprachen

Typinferenzmechanismen in typisierten Sprachen

Definition:

Techniken zur automatischen Bestimmung von Typen in Programmen ohne explizite Typdeklarationen.

Details:

• Ziel: Verbesserung der Code-Kompaktheit und Fehlererkennung
• Bekannte Algorithmen: Hindley-Milner, Damas-Milner
• Einfacher: Typableitung durch rekursive Analyse der Ausdrücke
• Komplexer: Constraint-gestützte Algorithmen zur Typinferenz
• Praktische Anwendung: viele funktionale Sprachen wie Haskell und OCaml
• Hindley-Milner: Besonders effektiv bei polymorphen Typen
• Beispiel: Variablen müssen nicht explizit deklariert werden; Typ wird automatisch abgeleitet
• \texttt{let x = 3} wird automatisch als \texttt{x: Int} abgeleitet

Formale Spezifikationen und Modellchecking

Definition:

Formale Spezifikationen: Mathematische Beschreibung eines Systems. Modellchecking: Automatisches Verifizieren, ob ein Modell eine Spezifikation erfüllt

Details:

• Formale Spezifikation: Nutzung mathematischer Notationen zur präzisen Beschreibung von Systemen
• Modelle: Abstrakte Darstellungen von Systemen
• Modellchecker: Tools wie SPIN, NuSMV
• Hauptziel: Fehler frühzeitig in der Entwicklungsphase finden
• Eigenschaftsspezifizierung mittels temporaler Logiken wie LTL (\textit{Linear Temporal Logic}) oder CTL (\textit{Computation Tree Logic})
• Ergebnisse: Bestätigung der Korrektheit oder Gegenbeispiele bei Fehlern