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.
Braindump SS14
Anbei und ganz frisch geTeXt. Viel Erfolg allen! Vielleich kann die ja jemand in die Prüfungen aufnehmen.
Attachment:
ThProg-SS14-Braindump.pdf: https://fsi.cs.fau.de/unb-attachments/post_138652/ThProg-SS14-Braindump.pdf
1 „Gefällt mir“
Aufgabe 1.2
Hey, ich wollte mal fragen, ob mein Lösungsansatz korrekt ist.
l1 = x⇑(y⇓z)
l2 = x’⇑(y’⇓z’) σ = [ x’/x, (y’⇓z’)/y ]
l1σ = x'⇑((y'⇓z')⇓z)
(1)↓ ↓(2)
(z⇓x') ⇑ (y'⇓z') (((y'⇓z')⇓z) ⇓ ((y'⇓z')⇓z)) ⇓ x'
(2)↓
((y'⇓z')⇓(y'⇓z')) ⇓ (z⇓x')
=> Das k.P. ist nicht zusammenführbar => das System ist nicht konfluent.
Ich bin der Meinung man darf hier im ersten Schritt nicht eine andere Regel anwenden, als die, die man für das kritische Paar verwendet. Um ein kritisches Paar von l1 = Regel 1 und l2 = Regel 1 zu finden, müsste man den Term derart aufstellen, dass sich die Regeln irgendwie „überlappen“. Dann kann auf den Term zwei mal auf unterschiedliche Weise die Regel 1 angewendet werden. Aber da man hier kein gültiges Sigma findet, sodass dies gilt, gibt es wohl kein kritisches Paar mit diesen Regeln.
Mein Ansatz für diese Aufgabe wäre so:
l1 = x⇑(y⇓z)
l2 = x’⇑ y’ σ = [ x’/x, y’/y ]
l1σ = x'⇑(y'⇓z)
(1)↓ ↓(2)
(z ⇓ x') ⇑ y' ((y'⇓z) ⇓ (y'⇓z)) ⇓ x'
(2)↓
(y'⇓y') ⇓ (z ⇓ x')
=> Das kritische Paar ist nicht zusammenführbar => System ist nicht lokal konfluent → System ist nicht konfluent
Ich hätte auch gleich eine Frage für die Aufgabe 2.1b), die applikative Reduktion: Ist der erste Schritt so richtig? So hätte ich die applikative Reduktion verstanden, allerdings sieht das ziemlich falsch aus.
geq (λfa. f(f a)) (λfa. f a)
→ geq (λa. (λfa. f a)(((λfa. f a) a))
geq (λfa. f(f a)) (λfa. f a)
Beachte, dass Applikation im Lambda-Kalkül linksassoziativ ist, d.h. geq (λfa. f(f a)) (λfa. f a) ist implizit wie folgt geklammert: (geq (λfa. f(f a))) (λfa. f a)
1 „Gefällt mir“
Meine Lösung wäre für die applikative Reduktion:
geq 2 1
δ> isZero (2 pred 1)
=isZero( (λfa.f(fa) pred) 1)
β> isZero( (λa.pred(pred a) 1)
β> isZero( pred(pred1))
δ> Das unterstrichene pred ausschreiben
Normale Reduktion:
geq 2 1
δ> isZero (2 pred 1)
δ>(2 pred 1) (λx.false) true
=(u pred[/u] 1) (λx.false) true
β>((λa.pred(pred a)) 1) (λx.false) true
β>(pred(pred 1)) (λx.false) true
Edit: Verbesserung von Ferron eingebaut, 1 ist in der Klammer 
Die normale hab ich auch so. Allerdings gehört bei deiner Lösung die 1 mit in die Klammer.
Aber Zitat aus dem Skript:
• (Lambda x. t)s ->a t[s/x], wenn t und s normal sind.
• Lambda x. t ->a Lambda x. t’, wenn t ->a t’.
• ts->a t’s, wenn t->a t’.
• ts->a ts’, wenn s->a s’ und t normal ist.
Müsste ich demzufolge nicht
β> isZero( (λa.pred(pred a)) |1|
als nächstes reduzieren?
Denn die dafür nötige Delta-Reduktion steht nach obiger Prioliste an Platz 2 und vor Reduktion der Argumente.
Oder ist das Problem hier, dass a noch keinen konkreten Wert hat und ich daher erst wie du die Beta-Red machen muss?
Hier kurz mit den Definitionen (wie ich sie verwendet habe):
Definieren wir
t:=isZero
s:=( (λa.pred(pred a) 1)
So müssen wir nach Regel 4 zuerst s auswerten.
Definieren wir nun
λx.t := λa.pred(pred a)
s := 1
Dann können wir Regel 1 anwenden und erhalten somit mein obiges Ergebnis “isZero( pred(pred1))”.
Soweit ich es verstanden habe muss man immer die Regeln von oben nach unten durchgehen und die erste die passt auch verwenden.
Demnach kommen wir gar nicht zu Regel 2, da wir direkt Regel 1 anwenden konnten.
Regel 1 hat bei applikativ aber noch den Zusatz „wenn s und t normal sind“.
Da t := pred(pred a), können wir t applikativ noch 2x delta-reduzieren und somit ist es noch nicht normal.
Demzufolge müssten wir erst das innerste „pred a“ delta-reduzieren.
So mein Gedankengang.
Außer natürlich man kann pred(pred a) noch nicht delta-reduzieren weil das a noch nicht bestimmt wurde.
Bedeutet die Applikative Reduktion nicht dass man “evaluate arguments before the function itself”
D.h. geq 2 1 ->??? geq ((ƛfa.f(fa)) 1) → … dann weiß ich net, wenn man Betta-Reduktion durchführt, dann wird das zweite Argument für geq fehlen oder? … → geq ((ƛa.1(1a)) → ?
@Hoschi, danke für die Erklärung
Siehe die Nebenbemerkung zur A2.1
" wir sehen |n| (anders als in der Probeklausur) hier als direkte repräsentation der entsprechenden Lambda-Terme. D.h. |1| = Lambda fa.fa .
Daher kann man hier die |2| und |1| nicht erst delta-reduzieren wie die vorschlägst.
Wäre es hingegen wie in der Probeklausur hättest du Recht, man müsste erst 2 dann 1 delta-reduzieren, und dann das geq.
Vorsicht, siehe
Du darfst hier definitiv nicht die 1 in den lambda-term der 2 beta-reduzieren!
1 „Gefällt mir“