[Toss-devel-svn] SF.net SVN: toss:[1437] trunk/Toss/www/reference/reference.tex

[<luk...@us...>]

Revision: 1437
          http://toss.svn.sourceforge.net/toss/?rev=1437&view=rev
Author:   lukstafi
Date:     2011-05-13 12:42:31 +0000 (Fri, 13 May 2011)

Log Message:
-----------
Reference specification of GDL translation: expanded {Rewriting Rule Creation}, first draft of {Translating Formulas}.

Modified Paths:
--------------
    trunk/Toss/www/reference/reference.tex

Modified: trunk/Toss/www/reference/reference.tex
===================================================================
--- trunk/Toss/www/reference/reference.tex	2011-05-12 23:29:43 UTC (rev 1436)
+++ trunk/Toss/www/reference/reference.tex	2011-05-13 12:42:31 UTC (rev 1437)
@@ -1112,9 +1112,13 @@
 \section{Game Description Language}
 
 The game description language, GDL, is a variant of Datalog used to
-specify games in a compact, prolog-like way. The GDL syntax and semantics
-are defined in \cite{GLP05,LHHSG08}, we refer the reader there for the
-definition and will only recapitulate some notions here.
+specify games in a compact, prolog-like way. The GDL syntax and
+semantics are defined in \cite{GLP05,LHHSG08}, we refer the reader
+there for the definition and will only recapitulate some notions
+here. When we build first-order formulas over GDL atoms during
+intermediate steps of translation, they are intended to be interpreted
+in already existing GDL models (which are defined in
+\cite{GLP05,LHHSG08}).
 
 The state of the game in GDL is defined by the set of propositions
 true in that state. These propositions are represented by terms of
@@ -1133,6 +1137,7 @@
 the second arguments of \texttt{legal} and \texttt{does} relations,
 \ie those terms which are used to specify the moves of the players.
 
+
 The complete Tic-tac-toe specification in GDL is given in
 Figure~\ref{fig-ttt-gdl}. While games can be formalised in various
 ways in both systems, Figures \ref{fig-ttt-code} and \ref{fig-ttt-gdl}
@@ -1762,49 +1767,62 @@
 
 \subsubsection{Rewriting Rule Creation} \label{subsec-rules}
 
-For each suitable tuple $\ol{\calC}, \ol{\calN}$ we have now
-created the unifier $\sigma_{\ol{\calC}, \ol{\calN}}$ and computed
-the erasure clauses $\calE_{\ol{\calC}, \ol{\calN}}$. To create the rules,
-we first collect all atoms in the bodies of
-$\sigma_{\ol{\calC}, \ol{\calN}}(\calC_i), \sigma_{\ol{\calC}, \ol{\calN}}(\calN_i)$
-and $\calE_{\ol{\calC}, \ol{\calN}}$. We generate a Toss rule candidate for
-every partition of atoms into true and false ones, and later \emph{filter}
-these candidates by checking for satisfiability in the initial structure
-of the stable part of the rule matching criteria and precondition.
+For each suitable tuple $\ol{\calC}, \ol{\calN}$ we have now created
+the unifier $\sigma_{\ol{\calC}, \ol{\calN}}$ and computed the erasure
+clauses $\calE_{\ol{\calC}, \ol{\calN}}$. To create the rules, we need
+to further partition the \emph{rule clauses} $\sigma_{\ol{\calC},
+  \ol{\calN}}(\calC_i), \sigma_{\ol{\calC}, \ol{\calN}}(\calN_i)$ and
+$\calE_{\ol{\calC}, \ol{\calN}}$, and augment them with further
+conditions. The reason is that the prepared rule clauses may have
+different matches in different game states, while the Toss rule has to
+be built from all the rule clauses that would match when the Toss rule
+matches. Therefore, we need to build a Toss rule for each subset of
+rule clauses that are ``selected'' by some game state (i.e. are
+exactly the rule clauses matching in that state), but add to it
+``separation conditions'' that prevent the Toss rule from matching in
+game states where more rule clauses can match.
 
-For a given a partition of GDL atoms into true and false ones,
-we will construct the candidate rule in two steps.
+We select groups of atoms (collected from rule clauses) that separate
+rule clauses, and generate a Toss rule candidate for every partition
+of the groups into true and false ones: we collect the rule clauses
+that agree with the given partition. The selected atoms, some negated
+according to the partition, form the separation condition.
 
