Benutzer:MovGP0/.NET/Lambda Calculus

Lambda Calculus

Notation
Math	C#
λx.(λy.(λz.f))	`x => (y => (z => f(x, y, z)))`
λx.λy.λz.f	`x => y => z => f(x, y, z)`
λxyz.f	`(x, y, z) => f(x, y, z)`

Konversion

α-Konversion: Variablennamen ändern

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));

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

β-Reduktion: Variable wird durch Wert ersetzt:

internal static Func<int, int> increment => x => x+1;
// increment(n) wird zu n+1

η-Konversion: Funktionen liefern bei den gleichen Argumenten immer die gleichen Ergebnisse zurück.; Zwei Funktionen sind gleich, wenn sie bei den gleichen Argumenten die gleichen Ergebnisse liefern.

Basics

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

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

Assoziativität: (f3∘f2)∘f1 = f3∘(f2∘f1) = f3(f2(f1(x)))

Unit (Identität): I := λx.x; f∘I = f; I∘f = f

public delegate T Unit<T>(T value);

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

Church Boolean: „True“ (t) liefert ersten Parameter (a);; True := λab.t = λa.λb.t; „False“ (f) liefert zweiten Parameter (b); False := λab.f = λa.λb.f

let True t f = t
let False t f = f

public delegate Func<dynamic, dynamic> Boolean(object @true);

public static partial class ChurchBoolean
{
    public static readonly Boolean True = @true => @false => @true;

    public static readonly Boolean False = @true => @false => @false;

Logisch-Und: And := λa.λb.a b False = λa.λb.a b (λt.λf.f)

public static partial class ChurchBoolean
{
    public static readonly Func<Boolean, Func<Boolean, Boolean>> And = a => b => (Boolean)a(b)(False);
    // substituting False function
public static Func<Boolean, Func<Boolean, Boolean>>
    And = a => b => a(b)(new Boolean(@true => @false => @false));
}

public static partial class BooleanExtensions
{
    public static Boolean And(this Boolean a, Boolean b) => ChurchBoolean.And(a)(b);
}

Logisch-Oder: Or := λa.λb.a True b

public static Func<Boolean, Func<Boolean, Boolean>> Or = a => b => a(True)(b);

public static Boolean Or(this Boolean a, Boolean b) => ChurchBoolean.Or(a)(b);

Logisch-Nicht: Not := λa.a False True

public static Func<Boolean, Boolean> Not = boolean => boolean(False)(True);

public static Boolean Not(this Boolean a) => ChurchBoolean.Not(a);

Exklusiv-Oder: Xor := λa.λb.a (Not b) b

public static Func<Boolean, Func<Boolean, Boolean>>
    Xor = a => b => a(Not(b))(b);

public static Boolean Xor(this Boolean a, Boolean b) => ChurchBoolean.Xor(a)(b);

System.Boolean

public static partial class ChurchEncoding
{
    // System.Boolean structure to Boolean function.
    public static Boolean Church(this bool boolean) => boolean ? True : False;

    // Boolean function to System.Boolean structure.
    public static bool Unchurch(this Boolean boolean) => boolean(true)(false);
}

If: If := λb.λt.λf.b t f; Eager: C# wertet rechte Austrücke zuerst aus („Applikative Reihenfolge“ statt „Normale Reihenfolge“); dH. then- und else-Branch wird ausgeführt und contition bestimmt anschließend den Rückgabewert.

public static readonly Func<Boolean, Func<dynamic, Func<dynamic, dynamic>>> EagerIf = condition => then => @else => condition  (then) (@else);

Lazy: Factories werden ausgeführt und anschließend der Rückgabewert mittels der Identitätsfunktion bestimmt.

public static readonly Func<Boolean, Func<Func<Unit<dynamic>, dynamic>, Func<Func<Unit<dynamic>, dynamic>, dynamic>>> If = condition => thenFactory => elseFactory => condition (thenFactory) (elseFactory)(Functions<dynamic>.Id);

Quellen

Lambda Calculus via C#

Dixin Yan: (1) Fundamentals. 7. Oktober 2016, abgerufen am 4. Mai 2017 (englisch).
Dixin Yan: (2) Boolean and Logic. 7. Oktober 2016, abgerufen am 4. Mai 2017 (englisch).
Dixin Yan: (3) Numeral, Arithmetic and Predicate. 9. Oktober 2016, abgerufen am 4. Mai 2017 (englisch).
Dixin Yan: (4) Tuple and Signed Numeral. 18. März 2017, abgerufen am 4. Mai 2017 (englisch).
Dixin Yan: (5) List. 18. März 2017, abgerufen am 4. Mai 2017 (englisch).
Dixin Yan: (6) Combinatory Logic. 18. März 2017, abgerufen am 4. Mai 2017 (englisch).
Dixin Yan: (7) Fixed Point Combinator and Recursion. 18. März 2017, abgerufen am 4. Mai 2017 (englisch).
Dixin Yan: (8) Undecidability of Equivalence. 21. Februar 2015, abgerufen am 4. Mai 2017 (englisch).

|}