In the paper new logics oriented on hierarchical data are developed. Algebras of partial predicates over such data with special compositions as operations form a semantic base for constructed logics. Characteristic property of such logics is the usage of composite names in their languages. Semantic properties of these logics are studied; corresponding sequent calculi are defined, their soundness and completeness are proved for logics of renominative level.
Mathematical logic is widely used in formal program development, analysis, and verification. Still, some discrepancies can be admitted between traditional logic and problems to be solved. For example: semantics of programs is presented by partial functions, whereas in traditional logic total functions and predicates are usually considered; programming languages have a developed system of data types, whereas traditional logic prefers to operate with simple unstructured types (sorts); semantic aspects of programs prevail over syntactical aspects, whereas in traditional logic we have the inverse situation. Discrepancies mentioned above complicate the usage of logic for program development and verification. In this paper we propose to take program models as an initial point and construct logics semantically based on such models.
To realize this idea we should first construct adequate models of programs. To tackle this problem we use composition-nominative approach to program formalization [1], which aims to construct a hierarchy of program models of various abstraction levels and generality. The main principles of the approach are the following.
Development principle (from abstract to concrete): program notions should be introduced as a process of their development that starts from abstract understanding capturing essential program properties and proceeds to more concrete considerations. Principle of integrity of intensional and extensional aspects: program notions should be presented in the integrity of their intensional and extensional aspects.
The intensional aspects in this integrity play a leading role. Principle of priority of semantics over syntax: program semantic and syntactical aspects should be first studied separately, then in their integrity in which semantic aspects prevail over syntactical ones. Compositionality principle: programs can be constructed from simpler programs (functions) with the help of special operations, called compositions, which form a kernel of program semantics structures. Nominativity principle: nominative (naming) relations are basic ones in constructing data and programs.
Here we have presented only principles relevant to the topic of the article; richer system of principles is developed in [2]. The above principles specify program models as composition-nominative systems (CNS) [1]. Such a system may be considered as a triple of simpler systems: composition, description, and denotation systems. A composition system defines semantic aspects of programs, a description system defines program descriptions (syntactical aspects), and a denotation system specifies meanings (referents) of descriptions. We consider semantics of programs as partial functions over class of data processed by programs; compositions are n-ary operations over functions. Thus, composition system can be specified as two algebras: data algebra and functional algebra.
Functional algebra is the main semantic notion in program formalization. Terms of this algebra define syntax of programs (descriptive system), and ordinary procedure of term interpretation gives a denotation system.
CNS can be used to construct formal models of various programming, specification, and database languages [1][2][3][4]. The program models presented by CNS are mathematically simple, but specify program semantics rather adequately; program models are highly parametric and can in a natural way represent programs of various abstraction levels; there is a possibility to introduce on a base of CNS the notion of special (abstract) computability and various axiomatic formalisms [5][6][7].
CNS are classified in accordance with levels of abstraction of their parameters: data, functions, and compositions. In this article levels of program models are induced by abstraction levels of data.
Data are considered at three levels: abstract, Boolean, and nominative. At the abstract level data are treated as "black boxes", thus no information can be extracted. At the Boolean level to abstract data new data considered as "white boxes" are added. Usually, these are logical values T (true) and F (false) from the set Bool. At the nominative level data are considered as "grey boxes", constructed of "black" and "white boxes" with the help of naming relations. The last level is the most interesting for programming. Data of this level are called nominative data. The class of nominative data over a set of names V and class of basic values W can be defined inductively or as the least fixed point of the recursive definition
, where ( , )
is the class of partial multi-valued (non-deterministic) functions.
To present nominative data we use the form Concretizations of nominative data can represent various data structures, such as records, arrays, lists, relations, etc. [1,4]. For example, a set {s 1 , s 2 , ..., s n } can be presented as nominative data [1s 1 , 1s 2 , ..., 1s n ], where 1 is treated as a standard name. Thus, we can formulate the following data representation principle: program data can be presented as concretizations of nominative data.
The levels of data abstraction formulated above may be treated as data intensionals. They respectively specify three levels of semantics-based program models: abstract, Boolean, nominative. The models of each level constitute extensionals of that level intensional. Program models of abstract level are very poor (actually, only sequencing compositions can be defined). Program models of Boolean level are richer and permit to define structured programming constructs (sequence, selection, and repetition). This level is still too abstract and does not explicitly specify data variables. At last, models of nominative level permit to formalise compositions of traditional programming. This level (its intensional) involves variables of different types. Consider, for example, a simple educational programming language WHILE [8], which is based on three main syntactical components: arithmetic expressions, Boolean expression, and statements. States of WHILE programs are considered as partial functions from the set V of variables to the set Z of values and here are denoted by V Z(=V Z). Thus, semantics of these components is the following: arithmetic expressions specify functions of the type V Z Z (we call them partial quasiary functions), Boolean expressions define functions of the type V Z Bool (partial quasiary predicates), statements specify functions of the type V Z V Z (partial biquasiary functions). Note that in our terminology V Z is a class of single-valued flat nominative data.
Example 1. Consider a Boolean expression x<y. Its semantics is formalized as a partial quasiary predicate less : V ZBool. This predicate is undefined on flat nominative data [x5, u4] (we write less ([x5, u4])), is defined on [x5, u4, y2] with value F (we write less ([x5, u4, y2])= F). Note that if a value of less is defined on some data, then the predicate is defined with the same value on any extension of this data. Thus, less ([x5, u4, y2, v4])=F, x, u, y, vV. This property is called equitonicity (a special case of monotonicity). A specific new composition is renomination 1 1 ,..., ,..., ([x2, u4, y4, v4]) = T. More elaborated programming languages work with hierarchical nominative data. In such languages composite names like x 1 .x 2 . … .x n are used to access data components. The details can be found in [2].
Having described program models of various abstraction levels, we can now start developing semantics-based logics which correspond to such models. Such logics will be called composition-nominative logics (CNL). Analysis of constructed program models shows that the main semantic notion of mathematical logic -the notion of predicate -can be defined at the Boolean level. At this level predicates are considered as partial functions from a class of abstract data A (with abstract intensional) to Bool.
In this case such compositions as disjunction , negation , etc, can be defined. These compositions are derived from Kleene's strong connectives [9]. Thus, the main semantic objects are algebras of partial predicates of the type <ABool; , >. The obtained logics may be called propositional logics of partial predicates. Such logics are rather abstract, therefore their further development is required at the nominative level. As was mentioned earlier, at this level we have two sublevels determined respectively by flat and hierarchical nominative data.
Three kinds of logics can be constructed from program models at the flat nominative data level: logics, which use only partial quasiary predicates (pure predicate logic); logics, which use additionally partial quasiary functions (predicate-function logics); logics, which use also bi-quasiary functions (program logics).
The first type of logics will generalize classical pure predicate logics, the second type -classical predicate logic (with functions and equality), and the third type can present various logics, which use program constructs.
Here we give a short characteristic only to composition-nominative pure predicate logics; predicate-function logics are described in [3]; as to composition-nominative program logics some initial variants are presented in [3,7].
From semantic point of view the main distinction of CNL from classical first-order logics is usage of partial quasiary predicates instead of total n-are predicates; this leads to algebras of quasiary predicates with compositions as operations. From syntactical point of view formulas of CNL are simply terms of algebras of quasiary predicates.
The main compositions that can be additionally specified at the nominative level are renomination 1 1
,..., ,...,
) and quantification x. These compositions use subject names as parameters. CNL of renominative level are based on algebras of the type <
x , x>. Properties of these algebras determine calculi for corresponding logics.
Note, that renomination (primarily in syntactical aspects) is widely used in classical logic, lambda-calculus, and specification languages like Z-notation [10], B [11], TLA [12], etc. Here we will give explicit semantic definition of this operation (cf. with [13]).
To preserve properties of classical first-order logic we should restrict the class V ABool of quasiary predicates. Namely, we introduce a class of equitone predicates and its different variations such as maxitotal equitone, local-equitone, equicompatible, and local-equicompatible classes [3]. Logics based on equitone and maxitotal equitone predicates are the "closest" generalization of classical first-order logic that preserve its main properties. These logics are called neoclassical logics [3].
The current article continues investigations of pure predicate logics over hierarchical nominative data initiated in [14]. Here we prove soundness (correctness) and completeness of the constructed logics. The distinctive feature of such logics is the usage of composite names of the form x 1 .x 2 . … .x n as parameters of renomination and quantification compositions.
The article is structured as follows: the first section is introduction, in the second section operations over hierarchical data are introduced and their properties are studied, the third section is devoted to compositions over predicates. In the fourth section semantic models and corresponding languages of logics are described, and the fifth section is devoted to definition of sequent calculi for some of the described logics.
Notions not defined here we interpret in sense of [3].
Class of hierarchical nominative data ND(V, A) over classes of basic names V and basic values A is defined inductively:
-nominative data of rank less or equal to k+1.
is the set of all finite single-valued mappings from V to ND k (V, A). Note, that we restrict nominative data to be single-valued mappings. This guaranties unambiguity of naming for data components. An empty nominative data has rank 0.
The set of hierarchical nominative data is defined as follows:
The value of name u in data d is equal to d(u), but we also write u:d in style of denaming operation. For a composite name u = y 1 .y 2 . … .y n notation u:d means y n :(…(y 2 :(y 1 :d))…). We drop a component xu:, if u: is undefined.
Hierarchical data can be represented also as oriented trees with edges labeled by basic names and leafs labeled by basic values.
Any hierarchical data d can be represented as a flat nominative data with composite names -elements of the set V + . These composite names are non-empty words in the alphabet V formed by concatenation "." of basic names along the path from the root to leafs in the tree representing d.
Such representations are called flat normal forms (FNF) of hierarchical data. Due to the unambiguity of naming all (composite) names of FNF must be different; moreover, they should be incomparable. Now it is possible to write
Let us formulate some definitions and properties of hierarchical data used in further proofs. From now on, names are considered as composite names from V + unless explicitly stated that they belong to V.
A prefix of a word uV + is any word x such that u = x.y for some yV*. , ,..., ,...,
In the general case we have that : HD(V, A) HD(V, A) we define as follows:
,..., ( ) || : ... :
Here all names v 1 ,..., v n should be pairwise incomparable. We see that the result of renomination can be presented uniquely in the standard form. Example 6. . , . , . . . , . , .
( )
To present convolution of renominations we use the standard form. Example 7.
. .
(
)
Thus, situation for hierarchical data is more difficult than for flat data for which convolution of renominations can be presented as one new renomination [3].
Example 8. . . , .
, .
x
From semantic point of view the notion of predicate is one of the basic concepts of logic.
By a predicate P on D we understand a single-valued partial function of the type D Bool. The truth and falsity domains of P are respectively
Compositions determine universal methods of predicate construction; they form the kernel of logic of corresponding type.
At the propositional level data are treated as abstract, therefore predicates are interpreted as functions from A to Bool, where A is an abstract class. Basic propositional compositions are disjunction and negation ( P, QA Bool, d A ):
, if ( ) or ( ) , ( )( ) , if ( ) and ( ) , undefined in other cases.
At the nominative level data are constructed from a set of subject names and a class of subject values. In this work logics of partial predicates over hierarchical nominative data at renominative and quantifier level are investigated.
A function of the form Р : HD(V, A) Bool is called a hierary predicate on HD(V, A). We denote the class of hierary predicates on HD(V, A) by PrH V_А .
The name xV is strictly unessential for a hierary predicate P on HD(V, A), if for arbitrary d, HD(V, A) we have P(d || -x + x) = P(d || -х ). The notion of unessential name is an analogue of fresh name in classical and nominal logics [15].
At the renominative level to propositional compositions we add renomination composition
... : )
Using vector notation , we can formulate the following properties of renomination: R)
. The properties of R, R&, R can be written down analogously. RR) ( ( )( ) ( ( ( )))
for each dHD(V, A).
, , ( ) ( )
RT) , , ( ) ( )
In the case of equitone predicates for composite names we have: RTE) , , ( ) ( )
, where is weak equality.
At the quantifier level basic compositions are , , v x R , x. Contrary to traditional case quantified names can be composite; quantification is possible both over all hierarchical or only over basic data. In this work we consider quantification over hierarchical data. Composition of existential quantification is defined in the following way:
, if there exists ( , ) : ( || ) , ( ) , if ( || ) for all ( , ), undefined in all other cases.
Composition of universal quantification is defined by formula хР=хР. Theorem 1. The class of equitone predicates over hierarchical data is closed under compositions , , v x R , x, х. Main properties of compositions x and x are the following.
Properties 4-6 can be rephrased for universal quantification.
Let us note that some properties valid in classical logic fail for the class of equitone predicates over hierarchical data.
Example 9. Let predicate х be defined by the following formula: Alphabet of a language of quantifier level includes symbols of basic compositions, a set Ps of predicate symbols, and a set of basic subject names (variables) V.
The set Fr of formulas for a quantifier level is defined inductively: 1) every predicate symbol from Ps is an (atomic) formula;
2) if and are formulas, then and are formulas;
3
For CNLH of renominative level we drop item 4 in this definition. Let nm() be the set of all names, which appear in the symbols of renomination and quantification in .
To distinguish symbols of compositions from their interpretations we use for the latter bold font (only in the following definitions). Let I : Ps PrH V_А be a total single-valued interpretation mapping, then a pair (AHD(V, A), I) is called a model of CNLH language. To simplify notation we will denote models as (A, I) Interpretation J : FrPrH V_А we define as follows:
1) J(р) = I(p) for each рPs; 2) J() = J()J(), J() = (J()); 3) J ( )
For renominative level we drop item 4. Predicate J(), which is the value of a formula interpreted on A = (A, I), we denote by A . A formula is partially true on A = (A, I) (denoted by A |= ), if A is partially true (irrefutable) predicate. is everywhere (partially) true, or irrefutable (denoted by |= ), if is partially true on every model of a language.
A formula is a logical consequence of a formula
Formulas and are logically equivalent ( ), if |= and |= . Formulas and are logically strictly equivalent ( TF ), if T( A ) = T( A ) and F( A ) = F( A ) for each AS A. The relation of logical consequence can be extended to arbitrary sets , Fr. is a logical consequence of in the model A ( A |= ) if for all dHD(V, A) the condition A (d) = T for all implies that it is impossible that A (d) = F for all . is a logical consequence of ( |= ), if А |= for all model A = (А, I). Relation |= is reflective but not transitive.
For CNLH the following statements hold. Theorem 2 (semantic equivalence). Suppose that ' is obtained from by substitution of some occurrences of 1 ,..., n with 1 ,...,
Theorem 3 (semantic equivalence, strong form). Suppose that ' is obtained from by substitution of some occurrences of 1 ,..., n with 1 ,..., n respectively. If
Theorem 4 (substitution of equivalents). Suppose that
A name xV is strictly unessential for (xsun()), if x is strictly unessential for a predicate A for every A = (A, I).
Proposition 4. Let уsun(). Then x TF x y yR .
For each рPs the set of strictly unessential subject names is fixed by a total function : Ps2 V . For CNLH we postulate infinity of the set V T = ( )
The following properties of formulas are representations of corresponding semantic properties of predicate algebras.
RsN) , , ( )
RT) , , ( )
Generalizing R and R, we get RR and RR. RR) (... ( )...)
RR) ( (... ( )...))
Similarly, we can write down the properties R&, R, R, RR&, RR, RR. RR_C)
)
. ( )
zR R if zV T and znm(R v x (y)). Similarly, we can formulate R and R. Properties R, R, R, R can be generalized to RR, RR, RR, RR; R and R to RR and RR.
For equitone predicates RT can be changed to RTE: RTE) , , ( )
For logics of equitone predicates we introduce the notion of primitive formula. A formula ( (... ( )...))
where уV is strictly unessential for .
, where уV is strictly unessential for .
For R |-and R -| z is totally strictly unessential and znm(R v x (y)). Properties R |-, R -| , R |-, R -| are analogous. Properties of type R, R, R, R can be generalized to properties of type RR, RR, RR, RR.
For logics of equitone hierary predicates we will build a calculus of sequent type. We will consider here only logics of renominative level. Sequents are interpreted as sets of labeled formulas marked by one of two symbols -
Derivation in the sequent calculus has the form of tree, the vertices of which are sequents. Such trees [3] are called sequent trees. A sequent tree is closed, if every its leaf is a closed sequent. A sequent is derivable, if there is a closed sequent tree with root . Sequent calculus is constructed in such a way that sequent |- -| has a derivation if and only if |= .
Semantic properties of relation |= have their syntactic analogues -sequent forms (rules). For renominative logics of equitone hierary predicates these forms are the following.
In the paper new logics oriented on hierarchical data are developed. Algebras of partial predicates over such data with special compositions as operations form a semantic base for constructed logics. These logics may also be treated as generalization of classical logic. First of all, this generalization concerns types of predicates: while classical logic is semantically based on total n-ary predicates, we have constructed logics based on partial quasiary and hierary predicates, defined on special types of hierarchical nominative data. Importance of such data is explained by their representational power, which permits to model data structures of specification and programming languages. Characteristic feature of such languages is usage of composite names to access data components. The constructed logics also use composite names. Semantic properties of such logics have been studied; corresponding sequent calculi have been defined, their soundness and completeness have been proved for logics of renominative level. Authors plan to present more developed logics at hierarchical nominative level in forthcoming papers.
Procedure of construction of a tree for is split into stages. Every application of sequent form is performed only for the finite set of accessible formulas. At the beginning of every stage we perform the step of access: to the list of accessible formulas one formula from each of lists of |--formulas and -| -formulas is added. We start the construction with a pair of first formulas from the lists.
Suppose that k stages of procedure have already been performed. On the stage k+1 we check whether all terminal nodes are closed. If yes, the procedure is completed positively, and we have got a closed sequent tree. If no, for every unclosed leaf we undertake a next step of access, whereupon we finish building of finite subtree with a vertex as follows.
We activate all accessible non-primitive formula . Then to every active formula we apply the proper sequent form. We remove all repetitions of formulas in a sequent.
During the construction of sequent tree the following cases are possible: 1. Procedure is completed positively; we have the finite closed tree. 2. Procedure is completed negatively, or is not completed; we have a finite or infinite unclosed tree. Such tree has at least one path all vertices of which are unclosed sequents. Such path is unclosed. Every formula of will be in and will become accessible. Theorem 6. Let be an unclosed path in sequent tree. Then there exists AS A = (A, I) and HD(V, A):
The set Н of labeled formulas of sequents of the path is a model set.
Let W be a combination of naming schemes of the set of renominants of primitive formulas of sequents of the path . Such W includes longest incomparable names, which are involved in renominations of formulas of sequents of the path .
We duplicate elements of
We specify the values of basic predicates on and on data of the form (... ( )...) In all other cases for dHD(V, A) the value of р A (d) can be set arbitrarily, taking into account equitonicity and strict inessentiality of names.
Theorem holds for atomic and primitive formulas due to above definitions of basic