Large-block schema

Large-block schema --- крупноблочная схема.

Large-block schema is an abstract model of imperative programs that is based on the notion of a program as a finite set of structured statements processing a finite set of structured variables. The class of large-block schemata includes (as proper subslasses) other models of imperative programs such as Martynyuk schemata and standard program schemata. It is complete with respect to simulation and allows the program optimizations affecting both program memory and control structure to be investigated.

Let [math]\displaystyle{ \Sigma }[/math] be an alphabet which consists of mutually disjoint sets of variables (denoted by [math]\displaystyle{ X }[/math]), constants, operator symbols, predicate symbols, access symbols and [math]\displaystyle{ k }[/math]-case symbols for any integer [math]\displaystyle{ k \gt 1 }[/math].

A large-block program schema [math]\displaystyle{ \alpha }[/math] is a triple [math]\displaystyle{ (G_\alpha, R_\alpha, \Omega_\alpha) }[/math], where [math]\displaystyle{ G_\alpha }[/math] is a flow-diagram, [math]\displaystyle{ R_\alpha }[/math] is a coloring and [math]\displaystyle{ \Omega_\alpha }[/math] is a nonempty set of interpretations.

A flow-diagram (or control-flow graph) [math]\displaystyle{ G_\alpha }[/math] is an ordered directed graph whose nodes are instructions (or statements). It has exactly one START instruction and a nonempty set of STOP instructions. An instruction with [math]\displaystyle{ k }[/math] outgoing arcs is called a [math]\displaystyle{ k }[/math]recognizer (or recognizer) if [math]\displaystyle{ k \gt 1 }[/math] and a transformer if [math]\displaystyle{ k=1 }[/math].

Every instruction [math]\displaystyle{ S }[/math] has a set of operands (divided into four disjoint subsets: strong inputs, nonstrong inputs, strong outputs, nonstrong outputs); the set for the START instruction is empty, and the set for each STOP consists of only nonstrong inputs. There are two relations on the set of operands: an equivalence relation which divides the set into subsets of (informationally) connected operands and a symmetric relation which consists of pairs of so called (informationally) incompatible operands. It is assumed that there is no such pairs of operands which are both connected and incompatible, and the outputs of every instruction are mutually incompatible.

Let [math]\displaystyle{ S }[/math] be a statement of [math]\displaystyle{ G_\alpha }[/math] distinct from START and STOP. Every output [math]\displaystyle{ d }[/math] of [math]\displaystyle{ S }[/math] has a data term [math]\displaystyle{ \Phi }[/math] of [math]\displaystyle{ S }[/math]; [math]\displaystyle{ \Phi }[/math] is built up using the inputs of [math]\displaystyle{ S }[/math] and the constants, and applying the operation symbols to them. If [math]\displaystyle{ d }[/math] is a nonstrong output of [math]\displaystyle{ S }[/math] and has [math]\displaystyle{ \Phi }[/math], [math]\displaystyle{ d }[/math] has also an access term of the form [math]\displaystyle{ g(\Phi_1,\Phi_2,\ldots,\Phi_n, \Phi, d) }[/math], where [math]\displaystyle{ g }[/math] is an ([math]\displaystyle{ n+2 }[/math])-ary access symbol and [math]\displaystyle{ \Phi_1,\Phi_2,\ldots,\Phi_n }[/math] are data terms of [math]\displaystyle{ S }[/math]. [math]\displaystyle{ S }[/math] can have a predicate term being a predicate symbol applied to data terms of [math]\displaystyle{ S }[/math], all inputs of which are strong ones. If [math]\displaystyle{ S }[/math] is a [math]\displaystyle{ k }[/math]-recognizer, [math]\displaystyle{ S }[/math] has a [math]\displaystyle{ k }[/math]case term being a [math]\displaystyle{ k }[/math]-case symbol applied to data terms of [math]\displaystyle{ S }[/math].

The colouring [math]\displaystyle{ R_\alpha }[/math] is such a mapping of the set of all operands on some subset [math]\displaystyle{ X_\alpha }[/math] (called the memory of the schema [math]\displaystyle{ \alpha }[/math]) of [math]\displaystyle{ X }[/math] that [math]\displaystyle{ R_\alpha(a)=R_\alpha(b) }[/math] for any two connected operands and [math]\displaystyle{ R_\alpha(a)\neq R_\alpha(b) }[/math] for any two incompatible operands. If [math]\displaystyle{ d }[/math] is a strong or nonstrong input (output, respectively) of a statement [math]\displaystyle{ S }[/math], then [math]\displaystyle{ x=R_\alpha(d) }[/math] is called a strong or nonstrong argument (result, respectively) of [math]\displaystyle{ S }[/math].

An interpretaion [math]\displaystyle{ I\in \Omega_\alpha }[/math] consists of

