Value of a schema under interpretation

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

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

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

if [math]\displaystyle{ \Phi }[/math] is constant, then [math]\displaystyle{ W(\Phi)=I(\Phi) }[/math];

if [math]\displaystyle{ \Phi }[/math] is an operand, then [math]\displaystyle{ W(\Phi)=W(R_\alpha(\Phi)) }[/math];

if [math]\displaystyle{ \Phi= f(\Phi_1, \ldots, \Phi_n }[/math], then [math]\displaystyle{ W(\Phi)=I(f)(W(\Phi_1),\ldots, W(\Phi_n)) }[/math].

The run of [math]\displaystyle{ \alpha }[/math] under [math]\displaystyle{ I }[/math] starts with the START instruction whose execution defines the memory state [math]\displaystyle{ W_1 }[/math], such that [math]\displaystyle{ W_1(x)=I(x) }[/math] for any [math]\displaystyle{ 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]\displaystyle{ G_\alpha }[/math], terminates abnormally with such [math]\displaystyle{ S_i }[/math] that [math]\displaystyle{ W_i(P)= }[/math] false for the predicate term [math]\displaystyle{ P }[/math] of [math]\displaystyle{ S_i }[/math] and the current memory state [math]\displaystyle{ W_i }[/math], and terminates normally with a STOP instruction. Only in the former case the value of [math]\displaystyle{ \alpha }[/math] under [math]\displaystyle{ I }[/math], denoted [math]\displaystyle{ val(\alpha, I) }[/math], is defined; it is the tuple of current values of the arguments of the STOP instruction.

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