Frage applikative Reduktion

Bachelor Theorie der Programmierung
1

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

2

Frage applikative Reduktion
Hallo Zusammen,

kann mir jemand beantworten ob folgende applikative Reduktion richtig wäre und wenn falsch wie Sie richtig ginge?

Applikative Reduktion nach Regeln der Vorlesung:
geq [2] [1] → Regel 4 (delta)
geq λf a.f(f a) [1] → Regel 4 (delta)
geq λf a.f(f a) λf b.f b->Regel 3 (delta)
isZero (λf a.f(f a) pred λf b.f b) ->Regel 3 (delta)
isZero (λf a.f(f a) fst(λf b.f b ( λp.pair(snd p) (succ(snd p))) (pair [0] [0])))

Regeln für applikative Reduktion aus Vorlesung:

  1. (λx. t)s ->a t[s/x], wenn t und s normal sind.
  2. λx. t ->a λx. t’, wenn t ->a t’.
  3. ts ->a t’s, wenn t ->a t’ und s normal ist.
  4. ts ->a ts’, wenn s ->a s’.
3

Hallo,

hier hat sich gleich mal ein Fehler im ersten Schritt eingeschlichen, Stichwort Klammerung. Siehe z.B. den Abschnitt “Zur Notation” auf Übungsblatt 4. Die letzte Umformung ist dann auch diesem Fehler zum Opfer gefallen. Am besten mal zur Übung explizit Klammern setzen!

Grüße
Christoph

4

wie hätte die umformung hier dann entsprechend aussehen müssen und wie sähen hier die klammern aus wenn man sie setzen würde?

ich hatte gedacht, dass die applikative reduktion entsprechend von innen nach außen arbeitet und die argumente einer funktion zuerst ausgewertet werden - hier also [2] und [1]
Klammerung hätte ich gedacht wäre wie folgt geq ([2] [1])

5

Nein, die Klammerung ist eben (geq [2]) [1]. Denn („Zur Notation“, Übungsblatt 4):

Ebenso ist dann in der vorletzten Zeile ((λf a.f(f a) pred) λf b.f b) zu klammern.

6

War aber der Schritt richtig, dass zuerst die Definition von [2] eingesetzt wurde, oder hätte man zuerst [1] auflösen müssen?

7

wäre folgende Reduktion entsprechend richtig?

geq [2] [1] → Regel 4 (delta)
geq [2] λf b.f b → Regel 4 (delta)
geq λf a.f(f a) λf b.f b ->Regel 3 (delta)
isZero (λf a.f(f a) pred λf b.f b) → (beta)
isZero (λ a.pred(pred a) λf b.f b)

welche Regel sollte beim letzen Schritt zum einsatz kommen?

Regeln für applikative Reduktion aus Vorlesung:

  1. (�λx. t)s ->a t[s/x], wenn t und s normal sind.
  2. λ�x. t ->a λ�x. t’, wenn t ->a t’.
  3. ts ->a t’s, wenn t ->a t’ und s normal ist.
  4. ts ->a ts’, wenn s ->a s’.
8

Die Aufgabe ist unterspezifiziert, deswegen kann es hier keine “richtige” Reduktion geben. Wie ist denn “geq” definiert? Es gibt hier mehrere Möglichkeiten:

geq = λn m . isZero (n pred m)
geq n = λm . isZero (n pred m)
geq n m = isZero (n pred m)

Siehe zu diesem Unterschied Übungsblatt 4, Aufgabe 2.2.