hornet - Eine Prolog-artige Embedded DSL für Python 3.3

[pillmuncher]

AKA: Learn You a Metaprogramming For Great Good
AKA: Horn-Klauseln via Expression Trees - daher der Name hornet.

https://github.com/pillmuncher/hornet

Es ist noch nicht so, wie ich es haben möchte, aber ich denke, es ist schon mal ein guter Anfang.

Die Idee dahinter ist, dass man Operatoren überlädt, und mit jedem Operator-Aufruf den bisherigen Zustand in einen neuen überführt. Ich kann es am besten an einem Beispiel erklären.

Code: Alles auswählen

def tribes(db, sam, joe, jim, bob, dan, hal, tom, lee, son, descendant,
           ancestor, related, related_, directly_related, forefather, tribe,
           Tribe, X, Y, Z, Seen):

    db.assertz(

        son(joe, sam),  # joe is the son of sam, etc.
        son(jim, joe),
        son(tom, bob),
        son(hal, bob),
        son(dan, jim),
        son(lee, jim),

        # X is a descendant of Y:
        descendant(X, Y) <<
            son(X, Y),          # one's son is one's descendant
        descendant(X, Z) <<
            son(Y, Z) &         # a descendant of one's son
            descendant(X, Y),   # is also one's descendant

        # X is an ancestor of Y:
        ancestor(X, Y) <<
            descendant(Y, X),   # one is an ancestor of one's descendant

        related(X, Y) <<
            related(X, Y, [X]),

        related(X, Y, Seen) <<
            directly_related(X, Z) &
            not_(member(Z, Seen)) &
            related_(Z, Y, Seen),

        related_(X, X, _),
        related_(X, Y, Seen) <<
            related(X, Y, [X | Seen]),

        directly_related(X, Y) <<
            son(X, Y),
        directly_related(X, Y) <<
            son(Y, X),

        # Z is the forefather of X:
        forefather(Z, X) <<
            son(X, Y) &
            forefather(Z, Y) & cut,
        forefather(Z, Z),

        tribe(X, [Z | Tribe]) <<
            forefather(Z, X) &
            findall(Y, descendant(Y, Z), Tribe),

    )


def genealogy(db, joe, bob, dan, lee, descendant, ancestor, related, tribe, A, B):

    db.consult(tribes)

    print('who is an ancestor of who?')
    for subst in db |- ancestor(A, B):
        print(subst[A], 'of', subst[B])
    print()

    print('who are joe\'s descendants?')
    for subst in db |- descendant(A, joe):
        print(subst[A])
    print()

    print('who are dan\'s ancestors?')
    for subst in db |- ancestor(A, dan):
        print(subst[A])
    print()

    print('who is bob related to?')
    for subst in db |- related(bob, A):
        print(subst[A])
    print()

    print('who is related to bob?')
    for subst in db |- related(A, bob):
        print(subst[A])
    print()

    print('who is lee related to?')
    for subst in db |- related(lee, A):
        print(subst[A])
    print()

    print('who is related to lee?')
    for subst in db |- related(A, lee):
        print(subst[A])
    print()

    print('is lee related to joe?')
    for subst in db |- related(lee, joe):
        print('Yes.')
        break
    else:
        print('No.')
    print()

    print('is lee related to bob?')
    for subst in db |- related(lee, bob):
        print('Yes.')
        break
    else:
        print('No.')
    print()

    print('one is not a relative of oneself. true?')
    for subst in db |- not_(related(A, A)):
        print('Yes.')
        break
    else:
        print('No.')
    print()

    print('who belongs to joe\'s tribe?')
    for subst in db |- tribe(joe, A):
        print(subst[A])
    print()


db = Database()
db.consult(genealogy)

Ergebnis:

Code: Alles auswählen

who is an ancestor of who?
sam of joe
joe of jim
bob of tom
bob of hal
jim of dan
jim of lee
sam of jim
sam of dan
sam of lee
joe of dan
joe of lee

who are joe's descendants?
jim
dan
lee

who are dan's ancestors?
jim
sam
joe

