Tutorium 10

Gruppen 5 und 7
Samuel Teuber
propa@teuber.dev
https://teuber.dev/propa

Übungsblätter

• Fragen?
• Probleme?
• Zu schwierig?

Übungsblatt 9: Abgabe diesen Donnerstag (9.1.)!

Klausur

Die Klausur findet am Dienstag, 24.03.2020 statt.
Anmeldung wohl ab heute

Bemerkung zu Lambda Kalkül

Jeden Reduktionsschritt einzeln?

• Solange nachvollziehbar: Mehrere Schritte auf einmal in Ordnung!
• Wichtig:
  • Bei Beweis, dass man X auf Y reduzieren kann nicht mit X => Y arbeiten
  • =>* nutzen (entweder immer oder wo tatsächlich notwendig!)

Reprise: Unifikation

Was war nochmal...

Substitution?

$$ \sigma = \{X_2⇨X_1\}\\ \sigma\left(\ f\left(X_1, Y\right)=X_2\ \right) = f(X_1, Y)=X_1 $$

Wie wird Substitution ausgeführt?

Einmalig, überall, gleichzeitig

Gleichungssysteme?

$$ f(X_1,X_2,X_3) = f(A,B,C)\\ X_2=C $$

Unifikator?

$$ \{X_1⇨A, X_2⇨C, X_3⇨C, B⇨C\} $$

Most General Unifier?

Wir nennen $\sigma$ den most general unifier (mgu), wenn...

...für alle Unifikatoren $\gamma$ gilt...

...es gibt einen zugehörigen Unifikator $\theta$, sodass...

$$ \gamma = \theta \circ \sigma $$

Robinson Algorithmus?

$$ C = \{\\ X_1 = f(X_2, X_3),\\ X_3 = g(X_4, X_5),\\ X_3 = g(X_7, X_5),\\ X_4 = X_5\\ \} $$

Typinferenz ohne Let

Veränderte Strategie:

• Konstruiere "Skelett" des Herleitungsbaums
  • Gleiche Regeln
  • Frische Variablen für Voraussetzungen
• Sammle Gleichungen, die erfüllt sein müssen
• Bestimme mgu des Gleichungssystems

Typinferenz mit Let

1. Berechne zunächst mgu $\sigma_{let}$ für Constraints aus linken LET Teilbaum ($C_{let}$)
2. Berechne $\tau = ta(\sigma_{let}(\tau_1),\sigma_{let}(\Gamma))$
3. Berechne rechten LET Teilbaum mit $\sigma_{let}(\Gamma) \cup \{f:\tau\}$

Typinferenz mit LET