Research On The Toggling-branching Recurrence Of Computability Logic

Computability Logic(CoL) is a formal theory of developing the truth in classical logic to the formal theory of computability. It is firstly introduced by Japaridze. In it, the computational problem was seen as a game between the machine and the environment; the computability means that there exists an interactive Turing Machine always be a win-ner in the game; the logical operators represent the operations on games; the "truth" is seen as existence of an algorithmic solution.Static property is a very important property for a static game. In CoL, when ana-lyzing strategies, the questions on the relative speeds of the players is never relevant. We call a game A is static iff, the player (?) of A,△and Γ are any runs of A,△is a (?)-delay of Γ, if Γ is a (?) won run of A, then△also is a (?) won run of A. Every operation in CoL should preserve the static property.The semantics of the CoL operators is the same as the operators in classical log-ic. Recently, many new operators was introduced in CoL such that toggling-branching (co)recurrence which is the most difficult and complex operation. The definition of this operation has been described by Japapridze, but the proof of the static property is not pro-vided yet. This problem has been an open problem in CoL. Therefore, the study of this thesis includes three problems:the static property of the toggling-branching recurrence; the static property of the new toggling-branching recurrence; the equivalence of the two versions.In this thesis, we introduce the formal definition of the toggling-branching recur-rence. We use the (Lr, Wn) pair to define this operation and give the static property proof based on the definition. Before the proof, we describe the actual node and outer actual node. After that, we provide the delay of a run and prove a lemma. For a static game A, if△is a (?)-illegal run of (?) A and△is a p-delay of Γ, then Γ also is a (?)-illegal run of d A. So we successfully prove the static property of the (?) and (?) by using the result of this lemma.The complexity of the definition for the (?) and(?) impedes the future progress in finding syntactic descriptions of the logic induced by (?) and(?). So we should introduce a new and significantly simplified version of the (?) and(?). In this thesis, we provide a new simple version for the (?) and(?). In order to avoid the confusion, we use the symbols (?)T,(?)T for the tight version of (?),(?), and the symbols of (?) L,(?)L for the loose version. Loose version substitute the actual node with the bistrings. We also prove the static property of the new version.In order to do the further research based on the toggling-branching recurrence, we shall prove the equivalence between the two versions. We introduce two interactive com-putation models which are HPM(Hard-Play Machine) and EPM(Easy-Play Machine). Fi-nally, We use the EPM to describe the moves, runs and the steps during the whole games. We design two routines to prove the equivalence. The first routine is EPM ε1which can always win in the game of (?)T-A V (?) L A. The second routine is EPM ε2can also always win in the game of (?)L-A(?)(?)TA.The main contributions of this thesis are as follows:1. Formal definition and static property proof of the toggling-branching recurrence1). We provide the definition by using the (Lr,Wn) pair. We classify the two different kinds of operations in the toggling-branching recurrence. One is the branching operation which only can be done by the outer actual node in the game; The other is the switch operation which can be done by any actual node. It is easy for the user to understand the description in the definition. We also provide the delay of a run in a game. By using the result of a lemma, we can proof the theorem that a static game A, if Γ is a p won run of (?) A, then the run△is a p-delay of Γ, is also a p won run of (?) A2. New version of the toggling-branching recurrence2). The old definition based on the tree model is easy to describe the moves in the toggling-branching recurrence. However, it is too complex to develop a deductive system based on the old definition. So we should introduce a new and significantly simplified version. The new version is defined in this thesis by using the bitstring to describe the moves. The definition is simpler and easier. After the new definition, we also give the static property of this version. During the proof, we find that the cases is much easier than the old version to be dealt with. It is a good news for the research to finding the deductive systems based on the toggling-branching recurrence.3. The equivalence of the two versions3). The features of the games make us to introduce a different computational model to describe the interactive problems. In CoL, we use the HPM and EPM which modified the Turing Machine as an interactive computation model. In this thesis, we use the EPM to describe the interactive problems between machine and environment. HPM and EPM are equivalent.4). The equivalence of the toggling-branching recurrence means that we shall find the EPMs to win in the (?)T-A(?)(?)LA and (?)L-A(?)(?)TA. We design a ε1to be always the winner in the game of (?)T-A(?)(?)LA. By analyzing the routine, we find such ε1exists. A more difficult S2also can be proved to exist in our thesis. So we finish the proof.To study the work stated in this thesis, we propose the following future research directions:1. We plan to find and design the deductive system based on the d and (?). It contains the rules、soundness and completeness of the new system. We try to do a research from CLl to CL15to find the new deductive system.2.We plan to find the applied system containing the toggling-branching (co)recurrence. The plan also includes the design and implementation of the application system in computer science. We have implemented the interactive computation based on CL1by the visual operation. All of these will provide the fundamentals for the new research.3. The progress of CoL mainly focus on the theoretical field. We plan to find and exploit the new application in computer science such as interactive computation network protocol、knowledge base system or resource-based planning system.