Transition Systems over Continuous Time-Space

Complexity and Computability in Analisys 2005, Informatik Berichte, Fern Universität Hagen (Technical Report), 320, 157-168, 2004

This paper gives transition systems over continuous time-space, which are systems of functions of continuous time-space into descrete states. These systeme are situated between the cellular automata and the partial differential equations. This paper shows the reasonable sufficient condition of the uniquness of the solution.

ps file [290KB]

ps.gz file [101KB]

pdf file [256KB]

pdf.gz file [119KB]

Effective Limit in Computable Analysis

This paper introduce the notion of effective limit, which gives an alternative definition of effective uniform topology. The aim of this paper is to combine the precedent works of algebraic structure and of limit structure, which have appeared in studies of computable analysis. This paper also compares the definition of computable functions based on representations and that based on computability structure, and shows that both of them are essentially equivalent to each other.

ps file [200KB]

ps.gz file [70KB]

Systems of logic for necessarity

This paper discusses a theory of modal predicate logic, which is based on S5. This paper gives four ways to define this theory. The first way is to define a system which tells whether a context supports a formula or not. In this way we evaluate a formula with not a model but a context. This theory distinguish occasional equality from necessary equality, as is discussed with the problem of referentially opaque context. The aim of this paper is to observe the mathematical properties of this theory. The second way is a derivation system of Hirbert-style, which is given by adding new axiom schemata to the rules of S5. The third is a derivation system of Gentzen-style, where a sequent is not a sequence of formulae but a table of formulae. his system satisfies cut elimination. The fourth is a kind of possible-world semantics. In the fourth way, a formula is valid when the formula is true in each partial abstraction models. This paper shows the equivalence of these four ways, that is, these four ways define the same theory.

ps file

ps.gz file

The Theory of Parametricity in Lambda Cube

This paper defines the theories of parametricity for the system lambda-P-omega in lambda cube, and shows some of its application. These theories are defined by the axiom sets in the formal theories. These theories prove various important semantical properties in the formal systems.

ps.gz file

The measure of an omega regular language is rational

An omega regular language is the omega language which is recognised by a Buchi automaton. It has been known that the measure of an omega regular language recognised by a deterministic Buchi automaton is a rational number. This paper shows the measure of every omega regular language is a rational number.

tex file

tex.gz file

ps file

ps.gz file

Kamo Hiroyasu, Kawamura Kiko & Takeuti Izumi:
``Computational Complexity of Fractal Sets''

Real Analysis Exchange, 26, pp1-21, 2001.

Conference version: ``Hausdorff Dimension and Computational Complexity'', Complexity and Computability in Analisys, Informatik Berichte, Fern Universitat Hagen (Technical Report) 235, pp41-50, 1998.

In studies on fractal geometry, there has been an important question which is whether classification by means of computable complexity is independent to classification by means of fractal dimension or not. In this paper, we will show that each self-similar set defined by polynominal time computable functions is in computable complexity P, if the self-similar set satisfies polynominal time open condition. This fact provides us examples of sets with P as its computable complexity and a noninteger as its Hausdorff dimension. We also construct a set with NP-complete as its computable complexity and an integer as its Hausdorff dimension. These two examples work as an evidence of independency of computable complexity and Hausdorff dimension.

ps.gz file tex file

Effective fixed point theorem over a non-separable metric space

Computability and Complexitu in Analysis, Infrmatik Berichte 272-9/2000, Fachberich Informatik, Fern Universitaete, Gesamthochschule in Hagen

This paper shows effective fixed point theorem for computable contractions. Effective fixed point theorem for computable contractions over a computably separable space is easily shown. A function over a separable space is represented by a Type-1 function, and the fixed point of a contraction is given by iteration of such Type-1 function. If the contraction is computable, then its fixed point is also computable. If the support space is not computably separable, the method above is not available. The function space of an interval into real numbers is not separable with polynominal time computability. This paper show the fixed point theorem for such non-separable spaces. This theorem is proved with iteration of Type-2 functionals. As an example of that, this paper shows that Takagi function is a polynominal time computable function.

ps.gz file

Pruning Terms for Principal Type Assignment

The proceedings of CATS2000, ENTCS, vol. 31.

Affine terms are lambda terms in which no variable occurs twice, and linear terms are affine terms in which each bound variable occurs exactly once. The principal type of a term is the most general type which is assignable to the term. Hirokawa gave characterisations of the principal types of linear terms and of beta-normal affine terms. Shouji gave a characterisation of the principal types of beta-eta-normal linear terms. The proofs of these three theorems are parallel, but independent to each other. This paper points out that by using Berardi's pruning, the theorem on beta-normal affine terms is obtained from the theorem on linear terms. This is the first result. And also this paper shows a characterisation of principal types of beta-eta-normal affine terms. Its proof is obtained from the theorem on beta-eta-normal linear terms by Berardi's pruning. This is the second result. Besides, this paper gives other proofs of the the theorems on eta-normal terms. This is the third result.

ps file

ps.gz file in this cite

A type theory for cyclic structure

In: M. Sato & Y. Toyama Eds, 3rd Fuji workshop on functional and logic programming, to appear.

This work proposes a type theory for cyclic structure.
The type theory is a formal system which deals not only with cyclic structures, but also with functions over cyclic structures into other structures.
The various functions over cyclic structures can be defined by destructors of cyclic structures.

In order to construct the destructors, the system has three characteristic points.
The first is that the system distinguishes the type of already constructed terms of cyclic structures from the type of terms of cyclic structures under constructing.
The second is that the system has the type of cyclic graphs as the expressions of cyclic structures as well as the type of cyclic structures itself.
The third is that the system constructs terms with proving equations mutually.

This work gives a sound interpretation of the system into a parametric model of System F.
It implies the consistency of the system of this work.

ps.gz file

An Axiomatic System of Parametricity

Journal version :
Fundamenta Informaticae 33(1998) pp397-432 IOS Press.
Conference version:
P. de Groote, J. R. HIndley Eds, Typed Lambda Calculi and Applications, vol. 1210 of LNCS, pp354-372, 1997.

Abstract:

Plotkin and Abadi have proposed a syntactic system for parametricity on a second order predicate logic. This paper shows three theorems about that system. The first is consistency of the system, which is proved by the method of relativization. The second is that polyadic parametricities of recursive types are equivalent to each other. The third is that the theory of parametricity for recursive types is self-realizable. As a corollary of the third theorem, the theory of parametricity for recursive types satisfies the term extraction property.

Journal version: ps.gz file

Conference version: ps.gz file

An upper bound of the values of primitive recursive functionals

This paper gives an upper bound of its value explicitly with the Hardy function for each primitive recursive functional, In the proof, the author defines a sequence of terms. The sequence is cofinal in the terms by some suitable ordering. The sequence is used as a scale in terms.