No description available.

No description available.

A one-dimensional cellular automaton is an infinite row of identical machines---the cells---which depend for their behaviour only on the states of their direct neighbours. This thesis introduces a new way to think about one-dimensional cellular automata. The formalism of Flexible Time allows one to unify the states of a finite number of cells into a single object, even if they occur at different times. This gives greater flexibility to handle the structures that occur in the development of a cellular automaton. Flexible Time makes it possible to calculate in an algebraic way the fate of a finite number of cells. In the first part of this thesis the formalism is developed in detail. Then it is applied to a specific problem of one-dimensional cellular automata, namely ether formation. The so-called ether is a periodic pattern of cells that occurs in some cellular automata: It arises from almost all randomly chosen initial configurations, and why this happens is not clear. For one of these cellular automata, the elementary cellular automaton with rule code 54, ether formation is expressed in the formalism of Flexible Time. Then a partial result about ether formation is proved: There is a certain fragment of the ether that arises with probability 1 from every random initial configuration, and it is then propagated with probability 1 to any later time. The persistence of the ether fragment is a strong argument that the ether under Rule 54 indeed arises from almost all input configurations. The result only requires that the states of the cells are chosen independently and with equal probability distributions, and that all cell states can occur. This is not yet a full proof of ether formation, but it is derived by formal means, not just by computer simulations.

No description available.

No description available.

Human beings from the moment they understood the power of their brain tried to create things to make their life easier and satisfy their needs either physical or mental. Inventions became more and more complicated, covering almost every aspect of human life and satisfying the never ending human curiosity. One of the reasons for this complexity is that an increasing number of systems exhibit concurrency. The development of concurrent systems is generally challenging since it is more difficult to fully understand their exact behaviour. In this thesis We present and investigate two of the most widely used and well studied theories to capture concurrent behaviour. Based on the results of PBC, we develop two algebras, one based on term re-writing and the other on Petri nets, aimed at the Specification and analysis of concurrent systems with timing information. The former is based on process expressions (at-expressions) and employs a set of SOS rules providing their operational semantics. The latter is based on a class of Petri nets with time restrictions associated with their arcs, called at-boxes, and the corresponding transition firing rule. We relate the two algebras through a compositionally defined mapping which for a given at-expression returns an at- box with behaviourally equivalent transition system. The resulting framework consisting of the two algebras is called the Timed-Arc Petri Box Calculus, or atPBC.

Les systèmes pédagogiques sont apparus récemment à propos des calculs propositionnels (jusqu'à l'ordre supérieur), et consistent à donner systématiquement des exemples des notions (hypothèses) introduites. Formellement, cela signifie que pour mettre un ensemble Delta de formules en hypothèse, il est requis de donner une substitution sigma telle que les instances de formules sigma(Delta) soient démontrables. Cette nécessité d'exemplification ayant été pointée du doigt par Poincaré (1913) comme relevant du bon sens: une définition d'un objet par postulat n'ayant d'intérêt que si un tel objet peut être construit. Cette restriction appliquée à des systèmes formels intuitionnistes rejoint l'idée des mathématiques sans négation défendues par Griss (1946) au milieu du siècle dernier, et présentées comme une version radicale de l'intuitionnisme. À travers l'isomorphisme de Curry-Howard (1980), la contrepartie calculatoire est l'utilité des programmes définis dans les systèmes fonctionnels correspondant: toute fonction peut être appliquée à un argument clos. Les premiers résultats concernant les calculs propositionnels jusqu'au second ordre ont été publiés récemment par Colson et Michel (2007, 2008, 2009). Nous exposons dans ce rapport une tentative d'uniformisation et d'extension au Calcul des Constructions (CC) des précédents résultats. Tout d'abord une définition formelle et précise de sous-système pédagogique du Calcul des Constructions est introduite, puis différents tels sous-systèmes sont déclinés en exemple / Pedagogical formal systems have appeared recently for propositional calculus (up to the higher order), and it consists of systematically give examples of introduced notions (hypotheses). Formally, it means that to use a set Delta of formulas as hypotheses, one must first give a substitution sigma such that all the instances of formulas sigma(Delta) can be proved. This neccesity of giving examples has been pointed out by Poincaré (1913) as a common-sense practice: a definition of an object by means of assumptions has interest only if such an object can be constructed. This restriction applied to intuitionistic formal systems is consistent with the idea of negationless mathematics advocated by Griss (1946) in the middle of the past century, and shown as a more radical view of intuitionism. Through the Curry-Howard isomorphism (1980), the computational counterpart is the utility of programs defined in the associated functional systems: every function can be applied to a closed value. First results concerning propositional calculi up to the second-order has recently been published by Colson and Michel (2007, 2008, 2009). In this thesis we present an attempt to standardize and to extend to the Calculus of Constructions (CC) those previous results. First a formal and precise definition of pedagogical sub-systems of the Calculus of Constructions is introduced, and different such sub-systems are exhibited as examples

This thesis reports on new music technology research which investigates the use of cellular automata (CA) for the digital synthesis of dynamic sounds. The research addresses the problem of the sound design limitations of synthesis techniques based on CA. These limitations fundamentally stem from the unpredictable and autonomous nature of these computational models. Therefore, the aim of this thesis is to develop a sound synthesis technique based on CA capable of allowing a sound design process. A critical analysis of previous research in this area will be presented in order to justify that this problem has not been previously solved. Also, it will be discussed why this problem is worthwhile to solve. In order to achieve such aim, a novel approach is proposed which considers the output of CA as digital signals and uses DSP procedures to analyse them. This approach opens a large variety of possibilities for better understanding the self-organization process of CA with a view to identifying not only mapping possibilities for making the synthesis of sounds possible, but also control possibilities which enable a sound design process. As a result of this approach, this thesis presents a technique called Histogram Mapping Synthesis (HMS), which is based on the statistical analysis of CA evolutions by histogram measurements. HMS will be studied with four different automatons, and a considerable number of control mechanisms will be presented. These will show that HMS enables a reasonable sound design process. With these control mechanisms it is possible to design and produce in a predictable and controllable manner a variety of timbres. Some of these timbres are imitations of sounds produced by acoustic means and others are novel. All the sounds obtained present dynamic features and many of them, including some of those that are novel, retain important characteristics of sounds produced by acoustic means.