who is bob related to?
tom
hal

who is related to bob?
tom
hal

who is lee related to?
jim
joe
sam
dan

who is related to lee?
dan
sam
joe
jim

is lee related to joe?
Yes.

is lee related to bob?
No.

one is not a relative of oneself. true?
Yes.

who belongs to joe's tribe?
[sam, joe, jim, dan, lee]

Alle Parameter der Funkionen tribes() und genealogy() - bis auf den ersten - werden automatisch mit sog. Atomen bzw sog. logischen Variablen initialisiert, die dieselben Namen haben, wie der Parameter, für den sie an die Funktion übergeben werden. Namen von Atomen beginnen mit einem Kleinbuschstaben und Namen von Variablen mit einem Großbuchstaben oder Unterstrich. Die Magie der automatischen Erzeugung dieser Objekte stammt vom Aufruf von db.consult(...)Tatsächlich ist es nur sehr wenig Magie, es sind nur ein paar Zeilen. Diese Atome können nun mittels Operatoren-Aufrufen manipuliert werden. Genau genommen erzeugen sie für jeden Operator-Aufruf ein neues Objekt, dass in sich alle Zuständsänderungen speichert. So wird etwa aus einem Atom, dessen __call__()-Methode aufgerufen wird, eine Relation zwischen den übergebenen Argumenten. aus dem Atom son wird so die Relation son(joe, sam), die besagt, das joe der Sohn von sam ist. Und bei einer Formel x << y entsteht eine Regel, die besagt, dass x wahr ist, sofern y wahr ist. Diese Regeln sind soz. der Treibstoff im Prolog-Motor. Man kann die Formel nämlich auch umgekehrt lesen: um x zu beweisen, beweise y. Hier ein anderes Beispiel umd das zu illustrieren:

Code: Alles auswählen

def barbara(db, socrates, plato, aristotle, man, mortal, Who, X):
    db.assertz(
        man(socrates),

        mortal(X) <<
            man(X),
    )
    for subst in db |- mortal(Who):  # Wer ist sterblich?
        print(subst[Who])
    print()

db = Database()
db.consult(barbara)

Antwort:

Code: Alles auswählen

socrates

In der Datenbank stehen zwei Klauseln: die Tatsache, dass socrates ein Mensch ist, und die Regel, dass Menschen sterblich sind. Prolog kann daraus die Anfrage, wer sterblich ist beweisen und uns mitteilen, wer derjenige ist. Das Verfahren in diesem Fall heißt SLD-Resolution. Dabei wird die Anfrage als sog. Anfangs-Ziel genommen und die Datenbank durchsucht, ob es eine Tatsache oder eine Regel gibt, deren Kopf (die linke Seite von <<) mit der Anfrage in Übereinstimmung geracht werden kann. Diesen Schritt nennt man Unifikation. Im o.s. Beispiel findet Prolog eine Übereinstimmung zwischen mortal(Who) und mortal(X) und unifiziert Who und X. Fortan - dh. im Laufe der aktuellen Ableitung - stehen beide Variablen für dasselbe, bisher unbekannte, Objekt. Sobald eine der beiden Variablen an ein solches Objekt gebunden wird, ist auch die andere automatisch daran gebunden. Da es sich bei mortal(X) um eine Regel handelt, versucht Prolog nun, die rechte Seite des << zu beweisen. dazu stellt es sich selbst die Anfrge man(X). Es durchsucht erneut die Datenbank und findet man(socrates). Nun wird socrates mit X unifiziert und damit implizit auch Who. Da man(socrates) eine Tatsache und keine Regel ist und mithin kein << mit einer zu beweisenden rechten Seite besitzt, ist eine erste Antwort gefunden, Who == socrates.

Klauseln dieser Art nennt man Hornklauseln. Sie können beliebig komplex sein. Unter logischer Betrachtung handelt es sich bei ihnen einfach um logsiche Formeln, aber dank des Curry-Howard-Isomorphismus lassen sie sich auch als Prozeduren lesen. Dadurch wird das Aufstellen von Axiomen zur Programmierung.