Separation logic is successful for software verification of heap-manipulating programs. Numbers are necessary to be added to separation logic for verification of practical software where numbers are important. However, properties of the validity such as decidability and complexity for separation logic with numbers have not been fully studied yet. This paper presents the translation of Pi-0-1 formulas in Peano arithmetic to formulas in a small fragment of separation logic with numbers, which consists only of the intuitionistic points-to predicate, 0 and the successor function. Then this paper proves that a formula in Peano arithmetic is valid in the standard model if and only if its translation in this fragment is valid in the standard interpretation. As a corollary, this paper also gives a perspective proof for the undecidability of the validity in this fragment. Since Pi-0-1 formulas can describe consistency of logical systems and non-termination of computations, this result also shows that these properties discussed in Peano arithmetic can also be discussed in such a small fragment of separation logic with numbers.

Abstract A cyclic proof system is a proof system whose proof figure is a tree with cycles. The cut-elimination in a proof system is fundamental. It is conjectured that the cut-elimination in the cyclic proof system for first-order logic with inductive definitions does not hold. This paper shows that the conjecture is correct by giving a sequent not provable without the cut rule but provable in the cyclic proof system.

A cyclic proof system, called CLKID-omega, gives us another way of representing inductive definitions and efficient proof search. The 2005 paper by Brotherston showed that the provability of CLKID-omega includes the provability of LKID, first order classical logic with inductive definitions in Martin-L\"of's style, and conjectured the equivalence. The equivalence has been left an open question since 2011. This paper shows that CLKID-omega and LKID are indeed not equivalent. This paper considers a statement called 2-Hydra in these two systems with the first-order language formed by 0, the successor, the natural number predicate, and a binary predicate symbol used to express 2-Hydra. This paper shows that the 2-Hydra statement is provable in CLKID-omega, but the statement is not provable in LKID, by constructing some Henkin model where the statement is false.

We address the problem of un-supervised soft-clustering that we call micro-clustering. The aim of the problem is to enumerate all groups composed of records strongly related to each other, whereas standard clustering methods find boundaries at which records are few. The existing methods have several weak points; generation of intractable amounts of clusters, biased size distributions, lack of robustness, etc. We propose a new methodology data polishing. Data polishing clarifies the cluster structures in the data by perturbating the data according to feasible hypothesis. More precisely, for graph clustering problems, data polishing replaces dense subgraphs that would correspond to clusters by cliques, and deletes edges not included in any dense subgraph. The clusters are clarified as maximal cliques, thus are easy to find, and the number of maximal cliques is reduced to tractable numbers. We also propose an efficient algorithm so that the computation is done in few minutes even for large scale data. The computational experiments demonstrate the efficiency of our formulation and algorithm, i.e., the number of solutions is small, such as 1,000, the members of each group are deeply related, and the computation time is short.

A cyclic proof system, called CLKID-omega, gives us another way of representing inductive definitions and efficient proof search. The 2011 paper by Brotherston and Simpson showed that the provability of CLKID-omega includes the provability of the classical system of Martin-Lof's inductive definitions, called LKID, and conjectured the equivalence. By this year the equivalence has been left an open question. In general, the conjecture was proved to be false in FoSSaCS 2017 paper by Berardi and Tatsuta. However, if we restrict both systems to only the natural number inductive predicate and add Peano arithmetic to both systems, the conjecture was proved to be true in FoSSaCS 2017 paper by Simpson. This paper shows that if we add arithmetic to both systems, they become equivalent, namely, the conjecture holds. The result of this paper includes that of the paper by Simpson as a special case. In order to construct a proof of LKID for a given cyclic proof, this paper shows every bud in the cyclic proof is provable in LKID, by cutting the cyclic proof into subproofs such that in each subproof the conclusion is a companion and the assumptions are buds. The global trace condition gives some induction principle, by using an extension of Podelski-Rybalchenko termination theorem from well-foundedness to induction schema. In order to prove this extension, this paper also shows that infinite Ramsey theorem is formalizable in Peano arithmetic.