-In the first step, we transform the GDL atoms into Toss clauses.
-This translation follows the definitions of atomic relations
-presented in Section~\ref{subsec-rels}, and the relations there were
-chosen so as to suffice for this translation. Due to space constraints
-we omit further technical details of this step here.
-%Before creating the rules, we currently expand (inline)
-%relations of $G$ that directly or indirectly depend on game state, and
-%we instantiate variables at fluent paths. We translate state terms
-%as Toss variables, so that terms are translated as the same variable
-%iff they are syntactically equal or differ only at fluent paths.
+For each candidate, we will construct the Toss rule in two steps.
 
-In the second step, we use Toss clauses to construct the structures
-for the rule. The $\frakL$-structure and precondition of a Toss rewrite rule
-is built by first translating the existential closure of conjunctions of
-bodies of \texttt{next} clauses of the rule. Based on the heads of
-\texttt{next} clauses, the relevant information is extracted from the
-resulting precondition formula and quantification over variables
-corresponding to $\frakL$ elements is dropped. The right-hand
-structure is constructed similarly.
+In the first step we generate the \emph{matching condition}: we
+translate the conjunction of the bodies of rule clauses and the
+separation condition. This translation follows the definitions of
+atomic relations presented in Section~\ref{subsec-rels} and is
+described in Section~\ref{subsec-translate}.
 
-Having constructed and filtered the rewriting rule candidates,
-we have almost completed the definition of $T(G)$. The rules
-are assigned to locations based on who moves in which location,
-as we only translate turn-based games for now. Payoff formulas
-are derived by instantiating variables standing for the \texttt{goal}
-values. The formulas defining the \texttt{terminal} condition and
-specific \texttt{goal} value conditions are existential closures of
-disjunctions of bodies of their respective clauses.
+Later we \emph{filter} the rule candidates by checking for
+satisfiability in the initial structure of the stable part of the
+matching condition.
 
+In the second step, we build a Toss rewrite rule itself. From the
+heads of rule clauses of a rule candidate, we build the
+$\frakR$-structure: each \texttt{next} term, with its fluent paths
+replaced by \texttt{BLANK}, is an $\frakR$ element, and the fluent
+predicates holding for the \texttt{next} state terms are the relations
+of $\frakR$. The $\frakL$-structure and precondition of the Toss rule
+is built from the matching condition, based on elements of $\frakR$.
+Quantification over variables corresponding to $\frakR$ elements
+(which are the same as $\frakL$ elements) is dropped, and atoms
+involving only these variables and not occurring inside disjunctions
+are extracted to be relations tuples in $\frakL$.
 
+Having constructed and filtered the rewriting rule candidates, we have
+almost completed the definition of $T(G)$. The rules are assigned to
+locations based on who moves in which location, as we only translate
+turn-based games for now. Payoff formulas are derived by instantiating
+variables standing for the \texttt{goal} values. The formulas defining
+the \texttt{terminal} condition and specific \texttt{goal} value
+conditions are translated as described in
+Section~\ref{subsec-translate}, from disjunctions of bodies of their
+respective clauses.
+
+
 \subsection{Translating Moves between Toss and GDL} \label{subsec-move-tr}
 
 To play as a GDL client, we need to translate legal moves from $G$
@@ -1828,7 +1846,30 @@
 such that $t\tpos_p = v$, and $a\tpos^m_p = s$, then we substitute
 $v$ by $s$. The move translation function $\mu$ is thus constructed.
 
+\subsection{Translating Formulas} \label{subsec-translate}
 
+\subsubsection{Stable Relations and Fluents}
+
+Divide Phi into the part other than \texttt{true}: LitsPhi (can
+contain disjunctions), positive \texttt{true} literals: Tru+ and
+negative \texttt{true} literals: Tru-.
+
+Translate conjunctions as conjunctions, and disjunctions as disjunctions.
+
+Translate TrLits(Phi, Tru1, Tru2) by translating each literal as a
+conjunction of literals, for every combination of mask paths into Tru1
+terms, such that at least one of the terms is from Tru2.
+
+Translate \texttt{true} atoms as a conjunction of their anchor and
+fluent predicates TrTru.
+
+Translate the whole Phi as ``ex Tru+ (TrLits(LitsPhi, Tru+, Tru+) and
+conj of TrTru(Tru+) and TrLits(ex Tru- (not (TrLits(LitsPhi, Tru+ sum
+Tru-, Tru-) and disj of TrTru(Tru-)))))''.
+
+\subsubsection{Introducing and Using Defined Relations}
+
+
 \section{Game Simplification in Toss}
 
 Games automatically translated from GDL, as described above, are verbose


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.