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.
System F
In der Vorlesung haben wir den List a folgendermaßen definiert:
List a = ∀r . r → (a → r → r) → r
nil = λuf . u
cons = λ x l u f . f x ( l u f )
Verstehe ich das richtig, dsss List a eine Funktion bekommt, die nil auswertet, und eine, die cons auswertet?
Kann jemand den Lambda-Ausdruck für cons erklären?
Ja, das ist so in etwa eine der möglichen Anschauungen. Genauer: jedes f vom Typ List a, bekommt eine funktion, die sich wie nil verhalten soll und eine, die sich wie cons verhalten soll. Soll heißt in diesem Fall, dass sie sich auch anders verhalten könnte, um etwas bestimmtes aus der Liste zu berechnen.
Die alternative Anschauung ist: Man übergibt einer Liste die einzelnen Fälle des Pattern-Matchings. Der erste Parameter (vom Typ r) beschreibt den Basisfall. Der zweite Parameter vom Typ (a → r → r) beschreibt den rekursiven Schritt, der zur Berechnung des Ergebnisses zwei Werte zu Verfügung hat: Zum einen das aktuelle Head-Element (vom Typ a) und zum anderen das Ergebnis des Rekursiven Aufrufs (vom Typ r).
Evtl. hilft schon das:
nil = λ nil_case cons_case . nil_case
cons = λ head tail . λ nil_case cons_case . cons_case head (tail nil_case cons_case)
Edit: In deiner Frage solltest du auch noch etwas Notation nachbessern. Die Gleichheit von Typen beschreibt man mit:
List a = ∀r . r → (a → r → r) → r
D.h. Der Typ List a ist gleich dem Typen ∀r . r → (a → r → r) → r.
Jedoch bedeutet der Doppelpunkt — z.B. in f : α — dass der λ-Ausdruck f vom Typ α ist.
Verbessert.
Vielen Dank für die Erklärung. So ist es schon klarer 
Das (tail nil_case cons_case) am Ende ist dann quasi der rekursive Aufruf, oder?
Wie zeigt man nun, dass |- nil : ∀a . List a ?
Zuerst wendet man (∀i) an und setzt den Term für nil ein: λ u f . u : List a
Aber wie geht es weiter? Die einzige Regel mit einem Lambda setzt λ x . s : α → β voraus, aber wir haben ja List a statt zwei Typen α und β?
List a ist nur eine kurzschreibweise für ∀r . r → (a → r → r) → r. D.h. wenn du passend (∀i) anwendest hast du einen Funktionstyp (dessen Konklusion β weider ein Funktionstyp ist).
Bei Teilaufgabe 2 sind wir in der Übung auf die Lösung
length = \ l . l zero ( \ x l . succ l )
->_beta \ l . l zero ( \ x. succ )gekommmen, die mir nicht einleuchtet.
Was bedeutet der Ausdruck im einzelnen und wie kommt man darauf?
Kann jemand eine Lösung von die Teilaufgaben 3 und 4 bereitstellen?
ein Objekt vom Typ List a ist ja eine Funktion, die einen “Startwert” s vom Typ r, und eine Funktion f von a \times r nach r nimmt (wobei diese Funktion natürlich gecurryt ist, also Typ a->r->r hat)
seien leereListe und einsZweiDrei=Cons 1 (Cons 2 (Cons 3 Nil)) = [1,2,3] beide vom Typ List Nat
Listen sind ja so gebaut, dass z.B. folgendes gilt:
leereListe s f = s
einsZweiDrei s f = f 1 (zweiDrei s f) = … = f 1 (f 2 (f 3 s))
also im Prinzip folgende fold-Operation:
foo = start; // foo hat den Typ r
for elem in liste { // elem hat den Typ a
foo = f (elem, foo);
}
return foo;die length-funktion nimmt jetzt ihre Eingabeliste, und wirft ihr als Startwert “zero” entgegen (Länge der leeren Liste ist 0), und gibt ihr noch eine funktion (\ x y . succ y) mit.
im obigen Beispiel also:
int start = 0;
int f (int elem, int foo) {
return foo+1; // ignore the elem parameter
}Ich hoffe das hilft ein wenig 
join sieht so oder so ähnlich (bis auf Reihenfolge falsch oder so) aus:
join = \ L . L (Nil) (\ elem accu . append (elem) (accu))Hier bekommt L (was ja ein List List a ist) als Startwert die “leere Liste (Nil)”, und die Funktion f hier nimmt ein elem vom Typ List a, und einen accu vom Typ List a, und konkateniert die beiden.
append geht im Prinzip genauso, ist mir jetzt aber zu eklig, das ausm Kopf hinzuschreiben
Hoffe, das hilft
Vielen Dank 
Mit deiner Erklärung bin ich auf das gleiche Ergebnis für join gekommen.
Diese beta-Reduktion kann ich nicht nachvollziehen. Setzt man bei beta-Reduktion nicht was für eine “Lambda-Variable” ein und hier verschwindet das l einfach?
length = \ l . l zero ( \ x l . succ l )
->_beta \ l . l zero ( \ x. succ )Wie wärs mit folgendem für append?
append = \ L1 L2 . L1 L2 ( \ x y . cons x y )Ich weiß nicht, ob das wirklich eine beta-Reduktion ist, aber \ x l . succ l ist äquivalent zu \ x . succ.
Bsp.:
(\ x l . succ l) f n ->_beta (\ l . succ l) n ->_beta succ n
(\ x . succ) f n ->_beta succ n
EDIT: Okay, ich kann nicht wirklich garantieren, das korrekt ist, was ich da sag. Ist nur meine Erklärung, wie die zitierte Lösung zu verstehen ist.
vorsicht, afaik ist das nämlich eben nicht äquivalent, auch wenn es sich sehr oft (und für unsere momentanen Zwecke) gleichartig verhält.
Das was du hier tust, kann man in dem Fall schon machen, und es wird – glaube ich – funktionieren. der ->_beta-Pfeil ist dort aber auf jeden Fall falsch, denn das ist ja keine Anwendung. Da steht einfach nichts zum anwenden.
UPDATE: eta-(η)-Umformung heißt das anscheinend.
1 „Gefällt mir“
Hab ich genauso.
Und für Join:
join=\ L . L nil (\ cur cs. append cur xs)