1. Introduction
In both mathematics and programming, we are increasingly confronted with inductively given constructs. These constructs can be, for example, new types of terms and formulas in logic or programs and new data types in high-level programming languages that are inductively defined using basic tools. All these inductively generated sets can be viewed as the smallest fixed points of a suitable operator. Classical Gandy’s theorem [
1,
2] allows us to inductively define some abstract set through the special operator
[
1] where the smallest fixed point will be a
-set. The
-set is most often not a computable set and, moreover, not a p-computable set. Therefore, the question arises of how to modify Gandy’s theorem so that the smallest fixed point be a computable or a p-computable set. In this paper, we just talk about the construction of a
-operator with the smallest fixed point being a
p-computable set, which allows us to consider many inductive formulas definable constructions as some polynomially computable set.
2. P-Computability
Let
be a finite alphabet and
where
is the set of finite words over the alphabet
. We say that a function
is p-computable [
3,
4,
5] if there exists a one-tape/multi-tapes deterministic Turing machine
T over the alphabet
and numbers
such that for all
a from
A the value of the function
is computed on
T in at most
steps, where
. The set
A is called p-computable if its characteristic function
is
p-computable. The class
P of problems which can be solved in polynomial time will often be denoted by
(accepted notation for the polynomial hierarchy). Therefore, the notation
-function for a
p-computable function and
-set for a
p-computable set will also be used. A partial function
is called a partial
p-computable function, if there exists a set
such that
is a
p-computable function (the Turing machine which represents
f computes
and stops at the final state
) and
is undefined (notation
or simple
) if
, while the Turing machine on the element
stops at the final state
and number of steps does not exceed
steps. As we can see, the partial
p-computable function is a
p-computable function, but sometimes it is convenient to assume that the value of a
p-computable function is undefined. We will also denote partial
p-computable functions as
-functions.
3. Word Splitting
Now let
be some finite alphabet and
=
is a new alphabet obtained by adding new symbols (brackets and comma) to
. Word splitting is the following partial function
such that:
- (1)
- (2)
starts with a left bracket and the number of left brackets in the word is equal to the number of right brackets, while for any initial subword such that it is not implemented, where the word can be represented as some concatenation of the words and .
Proposition 1. The word splitting is unique.
Proof. Prove by contradiction. Let there be two different splittings and such that and . Then, by definition, either , or and start with a left bracket and the number of right and left brackets for each word is the same. In the first case, and are the same. In the second case, is the subword of or is the subword of . Then, by definition, no proper subword starting with a left bracket can have an equal number of right and left brackets. Equality of words was also obtained. Further, in a similar way, we show that the remaining and at the same time . □
Proposition 2. is -function.
Proof. Consider a Turing machine T with two semi-tapes (hereafter called tapes) over the alphabet where B is an empty symbol:
- (1)
The 1st tape: we will store the word w.
- (2)
The 2nd tape: we will store the difference between the number of left and right brackets of the word w.
Algorithm of the multi-tapes machine:
- (1)
If the first symbol on the first tape is not a left bracket, then T stops the work in the final state . Otherwise, T replaces it on B symbol and goes on to the next steps.
- (2)
If the second symbol in the word w is from , then T reads the word w until it meets a symbol, not from . If it is not a comma or a right bracket then T stops the work in state .
- (3)
If the second symbol is not from and is not a left bracket, then T stops the work in the state .
- (4)
When T reads the left bracket of the word w, then T adds 1 on the second tape and shifts the head of the second tape to the right and when T reads the right bracket of the word w, then T replaces symbol 1 with B of the second tape and shifts the head of the second tape to the left.
- (5)
If there are no more symbols 1 on the second tape when T reads the right bracket from the first tape, then the machine replaces the right bracket with B on the first tape. If there are no other symbols from after this right bracket, then the machine stops work in the final state , otherwise, in the final state .
- (6)
If T meets a comma on the first tape and there are no symbols 1 on the second tape, then T replaces this comma with # symbol.
Computational complexity :
- (1)
T reads the word w on the first tape periodically replacing the comma or brackets with symbol #. The number of such steps does not exceed .
- (2)
On the second tape T writes or erases symbols 1. The number of such additions and removals does not exceed .
- (3)
Steps from (1) and (2) taken simultaneously. It turns out that the computational complexity .
□
Inductively define the notion rank of element
for
:
4. Generating Formulas and Families. False Element
Let be a model of signature with the basic set , where is constant symbols (), is functional symbols (), is predicate symbols (), is unary predicate symbols, . is the set of all subsets of the set . is families (generating families) positive quantifier-free formulas (hereafter called generating formulas) of signature which can include unary predicates ,..., with inputs of the form . Moreover, we require that for any free variable in the formula there should be no occurrences of the form and for each , where . This property will be called predicate separability.
The idea is to generate new elements in the form of lists obtained from such that and then add this set of elements to the main set of the model where:
If we are to extend the main set of elements M of the model to this new set of elements , then we need to redefine the functions on these new elements and redefine the truth of the predicates. It is clear that the functions on new elements will not be defined, so we will expand the basic set of elements M of the model of signature with a special -element to . Next, we define the semantic meaning of terms and formulas in the model for all elements from and not only for .
Since everywhere below only positive quantifier-free formulas with a positive occurrence in the form of for some and appear, then for these formulas on the model we inductively define the values of functions and the truth of predicates as well as the truth of positive quantifier-free formulas , :
- (1)
if and only if where .
- (2)
the function value equal , if at least one ,
- (3)
the function value equal if at least the value of one of the terms equals .
- (4)
the formulas of the form including will be considered false.
- (5)
the formulas of the form will be considered true for and false otherwise.
- (6)
the formulas of the form will be considered false if at least one of the terms has value .
- (7)
if and only if where .
- (8)
, retain their standard definitions of truth.
Let us denote enrichment of the model by such that:
- (1)
is a new main set.
- (2)
All predicates remain unchanged if the values of the terms are from M and are otherwise.
- (3)
All predicates remain unchanged if and are otherwise.
- (4)
All functions remain unchanged for and have a value otherwise.
Denote the expression it is enrichment at which the truth set of the predicate is extended to .
5. Fixed Points of Monotone Locally Finite Operators
Let be a model of signature and , , .
Then we introduce the notation: .
Construct an operator:
which transfers
n-th sets
to
n-th sets
according to the following rule:
where
and
is built on the model
of signature
in the following way:
We fix a partial order : , if for all
Remark 1. Operator is monotone with respect to the order , i.e., Remark 2. Operator possesses the property of a fixed point, i.e.: Associate the operator
with the sequence:
:
Let us denote projection onto the j-th coordinate by .
We will say that operator
is locally finite if for any
and any
is done:
where
are finite sets.
Proposition 3. Operator is locally finite.
Proof. Let , where are finite sets.
⇐ Inclusion in equality (3) for operator in one way is fulfilled by construction of our operator .
⇒ Let w be from . We get that w is a finite list made up of a finite number of elements from . Mark all the elements involved in constructing w from as for all . Note that all sets are finite and . Therefore, narrowing our sets to we get .
□
Proposition 4. The smallest fixed point of the operator is reached in w steps.
Proof. Claim that the fixed point of the operator is reached in w steps following automatically from the fact that the operator is monotone, has the fixed point property and is locally finite. □
6. Formulas Families
Further, we will consider generating families of formulas of the form where is encoding the variable with a string of v symbols length i. Let be a string of symbols above the alphabet length . Then the formula is obtained from replacing all occurrences of the form on i-th symbol in word . The number of free variables in this formula may be less, nevertheless we leave their number in the notation for as before.
The formula is obtained from substituting free variables by the corresponding values for all . Due to the predicate separability of the formula the maximum number of such occurrences in may not be more than .
Define as a set of symbols such that any formula of the form , , , , where , for some .
Define a potentially generating formula as a formula potentially generating an element such that and the following holds:
for some signification
. If for any
there is only one potentially generating formula in the family, then we can define a partial function
that constructs from an element
its potentially generating formula
if such a formula exists and is undefined otherwise
. In the next chapter we will require for functions
to be
p-computable.
7. -Models and -Operators
Model
of the finite signature
will be called a
p-computable model (
-model) [
4,
5,
6,
7] if all functions are
p-computable functions, all predicates and the main set are
-sets. If we want to mark the degree of the polynomial
n and the constant
C, we will write C-n-
-model instead of writing
-model. Sometimes, there will be records of the form C-p-
. In the first case,
p is the degree of the polynomial and in the second,
is the designation for the first level of the polynomial hierarchy. Designation of C-p-
-function will be also applied for functions and C-p-
-set will be also applied for sets. Note that
will be a C-p-
-model if such is the model
.
Let us call -operator the operator from (1) if for some the following four properties hold:
- (1)
p-computable model: is a C-p--model.
- (2)
predicate separability, quantifier-free and positivity: each family is either a finite or countable family of formulas, all formulas are positive, quantifier-free, predicate-separable.
- (3)
uniqueness of the generating formula: for any two formulas , with the same number of free variables and for any signification , , it is not true that there exists such significations as and consistent with such that:
- (4)
p-computability of element: we also require that all functions should be C-(p-1)--functions and families - C-p--families (time for checking , for all and ), .
Note that the -operator thus defined retains all the original properties: it is monotone, has a fixed point property and is locally finite, and therefore the smallest fixed point of the operator is reached in w steps.
We say that the smallest fixed point will be -set if any is a -set, where . Let be the C-(p-1)--function for -operator and - potential generating formula for l, where and all . Then the following lemma is true for any signification :
Lemma 1. is built according to the formula and by signification ϵ for the time not exceeding .
Proof. Consider the Turing machine T over alphabet consisting of five semi-tapes (hereafter called tapes):
- (1)
the 1st tape: the formula is written out.
- (2)
the 2nd tape: the word of length k is written out.
- (3)
the 3rd tape: for variables.
- (4)
the 4th tape: remembers the last position of the first tape.
- (5)
the 5th tape: builds a new formula .
Let the formula be written out on the first tape and the second tape should contain the word . The machine T starts to work in the extreme left position and reads the formula from the first tape. As soon as T reaches the word of the form , T begins to read this word and writes out in parallel symbol 1 on the fourth tape for each symbol of and symbol 1 for each symbol v of on the third tape, moving in parallel, the machine head on the second tape containing the word with a single delay. When all the symbols () are read, the head on the second tape will observe symbol which must be substituted for the word . Since the head position of the first tape is recorded on the fourth tape, T starts to overwrite on the first tape the word on symbols # and reduce in parallel the number of symbols 1 on the fourth tape. One as soon as there are no one-symbols left on the fourth tape, then T write the symbol to the first tape. Then T returns the heads of second, third and fourth tapes to the extreme left position and continue to sequentially find and replace the remaining occurrences of the form on the first tape and replace them with symbols # and . After all the replacements T must return the head of the first tape to the extreme left position and starts copying the formula of the first tape to the fifth tape while skipping the symbols #.
Calculate the total operating time of such a machine T:
- (1)
The machine T works with the formula on the first tape which includes words such as . The length of this formula does not exceed . In total, the number of steps does not exceed three lengths of .
- (2)
On the second tape, the machine does not change the word , simply reads it in parallel with the symbols v from the first tape and periodically returns the head to the extreme left position. The total number of shifts to the right of the machine head of the second tape does not exceed the length of the word on the first tape. The same goes for the number of the machine head shifts to the left. Therefore, on this tape, there will be no more than steps.
- (3)
On the third tape, the last monitored variable is written out. The number of the machine head shifts to the right and to the left does not exceed on this tape.
- (4)
For the fourth tape it is also does not exceed .
- (5)
To copy the final word from the first tape to the fifth and taking into account the preliminary setting of the head of the first tape to the extreme left position, it will also take no more than
□
Let be potentially generative formula for an element l.
Lemma 2. is built by word l and the formula for the time not exceeding .
Proof. Consider a Turing machine T over alphabet that also consists of three semi-tapes (hereafter called tapes):
- (1)
the 1st tape: the formula is written out, where the length of the formula does not exceed .
- (2)
the second tape: the word written out, where the length of the word does not exceeding .
- (3)
the third tape: builds a new formula .
The machine starts to work with the formula of the first tape, if necessary simultaneously copying the result to the third tape. If the machine T on the first tape reads a symbol that is not v, then T copies it to the third tape. If T reads the symbol v on the first tape, then T starts the process of finding the corresponding for replacement. When the machine T reads the i-th symbol v successively from the first tape, T transfers the machine head of second tape to the i-th symbol # that comes before the corresponding . When T reads all symbols v successively from first tape, then the machine will write the corresponding from second tape to the third tape. By repeating this algorithm on the third tape the word will eventually be written.
Calculate the total operating time of such a machine T:
- (1)
the machine T reads a word from the first tape or just stands and waits for further reading. The number of movements to the right does not exceed
- (2)
on the second tape, the machine head moves both to the right and to the left, but again only reading. Therefore, the number of steps does not exceed .
- (3)
the third tape: the number of steps does not exceed
□
8. A Polynomial Analogue of Gandy’s Theorem
Let from equality (2) be the smallest fixed point of -operator , then the next theorem is true:
Theorem 1 (polynomial analogue of Gandy’s theorem).The smallest fixed point of -operator is a -set.
Proof. The main idea of the proof is to show that the time for checking the truth of the formula on does not exceed the time , where k and C are fixed constants and is the rank of the element l and , . Since the rank , we get that for any l the complexity does not exceed .
Without loss of generality, we show this for , assuming in the induction step that this estimate is true for all , where and . Using the induction by complexity we show that , where the constant C is the maximum for all constants that participate in the splitting function , in functions and in the algorithm for checking the truth of the formula .
Induction base :
The time required to construct a potentially generating formula using l does not exceed . Next, we build and . The time required for this does not exceed and (Lemmas 1 and 2). Verifying the truth of the last formula for does not exceed . Summing everything up, we get that the verification time does not exceed .
The induction step: let our assumption be true for . We will show this for :
Case 1:
, then the formula
is false. We get it in time:
Case 2:
where
string of symbols
such that
if formula
is true on
and 0 otherwise.
Let’s calculate the time spent on all transitions:
- (1)
constructing a potentially generating formula using l in time
- (2)
determining the truth of all predicates
which are included in the formula. By the induction hypothesis, we obtain:
- (3)
further, we fix the signification considering whether the predicate is true or false, if the formula does not include any of the predicates for the variable , then we determine the truth for by default.
- (4)
By the formula and by the signification we construct . The time required for this does not exceed .
- (5)
By the formula and l we construct . The time required for this does not exceed .
If we sum up all the time of calculations, then we get the following:
We have shown that for any element
l of rank
in time
we determine the fact whether it belongs to the predicate
. Since
is always less than
, we can write the following:
□
9. Corollaries and Applications
For the -model as an application of the polynomial analogue of Gandy’s theorem, we present several corollaries. Some of these corollaries have already been proven earlier by other authors using other methods, some are presented for the first time.
Let the model
have a one-place predicate
U that selects the elements of the main set
M and a distinguished one-place predicate
(a predicate that will select list elements), then we will show how easy it is to prove the following statement on hereditarily finite lists
which was already proven earlier in [
8] but using a different technique:
Corollary 1. If is a -model, then is a -set.
Proof. A countable generating family of formulas
is as follows:
This family of formulas is predicate-separable, all formulas are positive quantifier-free, and the predicate is included in formulas positively. We can easily see that the operator is a -operator. □
Let the signature have the form: . Consider the model with the basic set of elements N and signatures . The interpretation of the constant will be 1 and s-the standard successor function. Further, an entry of the form will mean a term of the form n-fold application of the function s to .
Corollary 2. The set of quantifier-free formulas of signature σ is a -set.
Proof. The process of constructing auxiliary -sets using generating families for the corresponding predicates in the -model is as follows:
- (1)
Constants: : ,
- (2)
Variables: : ,
- (3)
Function symbols: : ,
- (4)
Predicate symbols: : , .
- (5)
Terms that are not constants and variables:
- (6)
The set of standard terms:
Generating family for quantifier-free formulas :
- (1)
- (2)
- (3)
- (4)
- (5)
- (6)
- (7)
□
Define the signature .
Corollary 3. The set of -formulas [9] signature is a -set. Proof. Define a family of -formulas . Just as in Corollary 2, we write out generating formulas for terms and formulas, with the only difference that we also add formulas for the above predicates:
- (8)
- (9)
We also write out generating formulas for , , , :
- (10)
- (11)
- (12)
- (13)
□
Corollary 4. The set of conditional terms of signature and -formulas is a -sets [9]. Proof. This is where the approach gets more interesting. We need to simultaneously generate both conditional terms and formulas containing these conditional terms. Therefore, we construct two generating families: , . In addition to generating formulas for standard terms in , we add countably many generating formulas for conditional terms:
- (8)
: , .
The family is defined by the same generating formulas as the family , with the only difference that the predicates must be replaced with everywhere. □
10. Conclusions
This work is a starting point for building a methodology for developing fast and reliable software. In this work, we study sufficient conditions for the
-operator under which the smallest fixed point remains a
-set. This allows us to create new elements and data types. Moreover, there are polynomial algorithms for checking the fact whether a certain element belongs to a given data type or not. The question of programming methodology is also of interest: which constructs can be used and which not for creating programs, if we want our programs to be polynomially computable. With the help of the main theorem of our paper and the theorems from the works [
8,
9,
10,
11,
12,
13,
14] it is already possible to develop logical programming languages, with programs being of polynomial computational complexity.