As an advanced network calculation mode, cloud computing is becoming more and more popular. However, with the proliferation of large data centers hosting cloud applications, the growth of energy consumption has been explosive. Surveys show that a remarkable part of the large energy consumed in data center results from over-provisioning of the network resource to meet requests during peak demand times. In this paper, we propose a solution to this problem by constructing a dynamic energy-efficient resource management scheme. As a (...) way of saving energy as well as maintaining cloud user’s quality of experience, the scheme presents a multitier cloud architecture by configuring physical machines into two pools: a hot pool and a warm pool. Each PM is configured with a resource search engine that finds an available virtual machine for the request, and a synchronous sleep mechanism is introduced to the warm pool. To analyze the end-to-end performance of the cloud system’s service with the proposed scheme, we establish a hybrid queueing system composed of three stochastic submodels by using a matrix-geometric solution. Accordingly, the average latency of requests and the energy-saving rate of the system are derived. Through numerical results, we show the influence of the synchronous sleep mechanism on the system performance. Moreover, from the perspective of economics, we build a system cost function to study the trade-off between different performance measures. An improved Salp Swarm Algorithm is presented to minimize the system cost and optimize the sleep parameter. (shrink)

Girard introduced phase semantics as a complete set-theoretic semantics of linear logic, and Okada modified phase-semantic completeness proofs to obtain normal-form theorems. On the basis of these works, Okada and Takemura reformulated Girard’s phase semantics so that it became phase semantics for proof-terms, i.e., lambda-terms. They formulated phase semantics for proof-terms of Laird’s dual affine/intuitionistic lambda-calculus and proved the normal-form theorem for Laird’s calculus via a completeness theorem. Their semantics was obtained by an application of computability predicates. In this paper, (...) we first formulate phase semantics for proof-terms of second-order intuitionistic propositional logic by modifying Tait-Girard’s saturated sets method. Next, we prove the completeness theorem with respect to this semantics, which implies a strong normalization theorem. (shrink)

In this paper, I will argue from a historical perspective that Gentzen’s 1935 consistency proof of 1st order Peano Arithmetic PA principally aimed to give a finitist interpretation of implication and this aspect of the 1935 proof emerged as the attempt to cope with the non-finiteness in BHK-interpretation of implication. My argument consists of two parts. First, I will explain that the fundamental idea of the 1935 proof is to show the soundness of PA on some finitist interpretation and Gentzen (...) had attempted to use BHK-interpretation as such an interpretation. It is claimed that he eventually thought that there is a ‘circularity’ which is due to the non-finiteness of BHK-interpretation of implication, so it cannot be used as a finitist interpretation. Secondly, I will argue that the principal aim of the 1935 proof is to give his own finitist interpretation of implication which avoids such a ‘circularity’. Finally, this paper’s conclusion and an open question are presented. (shrink)

Gentzen's three consistency proofs for elementary number theory have a common aim that originates from Hilbert's Program, namely, the aim to justify the application of classical reasoning to quantified propositions in elementary number theory. In addition to this common aim, Gentzen gave a “finitist” interpretation to every number-theoretic proposition with his 1935 and 1936 consistency proofs. In the present paper, we investigate the relationship of this interpretation with intuitionism in terms of the debate between the Hilbert School and the Brouwer (...) School over the significance of consistency proofs. First, we argue that the interpretation had the role of responding to a Brouwer-style objection against the significance of consistency proofs. Second, we propose a way of understanding Gentzen's response to this objection from an intuitionist perspective. (shrink)