Search

The Wang tiling is a classical problem in combinatorics. A major theoretical question is to find a (small) set of tiles which tiles the plane only aperiodically. In this case, resulting tilings are rather restrictive. On the other hand, Wang tiles are used as a tool to generate textures and patterns in computer graphics. In these applications, a set of tiles is normally chosen so that it tiles the plane or its sub-regions easily in many different ways. With computer graphics applications in mind, we introduce a class of such tileset, which we call sequentially permissive tilesets, and consider tiling problems with constrained boundary. We apply our methodology to a special set of Wang tiles, called Brick Wang tiles, introduced by Derouet-Jourdan et al. in 2016 to model wall patterns. We generalise their result by providing a linear algorithm to decide and solve the tiling problem for arbitrary planar regions with holes.

We introduce a formalization of a fuzzy relational database model using relational calculus on the category of fuzzy relations. We also introduce general formulas for the notion of database operations such as ’projection’, ’selection’, ’injection’ and ’natural join’ which can be used for both traditional and fuzzy database models. We prove several elementary properties of database operations using relational calculus. Next we demonstrate the truck backer-upper control problem using our formulation. Every fuzzy states, operation strategies, and solving procedures are described by database tables and formulas of relational calculus. We also show examples of computations of fuzzy relational databases using our Mathematica implementation.

Using a simple three-country model of international duopoly, this study analyzes the optimal choice of rules of origin (ROO) in a free trade area/agreement (FTA) when firms from outside the FTA must undertake foreign direct investment (FDI) in FTA countries and conduct part of their production process within the FTA to comply with the ROO. FDI causes spillovers of the superior production technology from a non-FTA firm to its competitor within the FTA, depending on how much of the production process is shifted to the FTA area. In this situation, this study predicts that as the degree of multilateral trade liberalization before formation of the FTA is higher, the optimal ROO tends to be less stringent.

We examine the optimal rules of origin (ROO) in a free trade area/agreement (FTA) by employing a stylized three-country partial equilibrium model of an international duopoly. We incorporate compliance costs of the ROO into the model. In particular, compliance costs are higher for a firm located in a non-member country of the FTA than for a firm (an internal firm) located in an FTA member country, whereas marginal production costs are lower for the former. The FTA member countries set the optimal level of ROO to maximize their joint welfare. An importing country within the FTA imposes tariffs on imports that do not comply with the ROO. We show that the optimal ROO may have a protectionist bias in the sense that they are set for only the internal firm to comply. ROO may also cause low utilization of FTAs when they are set such that even the internal firm does not comply with them. These cases arise depending on parameter values.

For positive integers $m$ and $n$, we denote by $\mathrm{BH}(m,n)$ the set of all $H\in M_{n\times n}(\mathbb{C})$ such that $HH^\ast=nI_n$ and each entry of $H$ is an $m$-th root of unity where $H^\ast$ is the adjoint matrix of $H$ and $I_n$ is the identity matrix. For $H_1,H_2\in \mathrm{BH}(m,n)$ we say that $H_1$ is \textit{equivalent} to $H_2$ if $H_1=PH_2 Q$ for some monomial matrices $P, Q$ whose nonzero entries are $m$-th roots of unity. In this paper we classify $\mathrm{BH}(17,17)$ up to equivalence by computer search., Comment: 9 pages

We have implemented a certified Wang tiling program for tiling a rectangle region using a brick corner Wang tile set. A brick corner Wang tile set is a special Wang tile set introduced by A. Derouet-Jourdan et al. in computer graphics in 2015 to model wall patterns texture. We have implemented a tiling algorithm using Coq proof assistant and proved its correctness. This correctness assures the existence of a tiling of any brick corner Wang tile set for any size of rectangle. The essential points of our proof are the existence of a tiling for a $2 \times 2$ rectangle and a simple induction process. Since the brick corner Wang tile is a class of infinite kinds of tile sets, it is not straightforward and there are many conditional branches to prove the correctness. The certification with Coq assures that there are no lack of conditions.

We implemented a Mathematica module of CGA which includes functions to denote CGA elements and compute several operations in CGA. We can draw the figure in 3D space which is corresponding to a CGA element. Our draw function is using Gr\"{o}bner Basis for simplifying equations of figures. It can be used for any dimensional figures. One of our motivations is to realize 3D origami system using our own CGA Library. We follow the 2D computational origami system E-Origami-System developed by Ida et.al. and formulated simple fold operations in 3D by using CGA points and motions. Then, we proved some geometric theorems about origami properties by computing CGA equation formulas.

One of our goals is to formalize an equivalence class(FEC) of the fuzzy relational database(FRDB). FRDB, an extension of RDB using a soft computing technique, fuzzy theory. Using our relational formulas of relational calculus, we can denote its properties by simple and correct formulas. Also, we can prove its properties formally using relational calculus. There are many applications of FRDB such as managing hyperlinks of web pages, customer relationship management (CRM), etc. Our motivation is developing formal verification tools for a software system using FEC of FRDB. We also formalize database operations such as “projection”, “selection”, and “natural join”. We prove several elementary properties of natural join operations using our formalization.

