Das deutsche Python-Forum

Über die letzten Wochen habe ich Hornet komplett überarbeitet:

https://github.com/pillmuncher/hornet

Hornet ist ein Prolog-in-Python, d.h. eine eingebettete Domänen-spezifische Sprache zur Logik-Programierung in Python. Es fußt auf drei grundlegenden Ideen:

die DSL selbst, basierend auf Expresison Trees
ein Mechanismus zur Ausführung darin geschriebener Logik-Programme, in Form einer dreiläufigen Continuation Monade
Tail-Call Elimination in Form eines Decorators und einer Driver-Funktion, um Rekursion verwenden zu können ohne den Ausführungs-Stack zu sprengen

Die DSL verwendet (ähnlich wie SymPy) Expression Trees, hier zur Modellierung von Horn-Klauseln. Daher der Name: HornET. Horn-Klauseln sind ein Konzept aus der Logik, bei der Quantifizierung implizit ist. Horn-Klauseln sind deswegen eine vollständige Form der Prädikaten-Logik erster Stufe (First Order Predicate Logic, FOL).

Der Ausführungsmechanismus beruht auf der Continuation Monade, hier erweitert auf drei Continuations: eine für den Erfolgsfall, eine für das Scheitern um Backtracking zu starten, und eine um Suchbäume zu beschneiden. Jede Stelle im Code, die alternative Lösungswege ausführen kann, wird Choice Point genannt. Bei speziellen Choice Points, den sog. Prunable Choice Points, kann eine Continuation eingeführt werden, die die Alternativen beschneidet, d.h. dass nicht alle Alternativen ausgewertet werden, sofern im Kontext des derzeitigen Ausführungsastes ein Cut steht (in Prolog `!`, hier 'cut').

Warum sollte man Prolog in Python verwenden wollen? Hier einige Beispiele:

Das vordefinierte Standard-Prädikat 'append/3' (d.h. eine logische Prozedur mit drei Argumenten) fügt zwei Listen zu einer dritten zusammen:

Code: Alles auswählen

append([A | B], C, [A | D]).when(
    append(B, C, D),
)
append([], A, A)

Verwendet werden kann es so:

Code: Alles auswählen

from hornet import database
from hornet.symbols import append, L, L1, L2
db = database()
for subst in db.ask(append([1, 2, 3], [4, 5], L)):
    print(subst[L])

das erzeugt das erwartete Ergebnis:

Code: Alles auswählen

[1, 2, 3, 4, 5]

Man kann das dasselbe Programm aber auch "rückwärts" laufen lassen und fragen: Welche Listen ergeben zusammengefügt die Liste '[1, 2, 3, 4, 5]'?

Code: Alles auswählen

for i, subst in enumerate(db.ask(append(L1, L2, [1, 2, 3, 4, 5]))):
    print(f"{i}:", subst[L1], "+", subst[L2])

Ergebnis:

Code: Alles auswählen

0: [1, 2, 3, 4, 5] + []
1: [1, 2, 3, 4] + [5]
2: [1, 2, 3] + [4, 5]
3: [1, 2] + [3, 4, 5]
4: [1] + [2, 3, 4, 5]
5: [] + [1, 2, 3, 4, 5]

Logik-Programmierung kann überall eingesetzt werden, wo symbolische Berechnung das Ziel ist, zB. zur symbolischen Differenzierung:

Code: Alles auswählen

db.tell(
    diff(X, Y, Z).when(d(X, Y, Z)),
    d(X, X, 1).when(
        cut,
    ),
    d(C, X, 0).when(
        is_atomic(C),
        cut,
    ),
    s(X + 0, Y).when(
        cut,
        s(X, Y),
    ),
    s(0 + X, Y).when(
        cut,
        s(X, Y),
    ),
    s(X - 0, Y).when(
        cut,
        s(X, Y),
    ),
    s(0 - X, -Y).when(
        cut,
        s(X, Y),
    ),
    d(U + V, X, A + B).when(
        cut,
        d(U, X, A),
        d(V, X, B),
    ),
    d(U - V, X, A - B).when(
        cut,
        d(U, X, A),
        d(V, X, B),
    ),
    d(0 * U, X, 0).when(
        cut,
    ),
    d(U * 0, X, 0).when(
        cut,
    ),
    d(1 * U, X, V).when(
        cut,
        d(U, X, V),
    ),
    d(U * 1, X, V).when(
        cut,
        d(U, X, V),
    ),
    d(C * U, X, C * A).when(
        is_atomic(C),
        ~equal(C, X), 
        cut, 
        d(U, X, A),
    ),
    d(U * V, X, B * U + A * V).when(
        cut,
        d(U, X, A),
        d(V, X, B),
    ),
    d(0 / U, X, 0).when(
        cut,
    ),
    d(U / V, X, (A * V - B * U) / (V * V)).when(
        cut,
        d(U, X, A),
        d(V, X, B),
    ),
    d(U**C, X, C * A * U ** (C - 1)).when(
        is_atomic(C),
        ~equal(C, X),
        cut,
        d(U, X, A),
    ),
    d(U**-C, X, -C * A * U ** (-C - 1)).when(
        cut,
        d(U, X, A),
    ),
    d(U**C, X, C * A * U ** (C - 1)).when(
        equal(C, -C1),
        is_atomic(C1),
        ~equal(C1, X),
        cut,
        d(U, X, A),
    ),
    d(sin(W), X, Z * cos(W)).when(
        cut,
        d(W, X, Z),
    ),
    d(exp(W), X, Z * exp(W)).when(
        cut,
        d(W, X, Z),
    ),
    d(log(W), X, Z / W).when(
        cut,
        d(W, X, Z),
    ),
    d(cos(W), X, -(Z * sin(W))).when(
        cut,
        d(W, X, Z),
    ),
    # Kürzung
    simp(X, Y).when(s(X, Y)),
    s(A, A).when(
        is_atomic(A),
        cut,
    ),
    # Addition
    s(0 + A, B).when(
        cut,
        s(A, B),
    ),
    s(A + 0, B).when(
        cut,
        s(A, B),
    ),
    ...
)

