Eine Transitionssemantik

In GOLOG wird bisher eine Evaluationssemantik verwendet [25]. Diese Semantiken basieren auf der kompletten Auswertung des Programms. Bevor die erste Aktion ausgeführt werden kann, muß eine komplette und gültige Lösungssequenz gefunden werden. Durch die Einbeziehung von Nebenläufigkeit erscheint es sinnvoller, Transitionssemantiken (Berechnungssemantiken) einzusetzen [25]. Diese basieren auf einzelnen Berechnungsschritten anstelle der gesamten Berechnung. Daher definieren wir eine Transition und ein Prädikat als:

:= Dies ist der Übergang von der Situation zu durch die Ausführung der ersten primitiven Aktion oder einer Testaktion aus . Für das Restprogramm kann dann zum Beispiel gelten: oder . Wir haben so eine Transition zwischen den Konfigurationen und definiert. bezeichnet also das von aus noch auszuführende Programm.

:= Die Konfiguration ist final, wenn die Bearbeitung abgeschlossen ist, also keine Aktion mehr ausgeführt werden muß. Die daraus abgeleiteten Situationen einer Endkonfiguration sind die gleichen, die durch einen entsprechenden -Term ermittelt werden.

Komplette Berechnungen werden nun durch die Aneinanderreihung von Einzelschritten bis zur Erreichung eines Endzustandes gebildet. Trans und Final müssen für alle 13 Konstrukte der Sprache ConGOLOG definiert werden. Diese formale Definition würde den Rahmen dieser Arbeit überschreiten. Es seien daher nur Beispiele genannt und auf [31] verwiesen:

• Leeres Programm (nil)
  
  $$\begin{array}{ccc} Trans(nil,s,\delta ',s') & \equiv & False\\ Final(nils,s) & \equiv & True \end{array}$$
  
  

• primitive Aktion
  
  $$\begin{array}{cccc} Trans(a,s,\delta ',s') & \equiv & Poss(a... ... \, \, \, \, \, \, \, \, \, \, \, \, \, \, \, \, & \end{array}$$
  
  

• Sequenz
  
  $$\begin{array}{cccc} Trans(\delta _{1};\delta _{2},s,\delta '... ... \, \, \, \, \, \, \, \, \, \, \, \, \, \, \, \, & \end{array}$$
  
  

• nebenläufige Ausführung
  
  $$\begin{array}{cccc} Trans(\delta _{1}\vert\vert\delta _{2},s... ... \, \, \, \, \, \, \, \, \, \, \, \, \, \, \, \, & \end{array}$$
  
  

Die möglichen Konfigurationen ergeben sich aus der wiederholten Ausführung der Relation von der Konfiguration aus, es sind also die Konfigurationen, die sich in der transitiven Hülle der Relation befinden. definiert dies innerhalb des Situationskalküls:

$$Trans^{\star }(\delta ,s,\delta ',s'):=\forall T[...\supset T(\delta ,s,\delta ',s')]$$

und ... steht für die Konjunktion der universellen Hülle der folgenden Implikationen:

$$\begin{array}{cc} True\supset T(\delta ,s,\delta ',s') & \\ ... ...',s'',\delta ',s')\supset T(\delta ,s,\delta ',s'). \end{array}$$

Nun kann eine neue Definition des -Operators mit Hilfe von und vorgenommen werden:

$$Do(\delta ,s,s'):=\exists \delta '.Trans^{\star }(\delta ,s,\delta ',s')\wedge Final(\delta ',s')$$

Das hier definierte ist äquivalent zu dem oben definierten. Eine Sequenz von Aktionen kann also ebenfalls durch

$$Axioms\models Do(\delta ,S_{0},do(\vec{a},S_{o}))$$

ermittelt werden [31]. Die Axiome müssen nur um die Definitionen von und erweitert werden.