[LINQ via C#-Reihe]

[Lambda-Kalkül über die C#-Reihe]

Der Lambda-Kalkül (auch bekannt als λ-Kalkül) ist ein theoretischer Rahmen zur Beschreibung der Funktionsdefinition, Funktionsanwendung, Funktionsrekursion und verwendet Funktionen und Funktionsanwendung, um Berechnungen auszudrücken. Es ist ein mathematisches formales System, kann aber auch als kleinste Programmiersprache angesehen werden, die jede berechenbare Funktion ausdrücken und auswerten kann. Als universelles Berechnungsmodell ist der Lambda-Kalkül in der Programmiersprachentheorie wichtig und insbesondere die Grundlage der funktionalen Programmierung. Die Kenntnis der Lambda-Kalküle hilft sehr beim Verständnis der funktionalen Programmierung, von LINQ, C# und anderen funktionalen Sprachen.

Ausdruck

Das Kernkonzept des Lambda-Kalküls ist Ausdruck. Es gibt 3 Arten von Ausdrücken im Lambda-Kalkül:Variable, Funktion, Anwendung. Ausdruck kann rekursiv definiert werden:

• Wenn v eine Variable ist, dann ist v ein Ausdruck
• Wenn v eine Variable und E ein Ausdruck ist, dann ist die Funktion λv.E ein Ausdruck. Die Funktionssyntax λv.E kann als die anonyme C#-Funktionssyntax v => E angesehen werden, wobei v der Parameter und E der Funktionskörperausdruck ist.
• Falls E₁ ist Ausdruck und E₂ Ausdruck ist, dann E₁ E₂ ist ein Ausdruck, der als Anwendung bezeichnet wird. Die Anwendungssyntax E₁ E₂ kann als C#-Funktionsaufrufsyntax E₁ angesehen werden (E₂ ), wobei E₁ ist der Funktionsdefinitionsausdruck und E₂ ist der Argumentausdruck.

Standardmäßig behandelt die Lambda-Kalkül-Funktion anonym. Im Lambda-Kalkül gibt es nur Variablennamen. Im Funktionsdefinitionsausdruck ist kein Funktionsname enthalten. In der C#-Sprache ist der Lambda-Ausdruck, der eine anonyme Funktion darstellt, ein Feature, das vor 3,5 Jahren in C# 3.0 mit .NET Framework eingeführt wurde. Tatsächlich wurden die Theorie des Lambda-Ausdrucks und des Lambda-Kalküls bereits in den 1930er Jahren von Alonzo Church, einem Mathematiker und Doktorvater von Alan Turing, eingeführt.

Die folgenden Konventionen sind Ausdrücke:

• Äußerste Klammern können weggelassen werden, z. E₁ E₂ bedeutet (E₁ E₂ ), in C# kann es als (E₁ (E₂ )):Funktion E₁ aufrufen mit Argument E₂
• Eine Folge von Funktionen wird kontrahiert:, z.B. Die Folge der Funktion λx.(λy.(λz.E)) wird als λxyz.E kontrahiert, mit anderen Worten, der Ausdruck λxyz.E bedeutet eigentlich λx.(λy.(λz.E)), was mit λx.λy identisch ist .λz.E, weil die Klammern nicht erforderlich sind. In C# kann man sehen, dass (x, y, z) => E immer zu x => (y => (z => E)) gecurryt wird, was identisch ist mit x => y => z => E denn => Operator ist rechtsassoziativ
• Anwendung bleibt assoziativ, z.B. E₁ E₂ E₃ bedeutet ((E₁ E₂ ) E₃ ), in C# kann es als ((E₁ (E₂ )) (E₃ )):Funktion E₁ aufrufen mit Argument E₂ , dann rufen Sie die zurückgegebene Funktion mit dem Argument E₃ auf

Gebundene Variable vs. freie Variable

In Funktion kann sein Körperausdruck Variablen verwenden. Es gibt 2 Arten von Variablen, die im Funktionskörperausdruck verwendet werden, gebundene Variable und freie Variable:

• Wenn die Variable der Funktion (Variablen vor dem Symbol .) im Ausdruck des Funktionskörpers vorkommt, handelt es sich bei diesen Variablenvorkommen (nach dem Symbol .) um gebundene Variablen. In C# kann dies als Vorkommen deklarierter Funktionsparameter im Funktionsrumpf angesehen werden.
• Alle anderen Variablen sind freie Variablen, in C# können sie als äußere Variable oder Schließung angesehen werden.

Für die Funktion λx.f x hat beispielsweise der Hauptausdruck f x die gebundene Variable x und die freie Variable f. Dies kann als x => f(x) in der C#-Syntax angesehen werden, im Hauptteil ist x ein Parameter und f ein Abschluss.

Eine Variable ist an ihre „nächste“ Funktion gebunden. Beispielsweise wird in λx.g x (λx.h x) das erste Vorkommen von x im Körperausdruck durch die äußere Funktion und das zweite Vorkommen von x durch die innere Funktion gebunden. In C# kann x => g(x)(x => h(x)) aus diesem Grund nicht kompiliert werden – der äußere Funktionsparameter hat denselben Namen wie der innere Funktionsparameter, was vom C#-Compiler nicht zugelassen wird:

internal static class Expression
{
    internal static Func<T, T> Variable<T>(Func<T, Func<Func<T, T>, T>> g, Func<T, T> h) => 
        x => g(x)(x => h(x));
}

Ausdrücke ohne freie Variablen werden auch als Kombinator bezeichnet, worauf später noch eingegangen wird.

Reduzierung

Im Lambda-Kalkül gibt es 3 Substitutionsregeln für den zu reduzierenden Ausdruck.

α-Umwandlung

Im Lambda-Kalkül können die gebundenen Variablen des Lambda-Ausdrucks durch andere Namen ersetzt werden. Dies wird Alpha-Konvertierung oder Alpha-Umbenennung genannt. In C# kann dies als Funktionsparameter angesehen werden, der umbenannt werden kann, z. B. x => f(x) ist äquivalent zu y => f(y).

Im obigen Beispiel von λx.g x (λx.h x) hat die innere Funktion λx.h x die Variable x, die durch einen anderen Namen y ersetzt werden kann, zusammen mit ihrem Erscheinen im Körper h x. Dann wird die innere Funktion zu λy.h y, also wird die äußere Funktion zu λx.g x (λy.h y). Jetzt wird es intuitiv, wie x und y durch die „nächste“ Funktion gebunden sind. In C# kann x => g(x)(y => h(y)) kompiliert werden:

internal static Func<T, T> Variable<T>(Func<T, Func<Func<T, T>, T>> g, Func<T, T> h) => 
    x => g(x)(y => h(y));

β-Reduktion

Die Beta-Reduktion des Funktionsanwendungsausdrucks (λv.E) R wird als E[v :=R] bezeichnet. Es bedeutet, alle freien Vorkommen der Variablen v im Ausdruck E durch den Ausdruck R zu ersetzen. In C# kann dies so angesehen werden, als ob die Funktion mit Argument aufgerufen wird, im Körper werden alle Parametervorkommen durch Argument ersetzt. Wenn zum Beispiel die Funktion x => x + 2 mit 1 aufgerufen wird, wird im Hauptteil x + 2 der Parameter x durch das Argument 1 ersetzt, sodass die Funktion als 1 + 2 ausgewertet wird.

η-Umwandlung

Eta-Umwandlung bedeutet, dass 2 Funktionen genau dann gleich sind, wenn sie für dasselbe Argument immer dasselbe Ergebnis liefern. Beispielsweise kann λx.f x durch f ersetzt werden, wenn x nicht frei in f vorkommt. In C# kann dies so betrachtet werden, dass die Funktion x => f(x) der Funktion f entspricht. Zum Beispiel:

internal static void LinqQuery()
{
    Func<int, bool> isEven = value => value % 2 == 0;
    Enumerable.Range(0, 5).Where(value => isEven(value)).ForEach(value => Console.WriteLine(value));
}

Hier haben die Funktionen value => isEven(value) und function isEven immer das gleiche Ergebnis für dasselbe Argument, also kann value=> isEven(value) durch isEven ersetzt werden. Ebenso kann value => Console.WriteLine(value) durch Console.WriteLine ersetzt werden. Die obige LINQ-Abfrage entspricht:

internal static void EtaConvertion()
{
    Func<int, bool> isEven = value => value % 2 == 0;
    Enumerable.Range(0, 5).Where(isEven).ForEach(Console.WriteLine);
}

Normale Reihenfolge

Die obigen Reduktionsregeln können auf Ausdrücke mit unterschiedlicher Reihenfolge angewendet werden. Bei normaler Reihenfolge wird der ganz linke, äußerste Ausdruck zuerst reduziert. Für Funktionsanwendungsausdrücke bedeutet dies, dass die Funktion zuerst Beta-reduziert wird, dann werden die Argumente reduziert, zum Beispiel:

  (λx.λy.y) ((λa.λb.a) (λv.v))
≡ λy.λy

In diesem Ausdruck wird die Funktion (λx.λy.y) mit dem Argument Ausdruck ((λa.λb.a) (λv.v)) angewendet. Der ganz linke, äußerste Ausdruck ist der Funktionsausdruck (λx.λy.y). Daher sollten in seinem Körper λy.y alle freien Vorkommen von x durch ((λa.λb.a) (λv.v)) ersetzt werden. Und da x nicht vorkommt, ist das Substitutionsergebnis immer noch λy.y. Bei der normalen Ordnungsreduktion wird der Argumentausdruck ((λa.λb.a) (λv.v)) überhaupt nicht reduziert.

Hier kann λy.y nicht weiter reduziert werden. Ein Ausdruck, der mit den obigen 3 Regeln nicht weiter reduziert werden kann, wird in Normalform aufgerufen. Hier ist λy.λy die Normalform von (λx.λy.y) ((λa.λb.a) (λv.v)). Einige Lambda-Ausdrücke können unendlich reduziert werden, haben also keine Normalform, was später besprochen wird.

Bewerbungsreihenfolge

Bei der applikativen Reihenfolge wird der ganz rechte, innerste Ausdruck zuerst reduziert. Für den Funktionsanwendungsausdruck bedeutet dies, dass die Argumente zuerst reduziert werden, dann wird die Funktion betareduziert. Nehmen Sie wieder den obigen Ausdruck als Beispiel:

  (λx.λy.y) ((λa.λb.a) (λv.v))
≡ (λx.λy.y) (λb.λv.v)
≡ λy.λy

Der Argumentausdruck ((λa.λb.a) (λv.v)) ist richtiger als der Funktionsdefinitionsausdruck (λx.λy.y), also wird ((λa.λb.a) (λv.v)) zuerst reduziert . Es kann zur Normalform (λb.λv.v) betareduziert werden, die nicht weiter reduziert werden kann. Dann wird (λx.λy.y) mit (λb.λv.v) angewendet, was auf die Normalform λy.λy betareduziert werden kann. Bei der Reduzierung der Anwendungsreihenfolge muss das Argument vor der Funktionsanwendung reduziert werden. Das ist die Strategie von C#.

Im Lambda-Kalkül führt das Reduzieren von Ausdrücken in beliebiger Reihenfolge zum gleichen Ergebnis, nämlich dem Church-Rosser-Theorem.

Funktionszusammensetzung

Im Lambda-Kalkül bedeutet die Funktionskomposition, einfache Funktionen zu einer komplizierteren Funktion zu kombinieren, die genauso wie die oben erwähnte C#-Funktionskomposition betrachtet werden kann. Die Zusammensetzung von f₁ und f₂ wird mit f₂ bezeichnet ∘ f₁ . Diese neue Funktion (f₂ ∘ f₁ ) ist wie folgt definiert:

(f2 ∘ f1) x := f2 (f1 x)

Hier die Funktionsnamen f₁ und f₂ Geben Sie die Reihenfolge der Anwendung an. f₂ ∘ f₁ kann auch als f₂ gelesen werden nach f₁ . in C# kann dies als die zuvor besprochene Vorwärtskomposition angesehen werden:

public static partial class FuncExtensions
{
    public static Func<T, TResult2> After<T, TResult1, TResult2>(
        this Func<TResult1, TResult2> function2, Func<T, TResult1> function1) =>
            value => function2(function1(value));
}

Wie bereits erwähnt, haben einige andere funktionale Sprachen einen Kompositionsoperator für Funktionen eingebaut, wie>> in F#, . in Haskell usw. C# unterstützt nicht die Definition benutzerdefinierter Operatoren für Funktionen. Als Problemumgehung kann eine Erweiterungsmethode o definiert werden, um diesen ∘-Operator darzustellen:

public static Func<T, TResult2> o<T, TResult1, TResult2>(
    this Func<TResult1, TResult2> function2, Func<T, TResult1> function1) =>
        value => function2(function1(value));

Also f₃ ∘ f₂ ∘ f₁ wird zu f₃ .o(f₂ ).o(f₁ ) in C#, was intuitiver ist, zum Beispiel:

internal static void Compose()
{
    Func<double, double> sqrt = Math.Sqrt;
    Func<double, double> abs = Math.Abs;

    Func<double, double> absSqrt1 = sqrt.o(abs); // Composition: sqrt after abs.
    absSqrt1(-2D).WriteLine(); // 1.4142135623731
}

Assoziativität

Die Funktionskomposition ist assoziativ. Das bedeutet (f₃ ∘ f₂ ) ∘ f₁ und f₃ ∘ (f₂ ∘ f₁ ) sind gleichwertig.

Beim Anwenden von x auf (f₃ ∘ f₂ ) ∘ f₁ , gemäß der Definition von ∘:

  ((f3 ∘ f2) ∘ f1) x
≡ (f3 ∘ f2) (f1 x)
≡ f3 (f2 (f1 x))

Und bei Anwendung von x auf f3 ∘ (f2 ∘ f1):

  f3 ∘ (f2 ∘ f1) x
≡ f3 ∘ (f2 (f1 x))
≡ f3 (f2 (f1 x))

In C# bedeutet dies f₃ .o(f₂ ).o(f₁ ) und f₃ .o(f₂ .o(f₁ )) sind äquivalent:’

internal static void Associativity()
{
    Func<double, double> sqrt = Math.Sqrt;
    Func<double, double> abs = Math.Abs;
    Func<double, double> log = Math.Log;

    Func<double, double> absSqrtLog1 = log.o(sqrt).o(abs); // Composition: (log o sqrt) o abs.
    absSqrtLog1(-2D).WriteLine(); // 0.34642256747438094
    Func<double, double> absSqrtLog2 = log.o(sqrt.o(abs)); // Composition: log o (sqrt o abs).
    absSqrtLog2(-2D).WriteLine(); // 0.34642256747438094
}

Einheit

Es gibt eine Einheitsfunktions-ID für die Funktionszusammenstellung:

Id := λx.x

so dass f ∘ Id und Id ∘ f beide äquivalent zu f:

f ∘ Id = f
Id ∘ f = f

Gemäß der Definition von ∘ und Id:

  (f ∘ Id) x
≡ f (Id x)
≡ f x

  (Id ∘ f) x
≡ Id (f x)
≡ f x

In C# kann ID wie folgt definiert werden:

// Unit<T> is the alias of Func<T, T>.
public delegate T Unit<T>(T value);

public static partial class Functions<T>
{
    public static readonly Unit<T>
        Id = x => x;
}

Hier erhält der Funktionsausdruck (λx.x) einen Namen Id, dies dient nur der Lesbarkeit. Wenn später auf diese Funktion verwiesen wird, wird ihr Name Id verwendet, was intuitiver ist als der Lambda-Ausdruck.