36727244
Horn Clause Computation by Self-assembly of DNA Molecules
Kobayashi proposed Horn clause computation by DNA molecules, which is more suitable for expressing complex algorithms than other models for DNA computing. This paper describes a new implementation of Horn clause computation by DNA. It employs branching DNA molecules for representing Horn clauses. As derivations are realized by self-assembly of such molecules, the implementation requires only a constant number of laboratory operations. Furthermore, it deals with firstorder Horn clauses with some restrictions. In order to realize first-order logic, we implement variable substitutions by string tiling proposed by Winfree, et al. As we show the computational power of a Horn clause program in our model, we give another proof that a polynomial number of operations using self-assembly of DNA molecules can compute any problem in NP.
39613508
A Magic Pot : Self-assembly Computation Revisited
Molecular computing is a novel computing paradigm recently emerged from groundbreaking wet lab experiments by Adleman in 1994. His experimental work marks a potential capability and feasibility of "one pot" computing with molecules for solving hard problems of practical size.This paper concerns a molecular computing paradigm based on "self-assembly" and "screening mechanism". After a brief getting back to and reviewing Adleman's original work, we propose a new molecular implementation method based on length-only encoding, which leads us to much simpler molecular implementation techniques to solve graph problems.With two examples, we demonstrate the effectiveness of the molecular implementation method for one pot computing based on self-assembly: one is Nondeterministic Finite Automaton Pot and the other Hamiltonian Path Problem Pot.
62399989
Proceedings of the 8th international conference on Grammatical Inference: algorithms and applications
28066504
Multiple splicing systems and the universal computability
We propose a new extension of splicing systems, called multiple splicing systems, based on a kind of logic grammars. First, we introduce a class of Elementary formal systems, called simple H-form EFS, and show that its generative power is equivalent to the class of basic splicing systems (the original Head's splicing system) and is more adequate as representation device for formal languages. Next, we gradually extend the simple class of EFSs and get a very natural extension of splicing systems, multiple splicing systems. We show that multiple splicing systems have universal computability.
32287187
Sticker systems with complex structures
Abstract In this paper, we propose a variant of sticker systems which uses molecules with complex structures. Since the original sticker systems (Paun et al. (1998) [2, 8]) working on double strands of DNA have been studied as a formal model for self-assembly in DNA computing, we extend the sticker systems to working on more complex (higher-order) structures of DNA molecules. The advantage of sticker systems with complex structures is that augmented with weak codings we can obtain the characterization of recursively enumerable languages by using only sticking (hybridization) operations for complex molecules, while the usual sticker systems require more complicated operations such as the simultaneous use of couples of dominoes or coherent computations besides morphisms.
207106066
Families of Noncounting Languages and Their Learnability from Positive Data
This paper introduces some subclasses of noncounting languages and presents some results on the learnability of the classes from positive data. We first establish several relationships among the language classes introduced and the class of reversible languages. Especially, we introduce the notion of local parsability, and define a class (k, l)-CLTS, which is a subclass of the class of concatenations of strictly locally testable languages. We show its close relation to the class of reversible languages. We then study on the relationship between the closure of the Boolean operations and the learnability in the limit from positive data only. Further, we explore the learnability question of some subclasses of noncounting languages in the model of identification in the limit from positive data. In particular, we show that, for each k, l≥1, (k, l)-CLTS is identifiable in the limit from positive data using reversible automata with the conjectures updated in polynomial time. Some possible applications of the result are also briefly discussed.
38971633
A New Translation for Semi-classical Theories - Backtracking without CPS
Most research of algorithm extraction from classical proofs is based on double negation translation or its variants. From the viewpoint of Curry-Howard isomorphism, double negation translation corresponds to CPS translation. Unfortunately, CPS translation makes resulting programs very complex. 
 
In this paper, we study a new translation for a semi-classical logic which is not based on double negation translation. Though it does not validate full classical logic, it translates Limit Computable Mathematics (LCM) into constructive mathematics. 
 
Our translation is inspired by game semantics with backtracking rules. Using the translation, we can extract an algorithm from a proof of a proposition A in LCM. The extracted algorithm gives a recursive winning strategy for the first mover of the game defined from A, at least when A is implication-free.
29272698
Monad as Modality
Abstract In 1989, Eugenio Moggi proposed a categorical framework for program semantics based on the notion of a strong monad. He showed that various kinds of computation can be modeled in his framework. On the other hand, strong monads are not suited for the categorical semantics of traditional modal logics. According to these observations, Moggi thought that the CurryHoward correspondence would not hold between programs and constructive proofs in modal logics. However, contrary to his view, we can show that proofs in a certain kind of modal logics are actually considered as programs. In this paper, first we shall introduce the notion of an l-strong monad which is a generalization of strong monads. Using this new notion, we can generalize Moggi's semantics-preserving soundness and completeness with respect to his equational logic. Next we shall show that l-strong monads give a sound and complete semantics of a constructive version of S4 modal logic. Finally, we present a method to extract a monad-based imperative functional program from a proof in the modal logic. Interestingly, this method can also be understood in terms of l-strong monads.
3026036
Towards a Semantic Wiki-Based Japanese Biodictionary
This paper describes an on-going project to develop and maintain a web-based Japanese Biodictionary within a Semantic Wiki environment. For the development of the dictionary, MediaWiki is extended to enable the writing of labeled links that represent RDF triples. The extension enables Semantic Wiki to provide not only collaborative environment for experts in various biol- ogy fields to create and edit the dictionary, but also the navigation support to manage relations between terms. Using a simple wiki syntax, people can de- velop and maintain the dictionary visually and easily.
8742017
Two Extensions of PX system
Abstract Two extensions of PX system will be discussed. The extensions are ctPX (catch/throw PX) and mvPX (multiple values PX). ctPX is a PX system extended with Nakano's catch/throw logic. ctPX enables to extract LISP programs with catch/throw mechanism form natural proofs. mvPX is a PX system which uses multiple values rather than lists to keep a finite sequences of data. Programs extracted by ctPX are more efficient than the ones by the original PX.