Ich lerne gerade Haskell und nehme auch an einem eher theoretischen Vortrag über funktionale Programmierung an der Universität teil.
Ich weiß, dass dies eine rein theoretische / akademische Frage ist, aber ich bin dennoch daran interessiert, verschiedene einfache Funktionen einfach mit reinem Lambda-Kalkül (d. h. ohne definierte Konstanten) auszudrücken.
Einige Vorlesungsmaterialien von mir definieren die booleschen Werte wie:
Wahr = \ xy.x
Falsch = \ xy.y
(\ bezeichnet das Lambda-Symbol)
Wenn sie wie diese Selektorfunktionen definiert sind, kann die if-Bedingung einfach wie folgt definiert werden:
If = \ x.x
Jetzt versuche ich eine kurze Form für die logische "und" -Funktion zu finden. Meine erste Vermutung ist:
und = \ xy. {( If x) [( If y) Wahr Falsch ] Falsch }
Also im Grunde würde diese Lambda-Funktion zwei Argumente u v erhalten, bei denen beide wie Wahr / Falsch eingegeben werden müssen. Wenn ich verschiedene Beta-Reduktionen mit allen 4 Kombinationen der Logiktabelle mache, bekomme ich das richtige Ergebnis.
Trotzdem sieht diese Funktion ein wenig hässlich aus und ich denke darüber nach, es eleganter zu machen. Irgendwelche Vorschläge hier?
Wir können Ihre Antwort nur reduzieren, um einen dickeren zu erhalten.
Zuerst ein paar Aufwärmübungen. Offensichtlich IF x ==> x , und als TRUE TRUE FALSE ==> TRUE und FALSE TRUE FALSE ==> FALSE , wenn x ein boolescher Wert ist als x TRUE FALSE ==> x .
Jetzt reduzieren wir
%Vor%und dieser Ausdruck funktioniert immer noch mit Wahrheitstabellen
%Vor% Nun, and True ist die Identity-Funktion und and False ist die konstante Funktion, die False zurückgibt, also können wir das verwenden.
was eine schöne Symmetrie mit
hat %Vor%(wo
%Vor%)
Das allgemeine Muster für Eliminatoren nimmt die Daten am Ende der Argumentliste, die oft elegant mit pointfree style arbeitet, wenn Sie also definiert haben:
%Vor%dann könnten Sie
ausdrücken %Vor%Was ist das Beste, was ich habe? Es gibt wahrscheinlich noch elegantere Formulierungen, wenn man Bools auf coole Weise betrachtet.
Kirchen Booleans, richtig? :) Ich habe zum Spaß ein kleines Modul entwickelt, indem ich das RankNTypes -Feature benutzt habe, um sie so nah wie möglich an der ursprünglichen Lambda-Kalkül-Version darzustellen.
Also, wenn Sie RankNTypes aktivieren:
Sie könnten den Typ von Church booleans als die Funktionen a -> a -> a für jeden Typ a darstellen und somit eine kompakte Repräsentation für True und False haben, die Ihrer sehr ähnlich ist. Die Eingabe erlaubt uns jedoch, die Funktionen freier zu gestalten.
Nun, wie ist eine Konjunktion in diesen Begriffen geschrieben? Angenommen, Sie haben einen linken Operanden l und einen rechten Operanden r , die beide CBool sind, dh Funktionen a -> a -> a , die Ihnen entweder den ersten oder den zweiten Parameter zurückgeben, je nachdem, ob ctrue oder% Code%. Sie können diese Funktion auswerten, indem Sie die Eingabe cfalse als ersten Parameter und r selbst als dritte eingeben. Wenn l ist l , dann wird es zu seinem ersten Parameter ausgewertet, der ctrue ist: sollte es wieder r sein, dann ist unsere Konjunktion erfüllt. In jedem anderen Fall wird ctrue zurückgegeben.
Die Disjunktion kann auf ähnliche Weise dargestellt werden, mit dem gleichen Trick, die Funktionen, die boolesche Werte darstellen, direkt auszuwerten. Abgesehen davon, dass Sie hier die beiden Argumente für die Bewertung von cfalse tauschen: Wenn l ist l , gibt es ctrue selbst zurück, ansonsten ist es bis zu l 's Wert
Wenn ich RankNTypes aktiviere, denke ich, dass dies am nächsten ist, da man zu den ursprünglichen Definitionen von Konjunktion und Disjunktion für Churchs boolesche Zahlen in Lambda Calculus kommen kann. Ich schrieb auch Funktionen, um aus dem normalen Bool und CBool, der Negation, und auch Churchs natürlichen Zahlen mit dem gleichen Stil hin und her zu übersetzen. Sie finden den gesamten Quellcode unter Ссылка .
Tags und Links haskell functional-programming lambda-calculus