Static analysis of multi-staged programs is challenging because the basic assumption of conventional static analysis no longer holds: the program text itself is no longer a fixed static entity, but rather a dynamically constructed value. This article presents a semantic-preserving translation of multi-staged call-by-value programs into unstaged programs and a static analysis framework based on this translation. The translation is semantic-preserving in that every small-step reduction of a multi-staged program is simulated by the evaluation of its unstaged version. Thanks to this translation we can analyze multi-staged programs with existing static analysis techniques that have been developed for conventional unstaged programs: we first apply the unstaging translation, then we apply conventional static analysis to the unstaged version, and finally we cast the analysis results back in terms of the original staged program. Our translation handles staging constructs that have been evolved to be useful in practice (typified in Lisp's quasi-quotation): open code as values, unrestricted operations on references and intentional variable-capturing substitutions. This article omits references for which we refer the reader to our companion technical report.

The study of type isomorphisms for different λ-calculi started over twenty years ago, and a very wide body of knowledge has been established, both in terms of results and in terms of techniques. A notable missing piece of the puzzle was the characterization of type isomorphisms in the presence of intersection types. While, at first thought, this may seem to be a simple exercise, it turns out that not only finding the right characterization is not simple, but that the very notion of isomorphism in intersection types is an unexpectedly original element in the previously known landscape, breaking most of the known properties of isomorphisms of the typed λ-calculus. In particular, isomorphism is not a congruence and types that are equal in the standard models of intersection types may be nonisomorphic.

Reynolds' separation logical system for pointer program verification is investigated. This paper proves its completeness theorem as well as the expressiveness theorem that states the weakest precondition of every program and every assertion can be expressed by some assertion. This paper also introduces the predicate that represents the next new cell, and proves the completeness and the soundness of the extended system under deterministic semantics.

This paper answers the open problem of finding a type system that characterizes hereditary permutators. First this paper shows that there does not exist such a type system by showing that the set of hereditary permutators is not recursively enumerable. The set of positive primitive recursive functions is used to prove it. Secondly this paper gives a best-possible solution by providing a countably infinite set of types such that a term has every type in the set if and only if the term is a hereditary permutator. By the same technique for the first claim, this paper also shows that a set of normalizing terms in infinite lambda-calculus is not recursively enumerable if it contains some term having a computable infinite path,and shows the set of streams is not recursively enumerable.

This paper analyses the computational behaviour of lambda-term applications. The properties we are interested in are weak normalisation (i.e. there is a terminating reduction) and strong normalisation (i.e. all reductions are terminating). One can prove that the application of a lambda-term M to a fixed number n of copies of the same arbitrary strongly normalising lambda-term is strongly normalising if and only if the application of M to n different arbitrary strongly normalising lambda-terms is strongly normalising, i.e. one has that M (X ... X)/n is strongly normalising, for an arbitrary strongly normalising X, if and only if MX1...Xnis strongly normalising for arbitrary strongly normalising X1, ..., Xn. The analogous property holds when replacing strongly normalising by weakly normalising. As an application of the result on strong normalisation the lambda-terms whose interpretation is the top element (in the environment which associates the top element to all variables) of the Honsell-Lenisa model turn out to be exactly the lambda-terms which, applied to an arbitrary number of strongly normalising lambda-terms, always produces strongly normalising lambda-terms. This proof uses a finitary logical description of the model by means of intersection types. This answers an open question stated by Dezani, Honsell and Motohama

Abstract This paper points out an error of Parigot's proof of strong normalization of second order classical natural deduction by the CPS-translation, discusses erasing-continuation of the CPS-translation, and corrects that proof by using the notion of augmentations.

Our paper [1] contains a serious error. Proposition 4.6 of [1] is actually false and hence our strong normalization proof does not work for the Curry-style λµ-calculus. However, our method still can show that (1) the correction of Proposition 5.4 of [2], and (2) the correction of the proof of strong normalization of Church-style λµ-calculus by CPS-translation. Firstly, our method is still effective for the correction of Proposition 5.4 of [2]. The proposition claims that for any Curry-style λµ-term u, which is not necessarily typable, if u ∗ is strongly normalizable, then u is strongly normalizable too. But its proof does not work, since Proposition 5.1 (i) of [2] is false because of erasing-continuation. Our method proves the similar result for the Curry-style λµ-calculus by Propositions 4.3 and 4.12 of [1]. Proposition. For any Curry-style λµ-term u, if there exists an augmentation u + of u such that u + ∗ is strongly normalizable, then u is strongly normalizable. Secondly, as mentioned in the concluding remarks of [1], our method is effective for the strong normalization proof of the Church-style λµ-calculus, which is called the second-order typed λµcalculus in [2]. The strong normalization of the typed λµ-calculus is proved in [2], but its proof with CPS-translation does not work since Proposition 5.5 of [2] is false because of erasing-continuation.

This paper gives a q-realizability interpretation for Feferman's constructive theory T/sub 0/ of functions and classes by using a set completion program without doubling variables, and proves its soundness. This result solves an open problem proposed by Feferman in 1979. Moreover by using this interpretation we can prove a program extraction theorem for T/sub 0/, which enables us to use constructive sets of T/sub 0/ for program synthesis.

Abstract A minimal formula is a formula which is minimal in provable formulas with respect to the substitution relation. This paper shows the following: (1) A β-normal proof of a minimal formula of depth 2 is unique in NJ. (2) There exists a minimal formula of depth 3 whose βη-normal proof is not unique in NJ. (3) There exists a minimal formula of depth 3 whose βη-normal proof is not unique in NK.