Algebra des Programmierens - Cheatsheet

Theorie der formalen Sprachen und Automaten

Definition:

Formale Sprachen und Automaten sind grundlegende Konzepte zur Beschreibung und Analyse von Berechnungsprozessen und Programmiersprachen.

Details:

• Formale Sprache: Menge von Wörtern über einem Alphabet.
• Alphabet: Endliche Menge von Symbolen, zum Beispiel \(\Sigma\).
• Grammatik: Regelmenge zur Erzeugung von Wörtern einer formalen Sprache.
• Chomsky-Hierarchie: Klassifikation von Grammatiken (Typ 0 bis Typ 3).
• Automaten: Modelle zur Erkennung formaler Sprachen, z.B. DFA, NFA.
• DFA (Deterministischer endlicher Automat): Endlicher Automat mit eindeutigen Übergängen pro Symbol.
• NFA (Nichtdeterministischer endlicher Automat): Endlicher Automat mit möglichen mehreren Übergängen pro Symbol.
• Reguläre Ausdrücke: Beschreiben reguläre Sprachen; Äquivalent zu DFA und NFA.
• Pumpinglemma: Hilfsatz zur Überprüfung der Zugehörigkeit zu regulären Sprachen.

Polynomfaktorisierung und algebraische Algorithmen

Definition:

Techniken zur Zerlegung von Polynomen in ihre irreduziblen Faktoren unter Einsatz effizienter algebraischer Methoden.

Details:

• Polynom-Faktorisierung: \textbf{f(x)} in Produkt irreduzibler Polynome zerlegen.
• Algebraische Algorithmen: Schnelle Berechnungsverfahren nutzbar in Computer-Algebra-Systemen.
• Schlüsseltechnik: Berlekamp’s Algorithmus, Zassenhaus’s Algorithmus, Lenstra–Lenstra–Lovász (LLL) - Algorithmus.
• Berlekamp’s Algorithmus: Nutzt Matrixreduktion und Linearkombinationen über endlichen Körpern.
• Zassenhaus: Kombiniert Hensel-Lifting und rekursiven Faktorisierung.
• LLL: Wendet reduktion in Gitter an um Faktoren zu finden.
• Typische Anwendung: Kryptographie, Codierungstheorie, symbolische Berechnungen in CAS.
• Softwarebeispiele: Maple, Mathematica, SAGE.

Formale Spezifikation und Verifikation

Definition:

Formale Methoden zur Beschreibung und Überprüfung von Software; notwendig für korrekte Programme.

Details:

• Formale Spezifikation: Mathematische Beschreibung von Software.
• Ziel: eindeutige und präzise Definitionen.
• Verifikation: Beweis, dass Software den Spezifikationen entspricht.
• Nutzung von Logik, Beweisen, und formalen Systemen.
• Wichtige Werkzeuge: Z3, Coq, Isabelle.
• Treffen auf Korrektheit, Konsistenz und Vollständigkeit.

Komplexitätstheorie algebraischer Algorithmen

Definition:

Analyse der Effizienz algebraischer Algorithmen unter Berücksichtigung ihrer Berechnungsressourcen, hauptsächlich Laufzeit und Speicher.

Details:

• Bestimme die Komplexität bezüglich der Eingabegröße (häufig n).
• Wichtige Klassen: P, NP, #P für algebraische Probleme.
• Algorithmen Beispiel: Polynom-Multiplikation, Faktorisierung von Polynomen.
• Wichtige Maßzahlen: Zeitkomplexität (T(n)), Speicherkomplexität (S(n)).
• Reduktionen und Vollständigkeit: z.B. Transformation eines Problems in ein anderes, um Komplexität zu vergleichen.
• Spezifische Methoden: Schnell-Fourier-Transformation (FFT), Strassens Algorithmus für Matrixmultiplikation.

Beweis über Programmeigenschaften

Definition:

Beweis über Programmeigenschaften verifiziert, dass Programme erwartete Eigenschaften erfüllen.

Details:

• Aussagenlogik und Prädikatenlogik zur Formulierung von Eigenschaften benutzen
• Schleifeninvarianten und Schleifenvarianten zur Beweisführung von Schleifen
• Modellprüfung (model checking) zur automatisierten Verifikation
• Formale Spezifikation als Basis für Beweis
• \textbf{Korrektheitsbeweis} durch partielle und totale Korrektheit:
• \textbf{Partielle Korrektheit:} Programm liefert korrekten Output für gültige Inputs
• \textbf{Totale Korrektheit:} Programm terminiert und liefert korrekten Output

Funktionale Programmierung

Definition:

Programmierung mit Funktionen als erste Klasse, unveränderliche Daten und reiner Funktionen.

Details:

• Keine Seiteneffekte
• Hauptkonzepte: Funktionen höherer Ordnung, anonyme Funktionen, currying
• Typische Funktionen: map, filter, reduce
• Beispiel: \texttt{map (\x -> x + 1) [1, 2, 3] = [2, 3, 4]}

Erstellung und Analyse von Graphen

Definition:

Erstellung und Analyse von Graphen befasst sich mit der Konstruktion, Darstellung und Untersuchung von Graphenstrukturen.

Details:

• Knoten (Vertices) und Kanten (Edges)
• Gerichtete und ungerichtete Graphen
• Adjazenzmatrix und Adjazenzliste zur Darstellung
• BFS (Breitensuche) und DFS (Tiefensuche) zur Traversierung
• Kurzeste-Wege-Algorithmen: Dijkstra, Bellman-Ford
• Minimal-Spanning-Tree: Prim, Kruskal
• Zusammenhangskomponenten
• Erkennungsalgorithmen für Zyklen

Automatisierung von Beweisen

Definition:

Automatisierung von BeweisenEinsatz von Software-Werkzeugen zur automatischen Verifikation mathematischer Beweise oder Programme.

Details:

• Wichtige Werkzeuge: Theorembeweiser (z.B. Coq, Isabelle)
• Prinzip: Formale Spezifikation -> Maschinelle Ableitung von Beweisen
• Ziel: Fehlerreduktion, Zeitersparnis, Erhöhung der Verlässlichkeit
• Einschränkungen: Komplexität der Beweise, notwendige formale Modellierung
• Relevante Methoden: Resolution, SAT-Solver, SMT-Solver
• Beispiele: Verifikation von Algorithmen, Sicherheitsprotokollen