Beispiel:

Code: Alles auswählen

from hornet.symbols import x, diff, simp, A, B, C
def diff_test(db):
    formula = x**-3 + 2 * x**2 + 7 * (x + 9)
    for subst in db.ask(simp(formula, A), diff(A, x, B), simp(B, C)):
        print(f"{subst[A] = !s}")
        print(f"{subst[B] = !s}")
        print(f"{subst[C] = !s}")

Ergebnis:

Code: Alles auswählen

subst[A] = x ** -3 + 2 * x ** 2 + 7 * (x + 9)
subst[B] = -3 * 1 * x ** (-3 - 1) + 2 * 2 * 1 * x ** (2 - 1) + 7 * (1 + 0)
subst[C] = -3 * x ** -4 + 4 * x + 7

Ein anderes Beispiel ist FizzBuzz:

Code: Alles auswählen

from toolz import take

from hornet import DCGs, database
from hornet.symbols import M, N, R, S, V, Ws, _, cut, equal, fb, fizzbuzz
from hornet.symbols import ifelse, inline, join, let, phrase, word, words

def main(db):
    db.tell(
        fizzbuzz(R).when(
            fb(1, R),
        ),
        fb(N, R).when(
            phrase(words(N), Ws),
            join(Ws, S),
            ifelse(
                equal(S, ""),
                equal(N, R),
                equal(S, R),
            ),
        ),
        fb(N, R).when(
            let(M, N + 1),
            fb(M, R),
        ),
        *DCGs(
            words(N).when(
                word(3, N),
                word(5, N),
                word(7, N),
                inline(cut),
            ),
            word(3, N).when(inline(let(M, N % 3), equal(M, 0)), ["fizz"]),
            word(5, N).when(inline(let(M, N % 5), equal(M, 0)), ["buzz"]),
            word(7, N).when(inline(let(M, N % 7), equal(M, 0)), ["quux"]),
            word(_, _),
        ),
    )

    for s in take(1111, db.ask(fizzbuzz(V))):
        print(s[V])


if __name__ == "__main__":
    main(database())

Hier wird eine DCG, eine Definite Clause Grammar, verwendet um die Ausgabe-Strings zu berechnen. Ergebnis:

Code: Alles auswählen

1
2
fizz
4
buzz
fizz
quux
8
fizz
buzz
11
fizz
13
quux
fizzbuzz
16
...
104
fizzbuzzquux
106
...

Dieses Beispiel zeigt auch, wie die jeweils nächste Zeile mittels Backtracking erzeugt wird.

Warum habe ich das gebaut? Weil ich wissen wollte, wie Prolog funktioniert. Hornet ist nicht fertig, es fehlen zB. noch viele vordefinierte System-Prädikate, Unit Tests, und ich kann auch nicht garantieren, dass es keine Bugs gibt. Als Proof-of-Concept allerdings funktioniert es und zeigt, dass es nicht nur möglich, sondern auch schnell genug ist für einige Anwendungsfälle. Einfache Parser etwa sind oft schnell genug und können sehr leicht gebaut werden, insbesondere Dank der integrierten DCG-Expansion. Ich habe auch großen Wert auf Interoperabilität mit Python gelegt, so dass Prädikate leicht in Python selbst implementiert werden können, etwa so:

Code: Alles auswählen

@db.tell
@predicate(univ(C, L))
def _univ(db: Database, subst: Subst) -> Step:
    cin = subst[C]
    lin = subst[L]
    assert isinstance(cin, Functor | Atom | Variable)
    match cin:
        case Atom(name=name):
            return _unify(lin, promote([cin]))(db, subst.map)
        case Functor(name=name, args=args):
            return _unify(lin, promote([Atom(name), *args]))(db, subst.map)
        case Variable():
            assert isinstance(lin, Cons | Empty)
            head, *tail = to_python_list(lin)
            assert isinstance(head, Atom)
            return _unify(cin, Functor(head.name, *tail))(db, subst.map)

Über Rückmeldungen würde ich mich freuen.