Es folgen einige Begriffsdefinitionen. Die Erklärungen beziehen sich auf die Standardeinstellungen von GGPS. Manche lassen sich in der Eingabedatei ändern. Siehe Eingabedatei.
Eine Konstante ist eine beliebige Zeichenkette ohne die Zeichen
#, (, ) und ` ' (Leerzeichen).
Eine Variable ist ein #, unmittelbar gefolgt von einer
nicht-negativen ganzen Zahl, z.B. #0 und #13.
Eine Funktion oder ein Operator ist eine Konstante gefolgt von (.
Z.B. sind in i(, *(, Op( die Zeichenketten
i, * und Op Funktionen.
Ein Satz oder Ausdruck ist eine vollständig geklammerte Anordnung aus
Konstanten, Variablen und Funktionen. Trennsymbol ist
,. D.h. Konstanten und Variablen sind Sätze und
f(...,...,...) ist ein Satz, wobei ... wieder
Konstanten, Variablen oder Sätze sein dürfen. Z.B.:
i(1), i(#1), *(1,#0),
*(#1,*(#2,#3)).
Eine Regel sind zwei durch = getrennte Sätze,
z.B. *(1,#0)=#0. Diese heißen äquivalent, = wird als
äquivalenzrelation behandelt.
GGPS akzeptiert beliebig viele Leerzeichen an beliebiger Stelle innerhalb von Regeln und Sätzen.
Eine Regelvariable ist eine Variable, die in Regeln vorkommen
darf und nicht in Sätzen. Regelvariablen sind #0-#9.
Eine Satzvariable ist eine Variable, die in Sätzen vorkommen darf und
nicht in Regeln. Satzvariablen sind #10 und Variablen mit
höherer Nummer.
Eine Äquivalenzklasse ist eine Menge von Sätzen, die GGPS bereits als äquivalent erkannt hat.
Eine Substitution ist eine Ersetzung von Variablen durch Sätze. Sie wird
durch -> angezeigt. Z.B. #1->i(#2).
Eine Substitution heißt gültig, wenn ihre wiederholte Anwendung auf
Sätze immer endet. Die Substitution #1->i(#1) ist z.B. nicht gültig.
Eine Unifikation zweier Sätze ist eine gültige Substitution, die diese beiden
Sätze identisch, d.h. zu gleichen Zeichenketten, macht. Zwei Sätze
heißen unifizierbar wenn es eine Unifikation der beiden Sätze gibt. Die
Sätze *(#1,#2) und *(1,i(#3)) sind mit der Substitution
#1->1, #2->i(#3) unifizierbar, die Sätze *(#1,#1) und
*(#10,i(#10)) sind nicht unifizierbar, da die Substitution
#1->#10, #10->i(#10) nicht gültig ist.
Als allgemeinste Unifikation oder allgemeinsten Unifikator bezeichnet man eine Unifikation, aus der jede andere Unifikation durch Substitution abgeleitet werden kann. Im folgenden ist immer allgemeinste Unifikation gemeint, auch wenn nur von Unifikation gesprochen wird.
Ein Ausdruck heißt Unterausdruck eines anderen Ausdrucks wenn er in dem anderen Ausdruck vorkommt.
Eine Regel heißt auf einen Satz anwendbar wenn es eine Unifikation zwischen einem Unterausdruck des Satzes und der linken Seite der Regel gibt.
Eine Variable heißt gebunden bzgl. einer Äquivalenzklasse wenn sie in mindestens einem Satz der Äquivalenzklasse vorkommt und in mindestens einem Satz nicht vorkommt.
Eine Variable heißt frei bzgl. einer Äquivalenzklasse wenn sie in allen Sätzen der Äquivalenzklasse vorkommt.
Eine Substitution heißt interpretierend wenn nicht nur Regelvariablen substituiert werden.
Eine Substitution eines Satzes in einer Äquivalenzklasse heißt äquivalenzerhaltend wenn nur gebundene Variablen ersetzt werden. Eine nicht interpretierende Substitution ist äquivalenzerhaltend, da nur Regelvariablen ersetzt werden und diese im Satz nicht vorkommen.
Beispiel:
Eine Äquivalenzklasse enthalte die Sätze #10 und
*(*(i(#11),#11),#10). Die Variable #10 ist also frei, die
Variable #11 gebunden. Substitutionen die allenfalls #11
ersetzen sind äquivalenzerhaltend.
Eine Regel sei auf einen Ausdruck anwendbar. Dann kann der entsprechende Unterausdruck durch die rechte Seite der Regel ersetzt werden und der Unifikator kann auf den gesamten Ausdruck angewandt werden. Falls der Unifikator äquivalenzerhaltend ist heißt dieser Ausdruck Regelergebnis. Falls der Unifikator nicht äquivalenzerhaltend ist wird der Unterausdruck auch durch die linke Seite der Regel ersetzt und der Unifikator wird auch auf den so entstehenden Ausdruck angewandt. Die beiden so entstehenden Ausrücke sind äquivalent und können somit als Regel interpretiert werden. Diese Regel heißt dann das Regelergebnis.
Beispiele:
Die Regel *(1,#0)=#0 werde auf den Ausdruck *(1,#10)
angewandt. Ist der entsprechende Unterausdruck der Ausdruck selbst, so
lautet die Unifikation #0->#10. Ersetzung des Unterausdrucks
durch die rechte Seite der Regel ergibt #0, Anwendung der
Substitution ergibt #10 als Regelergebnis.
Die Regel *(1,#0)=#0 werde auf den Ausdruck *(1,#10)
angewandt. Der entsprechende Unterausdruck sei #10.
Die Unifikation lautet dann #10->*(1,#0). Ersetzung des Unterausdrucks
durch die rechte Seite der Regel ergibt *(1,#0), Anwendung der
Substitution ergibt *(1,#0). Ersetzung des Unterausdrucks durch
die linke Seite der Regel ergibt *(1,*(1,#0)). Anwendung der
Substitution ergibt *(1,*(1,#0)). Das Regelergebnis ist also
*(1,#0)=*(1,*(1,#0)).
Die Regel *(1,#0)=#0 werde auf den Ausdruck *(#10,#10)
angewandt. Der entsprechende Unterausdruck sei die zweite #10.
Die Unifikation lautet dann #10->*(1,#0). Ersetzung des Unterausdrucks
durch die rechte Seite der Regel ergibt *(#10,#0), Anwendung der
Substitution ergibt *(*(1,#0),#0). Ersetzung des Unterausdrucks durch
die linke Seite der Regel ergibt *(#10,*(1,#0)). Anwendung der
Substitution ergibt *(*(1,#0),*(1,#0)). Das Regelergebnis ist also
*(*(1,#0),#0)=*(*(1,#0),*(1,#0)).
Zwei Äquivalenzklassen, die einen Satz gemeinsam enthalten, sind äquivalent und dürfen vereinigt werden. Dies kann geschehen, indem ein Satz als Regelergebnis erzeugt wird, der schon in einer anderen Äquivalenzklasse vorkommt als derjenigen, zu der der Satz gehört aus dem das Regelergebnis entstanden ist oder indem eine Regel als Regelergebnis erzeugt wird, wobei beide Seiten der Regel schon in verschiedenen Äquivalenzklassen vorkommen.
Vorgehensweise von GGPS: GGPS ordnet anfangs alle Regeln in Äquivalenzklassen ein, d.h. linke und rechte Seite einer Regel kommen jeweils zusammen in eine Äquivalenzklasse. Alle Regeln werden auf alle Sätze angewandt, wobei alle möglichen Regelergebnisse erzeugt werden. Die Regelergebnisse werden in entsprechende Äquivalenzklassen eingeordnet. Das heißt im Einzelnen:
Die Länge eines Satzes ist die Anzahl der in ihm vorkommenden Konstanten, Variablen und Funktionen.
Ein Satz heißt kleiner als ein anderer wenn er alphabetisch kleiner ist. Hierbei sind Konstanten alphabetisch kleiner als Variablen und Variablen alphabetisch kleiner als Funktionen. Eine Variable ist alphabetisch kleiner als eine andere Variable wenn ihre Nummer kleiner ist als die der anderen Variablen. Konstanten und Funktionen untereinander werden verglichen, indem ihre Zeichenketten alphabetisch verglichen werden. Ein Ausdruck ist zunächst alphabetisch kleiner als ein anderer Ausdruck, wenn er weniger Unterausdrücke enthält. Enthalten die beiden Ausdrücke gleich viele Unterausdrücke, so entscheiden zunächst die Funktionen, dann die Unterausdrücke darüber, welcher Ausdruck alphabetische kleiner ist. Wie ``alphabetisch kleiner'' jedoch exakt definiert ist, ist nicht so wichtig, Hauptsache es gilt: Ist ein Satz weder alphabetisch kleiner noch größer als ein anderer Satz, so sind die beiden Sätze identisch. Man kann sich also auch vorstellen, dass ``alphabetisch kleiner'' irgendeine totale Ordnung zwischen den Sätzen ist.
Ein Satz heißt komprimierbar, wenn es eine äquivalenzerhaltende Anwendung einer Regel gibt, so dass das Regelergebnis eine kleinere Länge hat oder so dass das Regelergebnis zwar gleiche Länge wie der Satz hat aber alphabetisch kleiner ist. Das Regelergebnis heißt dann kleiner als der Satz i.S.d. Komprimierbarkeit.
Ein Regelergebnis, das durch eine nicht interpretierende Unifikation entstanden ist, heißt durch Kompression entstanden, wenn hierdurch der ursprüngliche Satz komprimiert wurde. Alle anderen Regelergebnisse heißen durch Expansion entstanden.
Eine Regel heißt interessant wenn ihre rechte und linke Seite nicht komprimierbar und nicht identisch sind.
Der im Sinne der Komprimierbarkeit kleinste Satz einer Äquivalenzklasse heißt Standardform der Äquivalenzklasse.
Vorgehensweise von GGPS: Wenn GGPS ein Regelergebnis durch eine äquivalenzerhaltende Substitution erhält sieht es die Regel ``Regelergebnis=Standardform der Äquivalenzklasse'' als potentielle neue Regel an. Ist eine potentielle neue Regel interessant, so wird sie dem Regelsystem hinzugefügt.
Theorem: GGPS beweist alle interessanten Regeln, ausgenommen allenfalls solche, die durch eine bloße Substitution aus einer interessanten Regel enstehen. Anders formuliert: Man denke sich eine aus dem Axiomensystem ableitbare Regel. Dann findet GGPS ein Regelsystem, das diese Regel enthält oder obsolet macht.
Erweisen sich rechte oder linke Seite einer Regel nachträglich als komprimierbar, so wird die Regel als obsolet gekennzeichnet und in Zukunft nicht mehr angewandt.
Eine neue Regel entsteht ja aus einem Satz und einer Standardform einer Äquivalenzklasse. Die Standardform einer Äquivalenzklasse ist der i.S.d. Komprimierbarkeit kleinste Satz dieser Äquivalenzklasse. D.h. eine Regel kann aus zwei Gründen obsolet werden: Entweder der Satz, aus dem die Regel entstanden ist, erweist sich als durch eine neue Regel komprimierbar oder die Standardform der Äquivalenzklasse des Satzes ändert sich. Ändert sich die Standardform, so kann man aus der alten (nun obsoleten) Regel eine neue konstruieren, indem man einfach die neue Standardform einsetzt. Das macht GGPS auch. Erweist sich der Satz als komprimierbar, so sind keine besonderen Maßnahmen erforderlich, da bei der nächsten Kompression dieser Satz weiter komprimiert wird, und die modifizierte Version der obsoleten Regel somit automatisch gefunden wird.