萩原 学

This paper presents a formula for the cardinality of a class of BAD correcting codes proposed at ISIT2017. Furthermore, we show that the cardinality is approximately optimal. In other words, the ratio of the cardinality of the code and that of maximal cardinality BAD correcting code converges to 1 for sufficiently large length.

Invented in the 1960s, permutation codes have reemerged in recent years as a topic of great interest because of properties making them attractive for certain modern technological applications, especially flash memory. In 2011 a polynomial time algorithm called linear programming (LP) decoding was introduced for a class of permutation codes where the feasible set of codewords was a subset of the vertex set of a code polytope. In this paper we investigate a new class of linear constraints for matrix polytopes with no fractional vertices through a new concept called "consolidation." We then introduce a necessary and sufficient condition for which LP decoding methods, originally designed for the Euclidean metric, may be extended to provide an efficient decoding algorithm for permutation codes with the Kendall tau metric.

Permutation codes, in the form of rank modulation, have shown promise for applications such as flash memory. One of the metrics recently suggested as appropriate for rank modulation is the Ulam metric. Multipermutation codes have also been proposed as a generalization of permutation codes that would improve code size. In this paper we analyze the Ulam metric in the context of multipermutations, noting similarities and differences with the Ulam metric in the context of permutations. We then consider sphere sizes for multipermutations under the Ulam metric and resulting bounds on code size.

In this paper, we formalize the channel capacity of the binary symmetric erasure channel (BSEC) by using a proof-assistant system called Coq/SSReflect. This study is for the formalization of the fact that the binary symmetric channel (BSC) and binary erasure channel (BEC), which were previously formalized, are specializations of the BSEC.

A short proof for the s-deletion error-correction property of Helberg codes is given.

Classes of multi insertion/deletion error-correcting codes based on order theory and axiomatic algebra are proposed by an abstraction of Helberg's construction.

In this paper we report on work done to formalize coding theory in the Lean theorem prover, released by Microsoft Research and Carnegie Mellon University in 2015. We formalize definitions and theorems in a downloadable library named "Cotoleta" (COding Theory Over the LEan Theorem proof Assistant). This is the first coding theory library for Lean. Our formalization includes new template-like structures for formalizing error-correcting systems. As examples, repetition codes and the Ilamming (7,4) code are formalized using these structures. The reader is assumed to have some knowledge of information and coding theory but no formalization experience is assumed.

Bing's shrinking method is a key technique for constructing homeomorphisms between topological manifolds in geometric topology. Applications of this method include the generalized Schoenflies theorem, the double suspension theorem for homology spheres, and the 4-dimensional Poincare conjecture. Homeomorphisms obtained in this method are sometimes counter-intuitive and may even be pathological. This makes Bing's shrinking method a good target of formalization by proof assistants. We report our formalization of this method in Coq/Ssreflect.

The possibility of perfect permutation codes in the Ulam metric is explored, motivated by recent proposals of rank modulation schemes for flash memory devices. First a method of calculating sphere size of permutations under the Ulam distance utilizing Young tableaux is introduced. The nonexistence of perfect permutation codes in the Ulam metric is then proven.

The extraction of a stable signal from noisy data is very useful in applications that aim to combine it with a cryptographic key. An approach based on an error correcting code was proposed by Dodis et al., which is known as a fuzzy extractor. Physical unclonable functions (PUFs) generate device-specific data streams, although PUFs are noisy functions. In this paper, we describe a method for preparing a PUF key during fuzzy extractor implementation. The experimental results showed that all possible combinations of input message length and the number of correctable errors were tested for a BCH code with codeword length N, which was the length of the PUF responses. © Springer-Verlag Berlin Heidelberg 2014.

Modern mathematical proofs are becoming so big that they cause a problem of trust. Formal verification using proof-assistants has recently emerged as a solution to ensure the correctness of big proofs. Before being able to verify formally big proofs one must build substantial libraries of formal definitions and formal theorems. In this paper, we explain how we contribute to an existing formalization of information theory by extending it with a foundational theorem; namely, the variable-length source coding theorem.

Physical unclonable functions (PUFs) and biometrics are inherently noisy. When used in practice as cryptographic key generators, they need to be combined with an extraction technique to derive reliable bit strings (i.e., cryptographic key). An approach based on an error correcting code was proposed by Dodis et al. and is known as a fuzzy extractor. However, this method appears to be difficult for non-specialists to implement. In our recent study, we reported the results of some example implementations using PUF data and presented a detailed implementation diagram. In this paper, we describe a more efficient implementation method by replacing the hash function output with the syndrome from the BCH code. The experimental results show that the Hamming distance between two keys vary according to the key size and information-theoretic security has been achieved.