(1) a nonempty set [math]\displaystyle{ D_\alpha }[/math] called the domain of [math]\displaystyle{ I }[/math];

(2) an assignment of an element [math]\displaystyle{ I(c)\in D_I }[/math] to each variable and constant [math]\displaystyle{ c }[/math];

(3) an assignment of a function [math]\displaystyle{ I(f): D_I^n \rightarrow D_I }[/math] to every [math]\displaystyle{ n }[/math]-ary operator symbol [math]\displaystyle{ f }[/math];

(4) an assignment of a predicate [math]\displaystyle{ I(h): D_I^n \rightarrow \{ }[/math] true, false[math]\displaystyle{ \} }[/math] to every [math]\displaystyle{ n }[/math]-ary predicate symbol [math]\displaystyle{ h }[/math];

(5) an assignment of a (access) function [math]\displaystyle{ I(g): D_I^n \rightarrow D_I }[/math] to every [math]\displaystyle{ n }[/math]-ary access symbols [math]\displaystyle{ g }[/math], such that for any access functions [math]\displaystyle{ F_1, F_2, \ldots, F_m }[/math] and for any elements [math]\displaystyle{ a_1^1, }[/math] [math]\displaystyle{ \ldots, }[/math] [math]\displaystyle{ a_{k_1-1}^1, a_1^2, }[/math] [math]\displaystyle{ \ldots, }[/math] [math]\displaystyle{ a_{k_1-1}^2, }[/math] [math]\displaystyle{ \ldots, }[/math] [math]\displaystyle{ a_1^m,\ldots, a_{k_1-1}^m, a }[/math] from [math]\displaystyle{ D_I }[/math] if [math]\displaystyle{ F_1=F_m }[/math], [math]\displaystyle{ a_1^1=a_1^m, }[/math] [math]\displaystyle{ \ldots }[/math] [math]\displaystyle{ a_{k-1}^1=a_{k_m-1}^m, }[/math] then [math]\displaystyle{ F_1( }[/math] [math]\displaystyle{ a_1^1, }[/math] [math]\displaystyle{ \ldots, }[/math] [math]\displaystyle{ a_{k_1-1}^1, }[/math] [math]\displaystyle{ F_2( }[/math] [math]\displaystyle{ a_1^2, }[/math] [math]\displaystyle{ \ldots, }[/math] [math]\displaystyle{ a_{k_1-1}^2, }[/math] [math]\displaystyle{ \ldots, }[/math] [math]\displaystyle{ F_{m-1}( }[/math] [math]\displaystyle{ a^{m-1}_1, }[/math] [math]\displaystyle{ \ldots, }[/math] [math]\displaystyle{ a_{k_1-1}^{m-1}, }[/math] [math]\displaystyle{ F_m( }[/math] [math]\displaystyle{ a_1^m,\ldots, a_{k_1-1}^m, a))\ldots))= }[/math] [math]\displaystyle{ F_1( }[/math] [math]\displaystyle{ a_1^1, }[/math] [math]\displaystyle{ \ldots, }[/math] [math]\displaystyle{ a_{k_1-1}^1, }[/math] [math]\displaystyle{ F_2( }[/math] [math]\displaystyle{ a_1^2, }[/math] [math]\displaystyle{ \ldots, }[/math] [math]\displaystyle{ a_{k_1-1}^2, }[/math] [math]\displaystyle{ \ldots, }[/math] [math]\displaystyle{ F_{m-1}( }[/math] [math]\displaystyle{ a^{m-1}_1, }[/math] [math]\displaystyle{ \ldots, }[/math] [math]\displaystyle{ a_{k_1-1}^{m-1},a) }[/math] [math]\displaystyle{ \ldots)) }[/math];

(6) an assignment of a function [math]\displaystyle{ I(T): D_I^n \rightarrow \{1,2,\ldots, k\} }[/math] to every [math]\displaystyle{ n }[/math]-ary [math]\displaystyle{ k }[/math]-case symbol [math]\displaystyle{ T }[/math].

Inclusion and equivalence of schemata are defined as follows:

(1) [math]\displaystyle{ \alpha }[/math] includes (or extends) [math]\displaystyle{ \beta }[/math] iff [math]\displaystyle{ \Omega_\alpha \subseteq\Omega_\beta }[/math] and for any [math]\displaystyle{ I\in \Omega_\alpha }[/math], [math]\displaystyle{ val(\alpha, I)=val(\beta, I) }[/math] whenever [math]\displaystyle{ val(\alpha, I) }[/math] (see Value of schema under interpretation) is defined;

(2) [math]\displaystyle{ \alpha }[/math] and [math]\displaystyle{ \beta }[/math] are (strongly) equivalent iff either of them includes the other.