Fuzzy formal concept analysis(FFCA) is a development of formal concept analysis(FCA) with the degree of relation between objects and attributes. Using FCA approach, we will investigate the condition logical implication for fuzzy functional dependency. We also use Armstrong's rule to define soundness and completeness of our implication and fuzzy functional dependency model. We show difference and equivalence condition between fuzzy implication and fuzzy functional dependency. This condition can be used to develop the algorithm for finding attribute dependency.

In this paper we investigate quantum cellular automata whose global transitions are defined using a global transition function of classical cellular automata. And we prove the periodicity of behaviors of some quantum cellular automata.

Wall patterns are essential in the creation of textures for visually rich buildings. Particularly, irregular wall patterns give an organic and lively feeling to the building. In this chapter, we introduce a modeling method for wall patterns using Wang tiles which are known for creating aperiodic tiling of the plane under certain conditions. We introduce a class of Wang tiles and prove that any rectangle with border constraints and bigger than a \(2\times 2\) rectangle can be tiled. We use this proof to derive a tiling algorithm that is in linear time. Finally, we give some results of our algorithm and compare the computation time with previous Wang tiling algorithms introduced in computer graphics.

We consider a graph with labels of edges. A label means the length of an edge. We present a method to compute the length of the shortest path between two vertices using graph transformations. We introduce graph transformation rules which preserve the length of paths. Reducing to a simple graph which contains two vertices, we finally calculate the length of the shortest path of those two vertices. There were several algorithms for computing network reliabilities using graph transformations. We use the same framework as those algorithms for applying the graph transformation rules, but our transformation rules do not calculate the network reliabilities but calculate the length of the shortest path. 1. Introduction Graph transformation (graph reduction or graph rewriting) techniques are useful for developing an algorithm to compute several values of graph properties in the area such as circuits and networks. Politof and Satyanarayana (1986a) introduced a polynomial-time algorithm for the computation of network reliability for some restricted class of graphs, and Satyanarayana and Wood (1985) studied O (I E I)-time algorithms for kterminal reliability for series and parallel graphs. Politof and Satyanarayana (1986b) studied allterminal reliability for IFCF (inner for cycle free) graphs and they also presented O(IV D)-time algorithms for PCF (planar cube free) graphs. In these studies graph transformation methods were introduced to compute network reliabilities. Network graphs were classified into some class, e.g. IFCF graphs and PCF graphs, to give efficient algorithms using graph transformation methods. Okada and Hayashi (1991) showed the theoretical results about critical pair lemma for the graph transformation rules introduced by Politof and Satyanarayana (1986a; 1986b) . The notion of critical pair was firstly considered in the area such as studies of term rewriting systems. In Mizoguchi and Kawahara (1995) and Mizoguchi (1999) the concept of critical pair lemma was generalized to a graph rewriting system, and a complete graph rewriting system was introduced to computes network reliabilities such as Okada and Hayashi (1991) . In this paper, we introduce graph transformation rules to search the shortest path and compute its length for given graphs and construct an O (I E D-time algorithms for series and parallel graphs. Application of those rules yields to the shortest path and its * Department of Informatics , Kyushu University, 33 Fukuoka 812-8581, Japan. masa@i.kyushuu.ac.jp t Faculty of Mathematics , Kyushu University, 33 Fukuoka 812-8581, Japan. ym@math.kyushuu.ac.jp

We introduce computational models, such as sequential machines and automata, using the category theory. In particular, we introduce a generalized theorem which states the existence of the most efficient finite state automaton, called the minimal realization. First, we introduce set theoretical elementary models using sets and functions. We then consider a category of sequential machines which is an abstract model of finite automata. In the category theory, we consider several properties of compositions of morphisms. When we look at the category of sets and functions, we describe properties using equations of compositions of functions. Since the theory of category is a general theory, we can have many concrete properties from a general theorem by assigning it to specific categories such as sets and functions, linear space and linear transformations, etc.

We implemented operations appeared in the theory of automata using the Coq proof-assistant. A language which contains infinite elements is defined using ssreflect (a Small Scale Reflection Extension for the Coq system). We also implemented the modules for sticker systems. Paun and Rozenberg introduced a concrete method to transform an automaton to a sticker system in 1998. One of our aims is to present formal proofs of the correctness of their transformation. We modified some of their definitions to improve their insufficient results. We note that all of our formulation are written in Coq and we show some examples of machine-checkable proofs.

This paper studies two‐dimensional cellular automata ca−90(m,n) having states 0 and 1 and working on a square lattice of size (m−1)×(n−1). All their dynamics, driven by the local transition rule 90, can be simply formulated by representing their configurations with Laurent polynomials over a finite field F2={0,1}. The initial configuration takes the next configuration to a particular configuration whose cells all have the state 1. This paper answers the question of whether the initial configuration lies on a limit cycle or not, and, if that is the case, some properties on period lengths of such limit cycles are studied.

A new kind of computing system, a graph reduction system, is introduced using the original notation of graphs. Every graphs and reduction procedures are defined just like as term rewriting systems. Several properties of graphs and graph reductions are studied from the viewpoint of our graph reduction system. Especially, we investigate the ability of parallel reductions and compare parallel reductions with sequential reductions. We formalize the concepts of parallel reductions and sequentially simulatable parallel reductions. Sufficient conditions for reduction rules which guarantees the consistency of parallel reductions and sequential reductions are given. It is also showed that every parallel reduction preserves correctness of solutions for the graph reduction system solving equations of regular expressions.

A box-ball system is a kind of cellular automata obtained by the ultradiscrete Lotka-Volterra equation. Similarities and differences between behavious of discrete systems (cellular automata) and continuous systems (differential equations) are investigated using techniques of ultradiscretizations. Our motivations is to take advantage of behavious of box-ball systems for new kinds of computations. Especially, we tried to find out useful periodic box-ball systems(pBBS) for random number generations. Applicable pBBS systems should have long fundamental cycles. We focus on pBBS with at most two kinds of solitons and investigate their behaviours, especially, the length of cycles and the number of orbits. We showed some relational equations of soliton sizes, a box size and the number of orbits. Varying a box size, we also found out some simulation results of the periodicity of orbits of pBBS with same kinds of solitons.

We study a quantum cellular automaton (QCA) whose time-evolution is defined from global transition function of classical cellular automata (CA). In order to investigate natural transformations from CA to QCA, the present QCA includes CA with Wolfram's rule 150 and 105 as special cases. We firstly compute the time-evolution of the QCA and examine its statistical properties. As a basic statistical value, the probability of finding an active cell averaged over a spatial-temporal space is introduced, and the difference between CA and QCA is considered. In addition, it is shown that statistical properties in QCA are related to the classical trajectory in the configuration space., 20 pages,4 fgures

Discrete quantum cellular automata are cellular automata with reversible transition. This paper deals with 1d cellular automata with finite cell array and triplet local transition rules. We present the necessary condition of local transition rules for cellular automata to be reversible, and prove the reversibility of some cellular automata.

In this paper we present a basic notion of relational structures which includes simple graphs, labelled graphs and hypergraphs, and introduce a notion of partial morphisms between them. An existence theorem of pushouts in the category of relational structures and their partial morphisms is proved under a certian functorial condition, and it enables us to discuss single pushout rewritings of relational structures.

Summary A categorical interpretation of assertion (axiomatic) semantics of programming languages is proposed. All of the preconditions, postconditions, and programs are interpreted as (binary) relations in topoi with the use of relational calculus, and several fundamental properties of Dijkstra's weakest preconditions are proved. Assertions in the semantics depend on intuitionistic logic, so this is an extension of the assertion semantics due to E. G. Manes and M. A. Arbib

To implement Ginzburg's equality check procedure for regular expressions by using personal computers, we propose a new and more efficient axiom system consisting of an axiom and inference rules concerning a new relational symbol C in addition to a part of Salomaa's axiom system. The researches of axiom systems for the regular expressions started in the 60's. Redco [4] showed that it is impossible to make a complete axiom system with finite axioms and only one inference rule R1. He made a complete system with countably many axioms and an inference rule Rl. Salomaa [5] showed a complete and consistent axiom system by using two inference rules RI and R2. In his system every tautology has a constructive proof. But the construction of a proof is so complicated that it is not useful for practice. After a few years, Ginzburg [2] showed a simple mechanical procedure for checking equality of regular expressions by using derivatives. This method uses transition graphs so it is neither symbolic nor axiomatic. In the present paper, by using symbolic derivatives, we improve Ginzburg's procedure to a symbolic and axiomatic one. Moreover we examine which axiom in Salomaa's system is essen tial for showing the validity of the procedure. We choose some axioms which is useful for mechanical procedure, and we show that it is sufficient to show the termination of the checking procedure by using only those axioms. In section 2, we recall Salomaa's system Fi and introduce a new system F. In section 3, we show that in the system F*, the set of all symbolic derivatives of a regular expression is finite. This result guarantees the termination of improved Ginzburg's equality check procedure. In section 4, we introduce a new relational symbol C, and we improve the system F* to a more efficient system F+. Since we do not use an axiom of associative laws in the system F+, we can check equalities by a straightforward method. We implemented the efficient procedure on a personal computer. So we can easily check the equality of two regular expressions. Moreover we get the transition graphs which accept the expressions together with the answer of the equality. We show a brief example in the Appendix.

We construct a powerset monad, a filter monad and a primefilter monad in the category $ M $-Set of sets with $ M $-actions. To investigate the categories of algebras of these monads in $ M $-Set, we consider the category of complete semilattices (resp. continuous lattices, compact Hausd orff spaces) with $ M $-actions. We show that if $ M $ is a group, this category is isomorphic to the category of algebras of the powerset monad (resp. filter monad, primefilter monad) in $ M $-Set.