Просмотр кода страницы Value of a schema under interpretation

'''Value of a schema under interpretation''' ---  значение схемы при интерпретации. 

Let <math>\alpha=(G_\alpha, R_\alpha, \Omega_\alpha)</math> be a ''large-block schema''.
For any <math>I\in\Omega_\alpha</math> the schema <math>\alpha</math> can be run. The run consists in the execution instructions
that   results in transformations of the memory state. Every '''memory state''' <math>W</math> defines for any variable <math>x\in X_\alpha</math>
an element <math>W(x)\in D_I</math> called the value of <math>x</math> at <math>W</math>.

Let <math>\Phi</math> be a term and <math>W</math> be a memory state. The value of <math>\Phi</math> at <math>W</math>, denoted by <math>W(\Phi)</math>, is defined by the following
rules:

if <math>\Phi</math> is constant, then <math>W(\Phi)=I(\Phi)</math>;

if <math>\Phi</math> is an operand, then <math>W(\Phi)=W(R_\alpha(\Phi))</math>;

if <math>\Phi= f(\Phi_1, \ldots, \Phi_n</math>, then <math>W(\Phi)=I(f)(W(\Phi_1),\ldots, W(\Phi_n))</math>.

The run of <math>\alpha</math> under <math>I</math> starts with the START instruction whose execution defines the memory state <math>W_1</math>, such that
<math>W_1(x)=I(x)</math> for any <math>x\in X_\alpha</math>, proceeds sequentially by executing the instructions in the order
they occur in some path (called an '''execution sequence''') through <math>G_\alpha</math>, terminates abnormally
with such <math>S_i</math> that <math>W_i(P)=</math> '''false''' for the predicate term <math>P</math> of <math>S_i</math> and the current memory
state <math>W_i</math>, and terminates normally with a STOP instruction. Only in the former  case the '''value of''' <math>\alpha</math> '''under''' <math>I</math>, denoted
<math>val(\alpha, I)</math>, is defined; it is the tuple of current values of the arguments of the STOP instruction.

Let START, <math>S_1, S_2, \ldots,S_i,\ldots</math> and <math>W_1,W_2, \ldots,W_i,\ldots</math> be execution and memory
sequences of <math>\alpha</math> under <math>I</math>. The execution of <math>S_i</math> at <math>W_i</math>, in a general case, consists
in processing the current values of its arguments, replacing some parts of the current values of its results and
defining the next executed instruction (if <math>S_i</math> is a recognizer with a case term <math>\Phi</math> and <math>W_i(\Phi)=r</math>,
<math>S_{i+1}</math> is the  <math>r</math>-th successor of <math>S_i</math>). Let an output <math>d</math> of <math>S-i</math> have a variable <math>x</math> and a data term <math>\Phi</math>.
If <math>d</math> is a strong output, then the newly computed value <math>W_i(\Phi)</math> is assigned to <math>x</math>. If <math>d</math> is a nonstrong output
with an access term <math>g(\Phi_1,\ldots,\Phi_n,\Phi,d)</math>, then a (possible empty) part of the current value <math>W_i(x)</math> of <math>x</math>
is replaced with <math>W_i(\Phi)</math> in such a way that <math>W_{i+1}=W_i(g(\Phi_1,\ldots,\Phi_n,\Phi,d))</math>; the interpretation of <math>g</math>
and the values <math>W_i(g(\Phi_1),\ldots,W_i(\Phi_n)</math> specify the part of <math>x</math> which is replaced with <math>W_i(\Phi)</math>.
Thus, the execution <math>S-i</math> can use the value assigned to <math>x</math> by <math>S_j</math>, <math>j<i</math> (i.e. there is an '''information flow''' between
<math>S_j</math> and <math>S_i</math> through <math>x</math>) only if there is no such <math>S_k</math>, <math>j<k<i</math>, that either <math>x</math> is a strong result of <math>S_k</math> or
<math>S_k</math> redefines the part of <math>W_k(x)</math> which is assigned to <math>x</math> by <math>S_j</math>.