Entangled states play crucial roles in quantum information theory and its applied technologies. In various protocols such as quantum teleportation and quantum key distribution, a good entangled state shared by a pair of distant players is indispensable. In this paper, we numerically examine entanglement sharing protocols using quantum LDPC CSS codes. The sum-product decoding method enables us to detect uncorrectable errors, and thus, two protocols, Detection and Resending (DR) protocol and Non-Detection (ND) protocol are considered. In DR protocol, the players abort the protocol and repeat it if they detect the uncorrectable errors, whereas in ND protocol they do not abort the protocol. We show that DR protocol yields smaller error rate than ND protocol. In addition, it is shown that rather high reliability can be achieved by DR protocol with quantum LDPC CSS codes.

In recent years permutation codes have emerged as a field of great interest with new applications being suggested. In this paper we investigate two distance metrics and their induced weight functions on subgroups of the symmetric group, S-n, of permutations on n elements. Specifically, we introduce the Euclidean weight and compare its weight distribution to that of the Kendall tau weight. Our primary contribution is to extend LP (linear programming) decoding methods invented for permutation codes endowed with a Euclidean distance metric to codes utilizing the Kendall tau distance metric.

The most fundamental results of information theory are Shannon's theorems. These theorems express the bounds for reliable data compression and transmission over a noisy channel. Their proofs are non-trivial but rarely detailed, even in the introductory literature. This lack of formal foundations makes it all the more unfortunate that crucial results in computer security rely solely on information theory (the so-called "unconditional security"). In this paper, we report on the formalization of a library for information theory in the SSReflect extension of the Coq proof-assistant. In particular, we produce the first formal proofs of the source coding theorem (that introduces the entropy as the bound for lossless compression), and the direct part of the more difficult channel coding theorem (that introduces the capacity as the bound for reliable communication over a noisy channel). © 2012 Springer-Verlag.

A set of linearly constrained permutation matrices are proposed for constructing a class of permutation codes. Making use of linear constraints imposed on the permutation matrices, we can formulate a minimum Euclidian distance decoding problem for the proposed class of permutation codes as a linear programming (LP) problem. The main feature of this novel class of permutation codes, called LP decodable permutation codes, is this LP decodability. It is demonstrated that the LP decoding performance of the proposed class of permutation codes is characterized by the vertices of the code polytope of the code. In addition, based on a probabilistic method, several theoretical results for randomly constrained permutation codes are derived. © 2011 IEEE.

In this paper, we propose a construction method for two-level quantum error-correcting codes via non-binary LDPC codes over an extended field of order 2(p), p an integer p > 1. The proposed quantum error-correcting codes are based on binary quasi-cyclic LDPC codes which have almost achieved a "Bounded Distance Decoding (BDD)" limit but have not surpassed the limit yet. Quantum codes constructed from the proposed method surpass the BDD limit. Furthermore the codes outperform the efficiently-decodable state-of-the-art quantum codes.

For designing low-density parity-check (LDPC) codes for quantum error-correction, we desire to satisfy the conflicting requirements below simultaneously. 1) The row weights of parity-check "should be large": The minimum distances are bounded above by the minimum row weights of parity-check matrices of constituent classical codes. Small minimum distance tends to result in poor decoding performance at the error-floor region. 2) The row weights of parity-check matrices " should not be large": The performance of the sum-product decoding algorithm at the water-fall region is degraded as the row weight increases. Recently, Kudekar et al. showed spatially-coupled (SC) LDPC codes exhibit capacity-achieving performance for classical channels. SC LDPC codes have both large row weight and capacity-achieving error-floor and water-fall performance. In this paper, we propose a new class of quantum LDPC codes based on spatially coupled quasi-cyclic LDPC codes. The performance outperforms that of quantum "non-coupled" quasi-cyclic LDPC codes.

In this paper, we investigate the smallest value of p for which a (J. L. p)-QC LDPC code with girth 6 exists for J = 3 and J = 4. For J = 3, we determine the smallest value of p for any L. For J = 4, we determine the smallest value of p for L <= 301. Furthermore we provide examples of specific constructions meeting these smallest values of p.

符号理論はディジタル情報の信頼性確保のために不可欠な理論であり，現在の情報化社会を支える基盤理論の一つである．この理論は約60 年前に米国で生まれたが，日本でもこの時期から符号理論の研究が行われていた．しかし，研究者が増え，国際的に認められる研究成果が出るようになったのは40～50 年前のことである．それには，この研究を米国で始めた方々の帰国とW. W. Peterson の著書の影響が大きい．このころ，日本において現在につながる符号理論研究の原点が形成されたといってよいだろう．その後，特に符号理論の応用の面で日本は世界を先導する役割も担ってきた．この間，符号理論は何度かの大きな変革を経ながら，その応用範囲を拡大しつつ発展を続けてきている．本稿では，このような符号理論の流れを日本の視点から俯瞰する．