[Toss-devel-svn] SF.net SVN: toss:[1543] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1543] trunk/Toss
|
From: <luk...@us...> - 2011-08-21 10:27:44
|
Revision: 1543
http://toss.svn.sourceforge.net/toss/?rev=1543&view=rev
Author: lukstafi
Date: 2011-08-21 10:27:37 +0000 (Sun, 21 Aug 2011)
Log Message:
-----------
GDL translation: revised specification of translating as defined relations; fix in GDL.ml related to finding fluents; literal translation handling Distinct.
Modified Paths:
--------------
trunk/Toss/GGP/GDL.ml
trunk/Toss/GGP/TranslateFormula.ml
trunk/Toss/GGP/TranslateFormula.mli
trunk/Toss/GGP/TranslateFormulaTest.ml
trunk/Toss/GGP/TranslateGame.ml
trunk/Toss/GGP/TranslateGame.mli
trunk/Toss/GGP/TranslateGameTest.ml
trunk/Toss/www/reference/reference.tex
Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml 2011-08-18 09:30:20 UTC (rev 1542)
+++ trunk/Toss/GGP/GDL.ml 2011-08-21 10:27:37 UTC (rev 1543)
@@ -749,9 +749,10 @@
let br_vars = gdl_defs_vars ["",brs] in
let sb = List.map
(fun v ->
- v, Aux.not_conflicting_name ~truncate:true !used_vars v)
+ let nv = Aux.not_conflicting_name ~truncate:true !used_vars v in
+ used_vars := Aux.Strings.add nv !used_vars;
+ v, nv)
(Aux.Strings.elements br_vars) in
- used_vars := Aux.add_strings (List.map snd sb) !used_vars;
let sb = List.map (fun (v,t) -> v, Var t) sb in
List.map (subst_br sb) brs in
let expand_atom (rel, args as atom)
Modified: trunk/Toss/GGP/TranslateFormula.ml
===================================================================
--- trunk/Toss/GGP/TranslateFormula.ml 2011-08-18 09:30:20 UTC (rev 1542)
+++ trunk/Toss/GGP/TranslateFormula.ml 2011-08-21 10:27:37 UTC (rev 1543)
@@ -58,7 +58,7 @@
(* Whether $i$th argument is a $\mathrm{DefSide}$ or a
$\mathrm{CallSide}$, and the $p_{R,i}$ path for a relation $R$. *)
-type defrel_arg_type = (bool * path) array
+type defrel_arg_mode = (bool * path) array
type transl_data = {
f_paths : path_set; (* fluent paths *)
@@ -66,8 +66,8 @@
all_paths : path_set; (* sum of f_paths and m_paths *)
mask_reps : term list; (* mask terms *)
defined_rels : string list;
- defrel_arg_type : (string * defrel_arg_type) list ref;
- (* late binding to store $ArgType# data *)
+ defrel_arg_mode : (string * defrel_arg_mode) list ref;
+ (* late binding to store $ArgMode# data *)
term_arities : (string * int) list;
rel_default_path : (string * path option array) list;
}
@@ -78,7 +78,7 @@
all_paths = empty_path_set;
mask_reps = [];
defined_rels = [];
- defrel_arg_type = ref [];
+ defrel_arg_mode = ref [];
term_arities = [];
rel_default_path = [];
}
@@ -159,9 +159,30 @@
| Neg (Rel (rel, args)) -> transl_posdefrel false rel args
| Pos (Does _ | Role _) | Neg (Does _ | Role _) ->
[]
+ | Pos (Distinct ts) ->
+ let res =
+ Array.mapi (fun i t_i ->
+ if i = 0 then []
+ else aux (Neg (Rel ("EQ_", [|ts.(0); t_i|])))) ts in
+ List.concat (Array.to_list res)
+ | Neg (Distinct ts) ->
+ (* they shouldn't do it but since they did... *)
+ let res =
+ Array.mapi (fun i t_i ->
+ if i = 0 then []
+ else aux (Pos (Rel ("EQ_", [|ts.(0); t_i|])))) ts in
+ List.concat (Array.to_list res)
| Disj lits ->
- [Formula.Or (Aux.concat_map (fun l -> aux l) lits)]
- | _ -> assert false in (* FIXME: what about Distinct? *)
+ [Formula.Or (Aux.concat_map aux lits)]
+ | lit ->
+ (* {{{ log entry *)
+ if !debug_level > 0 then (
+ Printf.printf "transl_rels: Unhandled literal %s\n%!"
+ (literal_str lit)
+ );
+ (* }}} *)
+ [] (* assert false *)
+ in
Formula.And (Aux.concat_map aux rels_phi)
let transl_state data phi =
@@ -211,6 +232,11 @@
let neg_terms = state_terms neg_state_phi in
let neg_vars =
Aux.list_diff (List.map (var_of_term data) neg_terms) pos_vars in
+ let neg_ext, pos_ext = List.partition
+ (fun conj ->
+ List.exists (fun v->List.mem v (neg_vars :> Formula.var list))
+ (FormulaOps.free_vars conj))
+ ext_phi in
let all_terms = pos_terms @ neg_terms in
let phi_vars = clause_vars
(("", [| |]),
@@ -225,7 +251,7 @@
(clause_str (("rels_phi", [||]),rels_phi))
(clause_str (("pos_state_phi", [||]),pos_state_phi))
(clause_str (("neg_state_phi", [||]),neg_state_phi))
- ("ext_phi="^Formula.str ext_phi)
+ ("ext_phi="^Formula.str (Formula.And ext_phi))
);
(* }}} *)
let negated_neg_state_transl =
@@ -233,21 +259,23 @@
Formula.Or (
List.map (transl_state data) (nnf_dnf neg_state_phi)) in
let negated_part =
- Formula.And [
- (* positive because they form a "premise" *)
- transl_rels data rels_eqs all_terms neg_terms;
- (* the universal "conclusion" *)
- negated_neg_state_transl] in
+ Formula.And (
+ neg_ext @
+ [
+ (* positive because they form a "premise" *)
+ transl_rels data rels_eqs all_terms neg_terms;
+ (* the universal "conclusion" *)
+ negated_neg_state_transl]) in
let universal_part =
- if neg_terms = [] then []
+ if neg_terms = [] && neg_ext = [] then []
else if neg_vars = []
then [Formula.Not negated_part]
else [Formula.Not (
Formula.Ex ((neg_vars :> Formula.var list), negated_part))] in
let base_part =
Formula.And (
- [ ext_phi;
- transl_rels data rels_eqs pos_terms pos_terms;
+ pos_ext @
+ [ transl_rels data rels_eqs pos_terms pos_terms;
transl_state data pos_state_phi] @
universal_part) in
if pos_vars = [] then base_part
@@ -259,7 +287,7 @@
let translate data disj =
let disj = separate_disj disj in
Formula.Or (List.map (fun (rels_phi, pos_state, neg_state) ->
- transl_disjunct data rels_phi pos_state neg_state (Formula.And [])
+ transl_disjunct data rels_phi pos_state neg_state []
) disj)
@@ -269,7 +297,7 @@
let select_defrel_argpaths data all_branches =
(* TODO: code-review this and [build_defrel] functions *)
let select_for_defrel rel =
- (* searching for ArgType = DefSide,S,p *)
+ (* searching for ArgMode = DefSide,S,p *)
let branches = Aux.assoc_all rel all_branches in
(* {{{ log entry *)
if !debug_level > 2 then (
@@ -306,7 +334,7 @@
) sterms))
args p_defside in
let s_defside = List.map branch_sterms branches in
- (* now computing the ArgType(R,i) = CallSide,p variant *)
+ (* now computing the ArgMode(R,i) = CallSide,p variant *)
let call_branches = Aux.concat_map
(fun (_,(_, (phi, _, _ as body))) ->
let calls = Aux.assoc_all rel (rel_atoms phi) in
@@ -341,7 +369,7 @@
match defside, callside with
| Some p, _ | None, Some p -> p
| None, None ->
- (* the ArgType(R,i) = NoSide,p variant is precomputed *)
+ (* the ArgMode(R,i) = NoSide,p variant is precomputed *)
try
match (List.assoc rel data.rel_default_path).(i) with
| Some p -> p
@@ -352,11 +380,11 @@
"TranslateFormula.build_defrels: could not \
determine path for relation %s argument %d" rel i)
) p_defside in
- let defrel_arg_type = Aux.array_map2
+ let defrel_arg_mode = Aux.array_map2
(fun defside path -> defside <> None, path)
p_defside arg_paths in
- data.defrel_arg_type :=
- (rel, defrel_arg_type) :: !(data.defrel_arg_type);
+ data.defrel_arg_mode :=
+ (rel, defrel_arg_mode) :: !(data.defrel_arg_mode);
rel, (p_defside, s_defside, arg_paths) in
List.map select_for_defrel data.defined_rels
@@ -386,7 +414,7 @@
Formula.Eq (v, s_i)
else Formula.Eq (v, var_of_subterm data arg_paths.(i) args.(i)))
defvars in
- let arg_eqs = Formula.And (Array.to_list arg_eqs) in
+ let arg_eqs = Array.to_list arg_eqs in
let callside_sterms = (* $S_{j,l}$ *)
Aux.array_mapi_some
(fun i path ->
@@ -411,20 +439,20 @@
(rel_atom_str (rel, args)) sign
);
(* }}} *)
- let arg_type = List.assoc rel !(data.defrel_arg_type) in
+ let arg_mode = List.assoc rel !(data.defrel_arg_mode) in
(* the $s \tpos_{p_{R,i}} = t_i$ state terms *)
let arg_sterms = Array.mapi
(fun i (defside, path) -> if defside then None else
try Some (
List.find (fun s -> at_path s path = args.(i)) sterms_all)
with Not_found -> None)
- arg_type in
+ arg_mode in
let var_args = Array.mapi
(fun i (_, path) ->
match arg_sterms.(i) with
| None -> var_of_subterm data path args.(i) (* in J *)
| Some sterm -> var_of_term data sterm)
- arg_type in
+ arg_mode in
let defrel_phi = Formula.Rel (rel, var_args) in
let defrel_phi =
if sign then defrel_phi else Formula.Not defrel_phi in
@@ -432,7 +460,7 @@
(Aux.array_mapi_some (fun i (_,path) ->
if arg_sterms.(i) = None
then Some (var_of_subterm data path args.(i))
- else None) arg_type) in
+ else None) arg_mode) in
let in_J_eq_transl i (_,path) =
if arg_sterms.(i) = None
then
@@ -441,7 +469,7 @@
Some (transl_rels data eq_phi (v::sterms_all) [v])
else None in
let eqs_phi = Array.to_list
- (Aux.array_mapi_some in_J_eq_transl arg_type) in
+ (Aux.array_mapi_some in_J_eq_transl arg_mode) in
let base =
if eqs_phi = [] then defrel_phi
else Formula.And (defrel_phi::eqs_phi) in
Modified: trunk/Toss/GGP/TranslateFormula.mli
===================================================================
--- trunk/Toss/GGP/TranslateFormula.mli 2011-08-18 09:30:20 UTC (rev 1542)
+++ trunk/Toss/GGP/TranslateFormula.mli 2011-08-21 10:27:37 UTC (rev 1543)
@@ -2,7 +2,7 @@
(* Whether $i$th argument is a $\mathrm{DefSide}$ or a
$\mathrm{CallSide}$, and the $p_{R,i}$ path for a relation $R$. *)
-type defrel_arg_type = (bool * GDL.path) array
+type defrel_arg_mode = (bool * GDL.path) array
type transl_data = {
f_paths : GDL.path_set; (** fluent paths *)
@@ -10,8 +10,8 @@
all_paths : GDL.path_set; (** sum of f_paths and m_paths *)
mask_reps : GDL.term list; (** mask terms *)
defined_rels : string list;
- defrel_arg_type : (string * defrel_arg_type) list ref;
- (** late binding to store $ArgType$ data *)
+ defrel_arg_mode : (string * defrel_arg_mode) list ref;
+ (** late binding to store $ArgMode$ data *)
term_arities : (string * int) list;
rel_default_path : (string * GDL.path option array) list;
}
Modified: trunk/Toss/GGP/TranslateFormulaTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateFormulaTest.ml 2011-08-18 09:30:20 UTC (rev 1542)
+++ trunk/Toss/GGP/TranslateFormulaTest.ml 2011-08-21 10:27:37 UTC (rev 1543)
@@ -66,7 +66,7 @@
all_paths = all_paths;
mask_reps = mask_reps;
defined_rels = defined_rels;
- defrel_arg_type = ref [];
+ defrel_arg_mode = ref [];
term_arities = term_arities;
rel_default_path = rel_default_path;
}
Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml 2011-08-18 09:30:20 UTC (rev 1542)
+++ trunk/Toss/GGP/TranslateGame.ml 2011-08-21 10:27:37 UTC (rev 1543)
@@ -26,11 +26,6 @@
let debug_level = ref 0
let generate_test_case = ref None
-(** Translate static relations that otherwise would be translated as
- structure relations, but have arity above the threshold, as
- defined relations. *)
-let defined_arity_above = ref 2
-
(** Treat "next" clauses which introduce a fluent position for a
variable-variable mismatch, as non-erasing frame clauses (to be
ignored). ("Wave" refers to the process of "propagating the frame
@@ -38,6 +33,13 @@
[nonerasing_frame_wave] is set to [true].) *)
let nonerasing_frame_wave = ref true
+(** two heuristics for selecting defined relations: select relations
+ with arity smaller than three; or, select relations that have ground
+ defining clauses (i.e. defining clauses with empty bodies). *)
+type as_defined_rels =
+ Many_by_arity | Few_by_ground_def | Fewer_by_all_ground
+let as_defined_rels = ref Few_by_ground_def
+
(** When translating as turn-based, filter-out moves composed only of
actions such that each is a "noop" action of some player at some
location. Assumes that players do not use their "noop" actions
@@ -326,9 +328,16 @@
let m_pathl = paths_to_list m_paths in
let f_pathl = paths_to_list f_paths in
(* adding subterm equality relations and fact relations *)
- let struc_rels, defined_rels =
- List.partition (fun rel ->
- List.assoc rel arities <= !defined_arity_above) static_rels in
+ let struc_rels, defined_rels = List.partition
+ (fun rel ->
+ if !as_defined_rels = Few_by_ground_def
+ then List.exists
+ (fun ((rc,args),body) -> rel=rc && body = []) clauses
+ else if !as_defined_rels = Fewer_by_all_ground
+ then List.for_all
+ (fun ((rc,args),body) -> rel=rc && body = []) clauses
+ else List.assoc rel arities < 3)
+ static_rels in
let struc_rels = "EQ_"::struc_rels in
let defined_rels = defined_rels @ nonstatic_rels in
(* {{{ log entry *)
@@ -1473,7 +1482,7 @@
all_paths = paths_union f_paths m_paths;
mask_reps = mask_reps;
defined_rels = defined_rels;
- defrel_arg_type = ref []; (* built in TranslateFormula *)
+ defrel_arg_mode = ref []; (* built in TranslateFormula *)
term_arities = term_arities;
rel_default_path =
transl_arg_type_no_side defined_rel_arities init_state program
Modified: trunk/Toss/GGP/TranslateGame.mli
===================================================================
--- trunk/Toss/GGP/TranslateGame.mli 2011-08-18 09:30:20 UTC (rev 1542)
+++ trunk/Toss/GGP/TranslateGame.mli 2011-08-21 10:27:37 UTC (rev 1543)
@@ -2,6 +2,13 @@
val debug_level : int ref
val generate_test_case : string option ref
+(** two heuristics for selecting defined relations: select relations
+ with arity smaller than three; or, select relations that have ground
+ defining clauses (i.e. defining clauses with empty bodies). *)
+type as_defined_rels =
+ Many_by_arity | Few_by_ground_def | Fewer_by_all_ground
+val as_defined_rels : as_defined_rels ref
+
(** Limit on plys for both aggregate and random playouts. *)
val playout_horizon : int ref
Modified: trunk/Toss/GGP/TranslateGameTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateGameTest.ml 2011-08-18 09:30:20 UTC (rev 1542)
+++ trunk/Toss/GGP/TranslateGameTest.ml 2011-08-21 10:27:37 UTC (rev 1543)
@@ -215,8 +215,9 @@
]
let a () =
- GDL.debug_level := 4;
+ (* GDL.debug_level := 4; *)
TranslateGame.debug_level := 4;
+ TranslateFormula.debug_level := 4;
GameSimpl.debug_level := 4;
DiscreteRule.debug_level := 4;
()
Modified: trunk/Toss/www/reference/reference.tex
===================================================================
--- trunk/Toss/www/reference/reference.tex 2011-08-18 09:30:20 UTC (rev 1542)
+++ trunk/Toss/www/reference/reference.tex 2011-08-21 10:27:37 UTC (rev 1543)
@@ -1330,8 +1330,8 @@
state. Since an approximation is sufficient, we check only the
positive part of the legality condition of each move.
-In the future, instead of an aggregate playout we
-might use a form of type inference to approximate $\calS$.
+% In the future, instead of an aggregate playout we
+% might use a form of type inference to approximate $\calS$.
To construct the elements of the structure from state terms,
and to make that structure a good representation of the game in Toss,
@@ -1628,11 +1628,11 @@
% formulas.
%\end{definition}
-\subsection{Expanding the GDL Game Definition}
+\subsection{Expanding the GDL Game Definition}\label{expanding-gamedef}
Prior to further processing, we modify the wave clauses of the
game. Let $\calN \in \mathrm{Next}_{W}$, we add to the body of $\calN$
-a \texttt{true} atom $(\mathtt{true} \ BL(s_\calN)$ (where
+a \texttt{true} atom $(\mathtt{true} \ BL(s_\calN))$ (where
$\mathtt{BL}(t)=t\big[\calP_f \ot \mathtt{BLANK}\big]$). The added
state term will be the corresponding LHS element of the RHS element
introduced by the clause.
@@ -1669,6 +1669,10 @@
replace the atom by a disjunction of corresponding atoms, or if it is
a negative literal, by a conjunction of negated atoms.
+For simplicity, we still refer to the transformed definition as $G$,
+but it is to be understood as the result of transformation $G'$
+equivalent to the original game definition $G$.
+
\subsection{Structure Rewriting Rules}
To create the structure rewriting rule for the Toss game,
@@ -1958,12 +1962,16 @@
\subsection{Translating Formulas} \label{subsec-translate}
-First we describe translation in the case all GDL relations other than
-\texttt{next} are stable, \ie do not even indirectly depend on
-\texttt{true}. A stable GDL relation is translated as multiple stable
-Toss relations. Then we approach the GDL relations (other than
-\texttt{next}) that depend on \texttt{true} by translating them as
-defined relations in Toss.
+We translate a GDL relation as either multiple Toss stable relations
+(\ie structure relations that do not change during the game), or as
+Toss defined relation (\ie a relation given by its defining formula).
+All GDL relations that even indirectly depend on \texttt{true} need to
+be translated as defined relations. Of the remaining relations, we
+select the ones to be translated as structure (stable) relations
+heuristically. Currently, a parameter of the translation allows to:
+select relations with arity smaller than three; or, select relations
+whose (some, or all) defining clauses are ground (\ie with empty
+bodies).
\subsubsection{Stable Relations and Fluents}
@@ -1993,23 +2001,22 @@
is translated as:
\begin{align*}
- \mathrm{Tr}(\Phi_i,E) :=
+ \mathrm{Tr}(\Phi_i) :=
\exists \mathtt{BL}(\mathtt{ST}(ST^{+}_i)) \big( &
- E \wedge
+ \wedge
\TrRels(eqs_i \wedge G_i, \mathtt{ST}(ST^{+}_i), \mathtt{ST}(ST^{+}_i))
\wedge \TrST(ST^{+}_i) \wedge \\ &
- \neg \exists \big( \mathtt{BL}(\mathtt{ST}(ST^{-}_i)) \setminus
- \mathtt{BL}(\mathtt{ST}(ST^{+}_i)) \big) \big( \\ &
-\ \ \ \ \ \ \ \
-\TrRels(eqs_i \wedge G_i, \mathtt{ST}(ST^{+}_i) \cup
+ \neg \exists V^{-} \big(
+ \wedge \TrRels(eqs_i \wedge G_i, \mathtt{ST}(ST^{+}_i) \cup
\mathtt{ST}(ST^{-}_i), \mathtt{ST}(ST^{-}_i)) \wedge \\ &
\ \ \ \ \ \ \ \
-\TrST(\mathtt{NNF}(\neg ST^{-}_i)) \big) \big)
+\TrST(\mathtt{NNF}(\neg ST^{-}_i)) \big) \big) \\
+V^{-} & := \big( \mathtt{BL}(\mathtt{ST}(ST^{-}_i)) \setminus
+ \mathtt{BL}(\mathtt{ST}(ST^{+}_i)) \big)
\end{align*}
The result of translation is $\mathrm{Tr}(\Phi) :=
-\mathrm{Tr}(\Phi_1,T) \vee \ldots \vee \mathrm{Tr}(\Phi_n,T)$
-(argument $E$ is for later use).
+\mathrm{Tr}(\Phi_1) \vee \ldots \vee \mathrm{Tr}(\Phi_n)$.
We now proceed to define $\TrRels$ and $\TrST$. For an atom $r$, let
$\pm r$ mean either $r$ or $\neg r$ when on the left-hand-side, and
@@ -2027,7 +2034,7 @@
v_1 = \mathtt{BL}(s_1) \wedge \ldots \wedge v_n = \mathtt{BL}(s_n) \wedge \\
& p_1, \ldots, p_n \in \calP_m \wedge
s_1 \tpos_{p_1} = t_1 \wedge \ldots \wedge s_n \tpos_{p_n} = t_n \big\} \\
- & \textit{(when $R$ is a stable relation)} \\
+ & \textit{(when $R$ is not translated as defined relation)} \\
\TrST (\phi_1 \wedge \phi_2) = &
\TrST (\phi_1) \wedge \TrST(\phi_2) \\
\TrST (\phi_1 \vee \phi_2) = &
@@ -2044,109 +2051,113 @@
Mask_m(v) \; \big| \; v = \mathtt{BL}(t) \wedge t \in m \big\}
\end{align*}
-The case of $\TrRels$ for non-stable relations will be covered in the
-next section.
+The case of $\TrRels$ for relations intended to be translated as
+defined relations will be covered in the next section.
\subsubsection{Introducing and Using Defined Relations}
+Prior to translating formulas that use the defined relations, we need
+to transform the game definition, iteratively for each defined
+relation in the partial order of the ``call graph'', \ie whenever
+possible doing the transformation for a relation before doing it for
+relations used to define it. (We keep the convention from
+Section~\ref{expanding-gamedef}, that $G$ is substituted with the
+transformed definitions.)
+
+\paragraph{State Terms to Transfer Arguments}
+
Consider generating defined relation for relation $R$ with GDL defining clauses
-\[ \mathtt{(<= (R \ t^1_1 \ldots t^1_n) \ b_1)},
- \ldots, \mathtt{(<= (R \ t^k_1 \ldots t^k_n) \ b_k)}.\]
-For the $i$th argument of $R$ ($i \in \{1,\ldots,n\}$) we will find
-$\mathtt{ArgType}(R,i)$ with possible values
-$(\mathtt{DefSide},\calS_i,p_i)$, $(\mathtt{CallSide},p_i)$ and $(\mathtt{NoSide},p_i)$, with a mapping $\calS_i$ into state terms
-corresponding to the argument in a given context and a path $p_i \in
-\calP_m$ corresponding to the subterm position selected to
-``transfer'' the argument.
+\[ \mathtt{(<= (R \ t^1_1 \ldots t^1_n) \ b_1)}, \ldots, \mathtt{(<=
+ (R \ t^k_1 \ldots t^k_n) \ b_k)}.\] Let all atoms of $R$ in $G$
+(including both the heads $(R \ t^j_1 \ldots t^j_n)$, and inside of
+$b_j$ above) be $\calR=\big\{(R \ r^1_1 \ldots r^1_n),\ldots,(R \
+r^K_1 \ldots r^K_n)\big\}$. Based on $\calR$ we will find a partition
+of argument positions and an assignment of mask paths to positions
+$(a_1,p_1),\ldots,(a_n,p_n)$ such that $a_1=1$, $a_{i+1}-a_i \in \{0,1\}$, for any partition $\calI = \{i
+\ | \ a_i = I\}$, the paths $(p_i \ | \ i \in \calI)$ are distinct and
+do not conflict, \ie $(\exists s) (\forall p_i \ | \ i \in \calI) \
+s\tpos_{p_i}$. GDL arguments of a single partition will be passed as a
+single defined relation argument.
-Let $\mathrm{TrDistr}(b_j) = \Phi^j_1 \vee \ldots \vee \Phi^j_{m_j}$
-where $\Phi^j_l = G^j_l \wedge ST^{j+}_l \wedge ST^{j-}_l$. Let
-$\calS_i$ be a mapping from $(j,l)$ to $s^i_{j,l} \in
-\mathtt{ST}(ST^{j+}_l)$ and $p_i \in \calP_m$ a path such that
-$s^i_{j,l} \tpos_{p_i} = t^j_i$. If such a path and (total for $j,l$)
-mapping exist, then $\mathtt{ArgType}(R,i) =
-(\mathtt{DefSide},\calS_i,p_i)$.
+To find the paths and the partition, consider a clause body
+$\mathtt{b}$, any occurrence of relation $R$ atom $(R \ r^j_1 \ldots
+r^j_n)$ in $\mathtt{b}$ and positive literal $(\mathtt{true} \ s) \in
+\mathtt{b}$ (where the literal is not under disjunction). Let $\{p,i \
+| \ s \tpos_p = r^j_i \}$. We count such sets of paths for all
+$\mathtt{b}$ and positive $(\mathtt{true} \ s) \in \mathtt{b}$. We
+greedily select sets that together cover all argument positions, with
+highest size, and of equally sized with highest count. Of these, we
+build the partition by removing from the sets the path-position pairs
+where the position is already present in remaining path-position
+pairs, in order reverse to the selection criterion.
-Otherwise, let $r = R(u_1,\ldots,u_n)$ be an atom of $R$ occurring in
-a $\Phi_d = G \wedge ST^{+} \wedge ST^{-}$ disjunct of
-$\mathrm{TrDistr}$ result for arbitrary clause of the GDL game
-definition. Let $\calS_i(p)$ be a mapping from $\Phi_d$ to
-$s^i_{\Phi_d} \in \mathtt{ST}(ST^{+})$ with $p \in \calP_m$ a path
-such that $s^i_{\Phi_d} \tpos_p = u_i$, whenever such $s^i_{\Phi_d}
-\in \mathtt{ST}(ST^{+})$ exists. Let $p_i$ be such that the size of
-the domain of $\calS_i(p_i)$ is maximal. Set $\mathtt{ArgType}(R,i) =
-(\mathtt{CallSide},p_i)$.
+In case no set of paths contains a path for the $i$th argument, we set
+the path $p_i \in \calP_m$ (with a unique $a_i$) so that the
+intersection of the projection of the graph of $R$ for the initial
+game state $g_{R,i} = \{s | G \vdash R(t_1,\ldots,t_n) \textit{ for
+ any } \ol{t} \textit{ s.t. } t_i = s\}$, and the set of subterms of
+state terms at path $p_i$, $g_{p_i} = \{s \tpos_{p_i} | s \in
+\calS\}$, is maximal w.r.t. cardinality ($p_i = \arg \max_{p \in
+ \calP_m} \left| g_{R,i} \cap g_p \right|$).
-In case neither $\mathtt{DefSide}$ nor $\mathtt{CallSide}$ approach is
-satisfactory, we set $\mathtt{ArgType}(R,i) = (\mathtt{NoSide},p_i)$,
-where the path $p_i \in \calP_m$ is selected so that the intersection
-of the projection of the graph of $R$ for the initial game state
-$g_{R,i} = \{s | G \vdash R(t_1,\ldots,t_n) \textit{ for any }
-\ol{t} \textit{ s.t. } t_i = s\}$, and the set of subterms of state
-terms at path $p_i$, $g_{p_i} = \{s \tpos_{p_i} | s \in \calS\}$, is
-maximal w.r.t. cardinality ($p_i = \arg \max_{p \in \calP_m} \left|
- g_{R,i} \cap g_p \right|$).
+Ideally, $p_i \in \calP_m$ should be a path whose domain, \ie the set
+$\big\{t \big| s\tpos_{p_i} = t, s \in \calS\big\}$, contains the
+domain of the $i$th argument of $R$, \ie the sum of projections of $R$
+on $i$th argument for all possible game states. We do not guarantee
+this.
-For correctness, $p_i \in \calP_m$ should be a path whose domain, \ie
-the set $\big\{t \big| s\tpos_{p_i} = t, s \in \calS\big\}$, contains
-the domain of the $i$th argument of $R$, \ie the sum of projections of
-$R$ on $i$th argument for all possible game states. The current
-definition above does not guarantee this; the exact implementation may
-further evolve as $\mathtt{ArgType}$ is relevant for the quality of
-translation (\ie both for correctness and how many simplifications can
-be applied, see Section~\ref{sec-game-simpl}).
+Once the paths for arguments have been selected, we make sure that a
+clause in $G$ that has an atom $(R \ r^1_1 \ldots r^1_n)$, has the
+positive literals $(\mathtt{true} \ s_\calI)$ such that $\bigwedge_{i
+ \in \calI} s_\calI \tpos_{p_i} = r^j_i$. For every $\calI$ for which
+such a positive literal does not occur in the clause body, we add an
+atom $\big(\mathtt{true} \ \mathtt{BL}(\{p_i \ot r^j_i \ | \ i \in
+\calI\})\big)$ to the clause. The notation $\mathtt{BL}(\{p_i \ot t_i \ | \
+i \in \calI\})$ for a paths $p_i$ and terms $t_i$ denotes a state term
+containing $t_i$ at path $p_i$, and $\mathtt{BLANK}$ as subterms at
+all its positions that are not on any path $p_i$ (\ie are not prefixes
+of any $p_i$).
-We are ready to provide the translated definition $R_{def}$. Let
-$v_1,\ldots,v_n$ be fresh Toss variables, let $\calI_R = \big\{i
-\big| \mathtt{ArgType}(R,i) =
-(\mathtt{DefSide},\calS_i,p_i)\big\}$ and $p_{R,i}$ be such that
-$\mathtt{ArgType}(R,i) =
-(\mathtt{DefSide},\calS_i,p_{R,i})$ or $\mathtt{ArgType}(R,i) =
-(\mathtt{CallSide},p_{R,i})$. Let $\mathtt{BL}(p \ot t)$ for
-a path $p$ and term $t$ be a state term containing $t$ at path $p$,
-and $\mathtt{BLANK}$ as subterms at all its positions that are not on
-path $p$ (\ie are not prefixes of $p$). Using notation introduced
-above, let
+\paragraph{Translating Defined Relations}
+Recall the definitions introduced above to generate state terms to
+transfer arguments for translating a relation $R$ as defined
+relation. Let $(a_1,p_1),\ldots,(a_n,p_n)$ be the partition of $R$
+arguments and their paths, $a_n = N$, and $\calI_m = \{i \ | \ a_i = m\}$ (for $m \in \{1,\ldots,N\}$). Let
+$v_1,\ldots,v_N$ be fresh Toss variables.
+
+Recall that each $(R \ t^l_1 \ldots t^l_n)$ is also a $(R \ r^{j_l}_1
+\ldots r^{j_l}_n) \in \calR$ for some $j_l$. Therefore, there exist
+positive \texttt{true} literals $(\mathtt{true} \
+s^l_1),\ldots,(\mathtt{true} \ s^l_N)$ in the body $b_l$ such that
+$(\forall p_i \ | \ i \in \calI_m) \ s^l_m\tpos_{p_i}$. Let $V^l =
+\{\mathtt{BL}(s^l_1),\ldots,\mathtt{BL}(s^l_N)\}$. The translated definition
+$R_{def}$ is:
+
\begin{align*}
-E_{j,l} = &
- \bigwedge \big\{v_i=s^i_{j,l} \big| i \in \calI\big\} \wedge
- \bigwedge\big\{v_i=\mathtt{BL}(p_i \ot t^j_i) \big|
- i \in \{1,\ldots,n\} \setminus \calI\big\} \\
-S_{j,l} = &
-\bigwedge\big\{\mathtt{true}\big(\mathtt{BL}(p_i \ot t^j_i)\big) \big|
-i \in \{1,\ldots,n\} \setminus \calI\big\}
+ R_{def}(v_1,\ldots,v_N) = &
+ \mathrm{TrDefR}((<= (R \ t^1_1 \ldots t^1_n) \ b_1)) \\
+ & \vee \ldots \vee \\
+ & \mathrm{TrDefR}((<= (R \ t^k_1 \ldots t^k_n) \ b_k)) \\
+ \mathrm{TrDefR}((<= (R \ t_1 \ldots t_n) \ b)) = & (\exists{V^l})\big(
+ v_1=\mathtt{BL}(s_1) \wedge \ldots \wedge v_N=\mathtt{BL}(s_N) \wedge
+ \mathtt{Erase}_{V^l} (\mathtt{Tr}(b_l)) \big)
\end{align*}
+where $\mathtt{Erase}_V(\phi)$ erases all quantification over
+variables from $V$ in formula $\phi$.
-The translation is:
+It remains to define $\TrRels$ for the case of defined relations. Let
+$R$ be $N$, $p_1,\ldots,p_n$, $\calI_1,\ldots,\calI_N$ be as
+introduced for $R$. Since $(R \ r_1 \ldots r_n) \in \calR$, there
+exist $s_1,\ldots,s_N \in \calS_1$ such that $(\forall p_i \ | \ i \in
+\calI_m) \ s_m\tpos_{p_i}$. Put
\[
-R_{def}(v_1,\ldots,v_n) =
-\mathrm{Tr}(S_{1,1} \wedge \Phi^1_1,E_{1,1}) \vee \ldots
-\vee \mathrm{Tr}(S_{k,m_k} \wedge \Phi^k_{m_k},E_{k,m_k})
+ \TrRels (\pm R(r_1, \ldots, r_n), S_1, S_2) =
+ \pm R_{def}(\mathtt{BL}(s_1),\ldots,\mathtt{BL}(s_N)).
\]
-It remains to define $\TrRels$ for the case of non-stable GDL relations:
-\begin{align*}
- \TrRels (\pm R(t_1, \ldots, t_n), S_1, S_2) = &
- \exists \{v_i \ | \ i \in \calJ \} \big(
- \pm R_{def}(v_1, \ldots, v_n) \wedge \\ &
- \Land \big\{
- \TrRels (\mathtt{EQ}(t_i,t_i),
- S_1 \cup \{v_i\}, \{v_i\})
- \ \big| \ i \in \calJ \big\} \big) \\ &
- \textit{(when $R$ is not a stable relation)} \\
- \textit{where} \\
- \calJ = &
- \big\{i \ \big| \ i \in \calI_R \vee
- \neg \exists s \in S_1 (s\tpos_{p_{R,i}} = t_i) \big\} \\
- v_i = \mathtt{BL}(p_{R,i}\ot t_i) & \textit{ if } i \in \calJ \\
- v_i = \mathtt{BL}(s) & \textit{ if } i \not\in \calJ
- \textit{ where $s$ such that } s \in S_1 \wedge s\tpos_{p_{R,i}} = t_i
-\end{align*}
-
-
\subsection{Concurrent Moves and Toss Locations} \label{subsec-concurrency}
In Section~\ref{subsec-rules}, we described the creation of
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
