Gleichungslogik und Lambda-Kalkül

Worum geht's

Du lernst die Grundlagen von Gleichungslogik, Termersetzungssystemen und untypisiertem sowie typisiertem Lambda-Kalkül. Am Ende kannst du Semantik und Beweissysteme der Gleichungslogik anwenden, Termrewrites auf Korrektheit (Terminierung, Konfluenz) analysieren und Lambda-Terme sowohl programmieren als auch typisieren.

Was du danach kannst

• Konfluenz und Terminierung abstrakter Reduktionssysteme beweisen
• Gleichheiten mittels Rewriting und Gleichungslogik beweisen
• Semantik der Gleichungslogik definieren und zur Widerlegung von Gleichheiten nutzen
• Konfluenz und Terminierung einfacher Rewritesysteme nachweisen
• Eigenschaften des Lambda-Kalküls (z. B. Konfluenz, Terminierung) beweisen
• Berechenbare Funktionen als untypisierte Lambda-Terme ausdrücken
• Typen für untypisierte Lambda-Terme ableiten
• Typed Lambda-Terme und Beweise ineinander überführen

Aus was das Modul besteht

• VorlesungVermittlung der Theorie im dialogischen Vortrag
• Übung/TutoriumBearbeitung von Übungsaufgaben einzeln oder in Gruppen mit Tutorunterstützung

Lehrmethode

• Vortrag/FrontalunterrichtErklärung und Darstellung des Materials im Rahmen der Vorlesung
• Übungsaufgaben mit TutorunterstützungAnwendung und Vertiefung des Vorlesungsstoffs, größtenteils schriftlich, teils computerbasiert