To represent interactive objects, we propose a choice-disjunctive declaration statement of the form $S add R$ where S, R are the (procedure or field) declaration statements within a class. This statement has the following semantics: request the user to choose one between S and R when an object of this class is created. This statement is useful for representing interactive objects that require interaction with the user.

This paper proposes a new approach to defining and expressing algorithms: the notion of task logical algorithms. This notion allows the user to define an algorithm for a task T as a set of agents who can collectively perform T. This notion considerably simplifies the algorithm development process and can be seen as an integration of the sequential pseudocode and logical algorithms. This observation requires some changes to algorithm development process. We propose a two-step approach: the first step is to define an algorithm for a task T via a set of agents that can collectively perform T. The second step is to translate these agents into (higher-order) computability logic.

Higher-order rewrite systems (HRSs) and simply-typed term rewriting systems (STRSs) are computational models of functional programs. We recently proposed an extremely powerful method, the static dependency pair method, which is based on the notion of strong computability, in order to prove termination in STRSs. In this paper, we extend the method to HRSs. Since HRSs include λ-abstraction but STRSs do not, we restructure the static dependency pair method to allow λ-abstraction, and show that the static dependency pair method also works well on HRSs without new restrictions.

Simply-typed term rewriting systems (STRSs) are an extension of term rewriting systems. STRSs can be naturally handle higher order functions, which are widely used in existing functional programming languages. In this paper we design recursive and lexicographic path orders, which can efficiently prove the termination of STRSs. Moreover we discuss an application to the dependency pair and the argument filtering methods, which are very effective and efficient support methods for proving termination.

In the theory of average-case NP-completeness, Levin introduced the polynomial domination and Gurevich did the average polynomial domination. Ben-David et al. proved that if P-samp (the class of polynomial-time samplable distributions) is polynomially dominated by P-comp (the class of polynomial-time computable distributions) then there exists no strong one-way function. This result will be strengthened by relaxing the assumption from the polynomial domination to the average polynomial domination. Our results also include incompleteness for average polynomial-time one-one reducibility from (NP,P-samp) to (NP,P-comp). To derive these and other related results, a prefix-search algorithm presented by Ben-David et al. will be modified to survive the average polynomial domination.

We study the pm-degrees and pT-degrees of immune and bi-immune sets. We demonstrate the existence of incomparable pT-immune degrees in deterministic time classes.