Search

We define nominal equational problems of the form $$\exists \overline{W} \forall \overline{Y} : P$$ ∃ W ¯ ∀ Y ¯ : P , where $$P$$ P consists of conjunctions and disjunctions of equations $$s\approx _\alpha t$$ s ≈ α t , freshness constraints $$a\#t$$ a # t and their negations: $$s \not \approx _\alpha t$$ s ≉ α t and "Equation missing", where $$a$$ a is an atom and $$s, t$$ s , t nominal terms. We give a general definition of solution and a set of simplification rules to compute solutions in the nominal ground term algebra. For the latter, we define notions of solved form from which solutions can be easily extracted and show that the simplification rules are sound, preserving, and complete. With a particular strategy for rule application, the simplification process terminates and thus specifies an algorithm to solve nominal equational problems. These results generalise previous results obtained by Comon and Lescanne for first-order languages to languages with binding operators. In particular, we show that the problem of deciding the validity of a first-order equational formula in a language with binding operators (i.e., validity modulo $$\alpha $$ α -equality) is decidable.

A grammar compression algorithm, called GCIS, is introduced in this work. GCIS is based on the induced suffix sorting algorithm SAIS, presented by Nong et al. in 2009. The proposed solution builds on the factorization performed by SAIS during suffix sorting. A context-free grammar is used to replace factors by non-terminals. The algorithm is then recursively applied on the shorter sequence of non-terminals. The resulting grammar is encoded by exploiting some redundancies, such as common prefixes between right-hands of rules, sorted according to SAIS. GCIS excels for its low space and time required for compression while obtaining competitive compression ratios. Our experiments on regular and repetitive, moderate and very large texts, show that GCIS stands as a very convenient choice compared to well-known compressors such as Gzip 7-Zip; and RePair the gold standard in grammar compression; and recent compressors such as SOLCA, LZRR, and LZD. In exchange, GCIS is slow at decompressing. Yet, grammar compressors are more convenient than Lempel-Ziv compressors in that one can access text substrings directly in compressed form without ever decompressing the text. We demonstrate that GCIS is an excellent candidate for this scenario, because it shows to be competitive among its RePair based alternatives. We also show that the relation with SAIS makes GCIS a good intermediate structure to build the suffix array and the LCP array during decompression of the text.

Parallel island models are used to increase accuracy and performance (speed-up) of meta-heuristics. Such models provide gains by the exchange of information between islands through the migratory process. The key to obtaining gains with parallel island models is the manipulation of migration parameters, since depending on how these parameters are handled the gains vary. Based on this assumption, this work uses three meta-heuristics: genetic algorithm, self-adjusting particle swarm optimization and social spider algorithm. From each metaheuristic, parallel island models were proposed, diversifying the number of natives on the islands, and the behavior of these models were studied. The assessment confirmed the impact of variations migration parameters on accuracy and performance as well as the importance on the number of natives located on the islands. The best solutions were obtained with island models from genetic algorithm and self-adjusting particle swarm optimization, and the best speedups were achieved with island models from social spider algorithm.

The nominal approach allows us to extend first-order syntax and represent smoothly systems with variable bindings, using nominal atoms instead of variables and dealing with renaming through permutations of atoms. Nominal unification is, therefore, the extension of first-order unification modulo \(\alpha \)-equivalence by taking into account this nominal setting. In this work, we present a specification of a nominal C-unification algorithm (nominal unification with commutative operators) in PVS and discuss the proofs of soundness and completeness. Additionally, the algorithm has been implemented in Python. In relation to the only known specification of nominal C-unification, there are two novel features in this work: first, the formalization of a functional algorithm that can be directly executed (not just a set of non-deterministic inference rules); second, simpler proofs of termination, soundness and completeness, due to the reduction in the number of parameters of the lexicographic measure, from four parameters to only two.

A formalisation of soundness of the notion of α-equivalence in nominal abstract syntax modulo associative (A) and associative-commutative (AC) equational theories is described. Initially, the notion of α-equivalence is specified based on a so called “weak” nominal relation as suggested by Urban in his nominal development in Isabelle/HOL. Then, it is formalised in Coq that this equality is indeed an equivalence relation. After that, general α-equivalence with A and AC function symbols is specified and formally proved to be an equivalence relation. As corollaries, the soundness α-equivalence modulo A and modulo AC is obtained. Finally, an algorithm for checking α-equivalence modulo A and AC is proposed. General α-equivalence problems are log-linearly solved while AC and the combination of A and AC α-equivalence problems have the same complexity as standard first-order approaches. This development is a first step towards verification of nominal matching, unification and narrowing algorithms modulo equational theories in general.

In the days of its foundation, the field of science covered by UNIF – a series of annual international workshops on unification – was still in its infancy. With the advent of automated reasoning, term rewriting, logic programming, natural language processing, and program analysis, the areas of computer science concerned by unification were seething with excitement. With the coming out of researches in constraint solving and admissibility of inference rules and with the breaking out of applications, such as type checking, query answering, and cryptographic protocol analysis, the development of unification was not long in going at full speed.

The task mapping problem of real-time applications onto a homogeneous multiple processors system-on-a-chip (MPSoC) is an NP-complete problem that can be addressed using search-based meta-heuristic methods. A particular case is the priority preemptive wormhole-based Network-on-a-Chip (NoC) communication architecture that takes into consideration the end-to-end schedulability analysis. In this paper, we present a Adaptive Genetic Algorithm (AGA) with adaptive parameter control strategies that is capable of efficiently achieving schedulable task placements. In our experiments, we perform analytic methods in different scenarios with multiple synthetically generated real-time applications, as well as various platforms with a ranging number of processors to provide a statistical study comparing our algorithm against a standard genetic algorithm approach.

Designing efficient parallel island Genetic Algorithms (GA) is a difficult task: several decisions are needed related to the adequate structure of the islands, how they are connected, how many individuals should migrate, and how often they should migrate. The impact of these choices has not yet been fully understood since they might vary for different problems. In previous work, a variety of island model GAs to solve Reversal Distance Problem (RDP) over uni-crhomosomal genomes were proposed from which adequate choices were pointed out that provided results with an excellent balance among accuracy and performance. In this work, another evolutionary problem is considered in order to analyze how general were the decisions taken for island model GAs over RDP. The problem is translocation distance over multi-chromosomal genomes, which involves the interchange of gene between different chromosomes. Despite the fact that this problem falls also in the category of evolutionary distance problems, it is different from the RDP. Regarding accuracy, island models using a dynamic communication topology for exchange of individuals between islands provided the best solutions; while regarding performance, models using a static topology reached the highest speedup. Comparing with previous work on RDP, it was observed that islands models that did not provided good accuracy in RDP provided good quality solutions for translocation distance problem, while the best island models for RDP did not repeat the same success for translocation distance problem. The only invariant is that all the island model GAs in addition to competitive speedups provided better results than the corresponding sequential GA.

The construction of correct software, i.e. a computer program that meets a given specification, is an important goal in Computer Science. Nowadays, not only critical software (the ones used in aircraft, hospitals, banks, etc.) is supposed to provide additional guarantees of its correctness. Nevertheless, this is not an easy task because proofs are often long and full of details. In this sense, a strong background in logical deduction is essential to provide Computer Science (CS) professionals the necessary competencies to understand and provide mathematical proofs of their programs. Logic courses for CS tend to follow old precepts without emphasizing mastering deduction itself. In our institution, for several years we have followed a more pragmatical approach, in which the foundational aspects of both natural deduction and deduction a la Gentzen are taught and, in parallel, the operational premises of deduction are put into practice in proof assistants. Thus, CS students with a minimum knowledge in programming are challenged on providing correctness certificates for simple algorithms. “Putting their hands in the dough” they acquire a better understanding of the value and importance of deductive technologies in computing. Here we show how this is done relating natural deduction and sequent calculus deduction and using the proof assistant PVS in the simple context of a library of sorting algorithms.

Nominal rewriting generalises first-order rewriting by providing support for the specification of binding operators. In this paper, we give sufficient conditions for (local) confluence of closed nominal rewriting theories, based on the analysis of rule overlaps. More precisely, we show that closed nominal rewriting rules where all proper critical pairs are joinable are locally confluent. We also show how to refine the notion of rule overlap to derive confluence of the closed rewriting relation. The conditions that we define are easy to check using a nominal unification algorithm.

Orthogonality is a discipline of programming which syntactically guarantees determinism of functional specifications. Essentially, orthogonality avoids critical forks in term rewriting systems (TRSs) twofold: avoiding overlappings between left-hand sides of the rules (non-ambiguity) prohibiting rules in the definitions of functions that may apply simultaneously and forbidding repetitions of variables in the left-hand side of the rules (left-linearity) that may produce forks. In the theory of term rewriting systems, determinism is captured by the well-known property of confluence that is a consequence of orthogonality. This work describes a complete formalization in PVS of the theorem of confluence of orthogonal term rewriting systems. The formalization includes definitions and results on parallel reduction, in particular Rosen’s Parallel Moves Lemma. It is made available as a PVS theory orthogonality inside the directory TRS of the NASA Langley PVS Library. Like all of TRS, orthogonality is intended to stay close to textbook proofs. The present proof uses the Parallel Moves Lemma at dominating positions of a parallel context. In this manner, all parallel forks filling the holes of the context are joined and, as result, a term of joinability for the whole fork is constructed.

Nominal unification is an extension of first-order unification that takes into account the \(\alpha \)-equivalence relation generated by binding operators, following the nominal approach. We propose a sound and complete procedure for nominal unification with commutative operators, or nominal C-unification for short, which has been formalised in Coq. The procedure transforms nominal C-unification problems into simpler (finite families) of fixed point constraints, whose solutions can be generated by algebraic techniques on combinatorics of permutations.

This paper presents a formalization of the proof of the undecidability of the halting problem for a functional programming language. The computational model consists of a simple first-order functional language called PVS0 whose operational semantics is specified in the Prototype Verification System (PVS). The formalization is part of a termination analysis library in PVS that includes the specification and equivalence proofs of several notions of termination. The proof of the undecidability of the halting problem required classical constructions such as mappings between naturals and PVS0 programs and inputs. These constructs are used to disprove the existence of a PVS0 program that decides termination of other programs, which gives rise to a contradiction.

Computing evolutionary distances using gene order data is a complex combinatory problem; nevertheless, for specific metrics exact polynomial algorithms were proposed, having in many cases non trivial approaches. This scenario can become harder if we want to reconstruct phylogenies based on gene order data: first it is necessary to explore the search space of possible tree structures which is well-known to be exponential; second, it is necessary a method for evaluating the cost of these trees, i.e. to find a labeling of the internal nodes that leads to the most parsimonious cost of a tree under a given evolutionary distance. The latter problem was shown to be NP-hard even for 3 genomes (median problem) under many evolutionary distances. In this paper we propose a variable neighborhood search approach for solving the large phylogeny problem for data based on gene orders. Also, a greedy approach is proposed for the small phylogeny problem aiming to reduce the running time of the Kovac et al. dynamic programming approach. Our proposed algorithms were implemented as the software called HELPHY. Experiments showed that the running time is improved for finding trees with good scores (reversal distance) for the Campanulaceae dataset, and a new tree structure was found having the best known score (double cut and join distance) for the case of Hemiascomycetes dataset.

Rearrangement by reversals is a suitable global operation when treating genomes with a single chromosome. Sorting unsigned genomes by reversals is an NP-hard optimization problem. Several approximation algorithms were proposed, among them, in previous work, a competitive genetic algorithm and its standard parallel version, that provides a substantial speedup, were introduced. In this paper, two approaches using island models to parallelize such algorithm are presented. The first approach uses the unidirectional ring communication topology to exchange individuals between neighboring islands and, the second uses a complete graph scheme for the distribution of individuals among islands. Both approaches were proposed with the objective of improving precision (that is, for reducing the number of reversals) and decreasing the runtime regarding the sequential GA. Experiments were performed with randomly generated synthetic genomes and the results show that the parallel approach using the ring communication topology outperforms the previously proposed GA and its parallel version in terms of accuracy, providing solutions with less reversals and, that the parallel approach using the complete graph topology does not provide significant improvements. Both the new parallel GA approaches get competitive speedups regarding the speedup achieved by the standard parallel version of the genetic algorithm.

We present an algorithm to decide the intruder deduction problem (IDP) for a class of equational theories that include associative and commutative (AC) operators. The algorithm is based on the analysis of reductions in the head of terms built from normal contexts using the initial knowledge of the intruder. It relies on a new and efficient algorithm to solve a restricted case of higher-order AC-matching. For the subclass of theories for which AC operators have inverses, our algorithm runs in polynomial time on the size of a saturated set built from the initial knowledge of the intruder. To illustrate, we apply the results to Pure AC theories, Abelian Groups, Abelian Groups extended with exponentiation, and XOR. Although specific algorithms have already been defined to deal with each of these theories, we provide a modular approach that can deal with all of them in a uniform way.

We introduce GCIS, a grammar compression algorithm based on the induced suffix sorting algorithm SAIS, presented by Nong et al. in 2009. Our solution builds on the factorization performed by SAIS during suffix sorting. We construct a context-free grammar on the input string which can be further reduced into a shorter string by substituting each substring by its corresponding factor. The resulting grammar is encoded by exploring some redundancies, such as common prefixes between suffix rules, which are sorted according to SAIS framework. When compared to well-known compression tools such as Re-Pair and 7-zip under repetitive sequences, our algorithm is faster at compressing and achieves compression ratio close to that of Re-Pair, at the cost of being the slowest at decompressing.

In this chapter, we present a style of deduction known as Gentzen’s sequent calculus that is different from the one of natural deduction (both invented by Gerhard Gentzen) and has relevant computational interest and applications.

The propositional logic has several limitations for expressing ideas; mainly, it is not possible to quantify over sets of individuals and reason about them.

In this chapter, we present simple cases of study in order to illustrate the application of PVS for formalizing algebraic and algorithmic properties.

The deductive rules studied in the previous chapters have been implemented in several computational environments such as theorem provers and proof assistants.

The most elementary logical system of some practical interest is the propositional logic. In this system is it possible to express logical consequences, conjunction, disjunction, and negation of propositions.

This work presents formalizations of properties and algorithms for the first-order unification theory in the proof assistant PVS. In previous works a formalization of the theorem of existence of most general unifiers (mgu's) for first-order unifiable problems was presented and then, it was illustrated how the formalizations of correctness and completeness used for the proof of the theorem of existence, can be adapted in order to verify greedy unification algorithms 'a la Robinson. The distinguishing feature of these two formalizations is that they remain close to the textbook proofs which was possible through the use of the higher-order specification language and proof engine of PVS. That work consists of two elaborated PVS theories having been the one related with the theorem of existence of mgu's applied for obtaining a full formalization of the Knuth-Bendix(Huet) critical pair theorem. In addition to these two developments, this work describes a formalization of the correction and completeness of a more elaborated first-order unification algorithm. In contrast with the greedy algorithm, the current one is more efficient. It navigates in a post-order traversal the tree structure of the two terms being unified in such a way that after the difference at the first position of conflict (found in inner-most, left-most order) between the terms is eliminated through a linkage substitution (mapping a variable into a term), the search of the following position of conflict is computed through application of auxiliary functions starting from the previous position. Unlike this more efficient traversal, the greedy unification algorithm always restarts the search of conflicts from the root of the terms being unified. The new formalization gave rise to a more elaborated PVS development in which unlike a relatively straightforward application of correctness and completeness formalizations of the theorem of existence of mgu's, it was necessary the formalization of a series of structural auxiliary lemmas to deal with formalization of properties of the tree data structure used to represent terms.

Adaptation of mobile robot controllers commonly requires the computation of optimal points of operation. Specifically, for miniature mobile robots with serious computational limitations, that are typical of embedded systems, one of the main challenges is the adaptation of efficient computational methods in order to find solutions of complex optimization problems, which demand large execution times. This drawback compels the design of high-performance parallel optimization algorithms which must run over embedded system platforms. This paper describes how adequate hardware implementations of the Particle Swarm Optimization (PSO) algorithm can be useful for real time adaptation of mobile robot controllers. For achieving this, a new architecture is proposed, which is based on an FPGA implementation of the opposition-based learning (OBL) approach applied to the PSO (for short HPOPSO), and which explores the intrinsic parallelism of this algorithm in order to adjust the weights of a neural robot controller in real time according to desired behaviors. The proposed HPOPSO was applied to the learning-from-demonstration problem in which a teacher performs executions of the desired behavior. Effectiveness of the proposed architecture was demonstrated by numerical simulations and the feasibility of the adaptive behavior of the neural robot controller was confirmed for two obstacle avoidance case studies that were preserved when one or more failures on the distance sensors occur. The HPOPSO, which uses the OBL technique, improves the quality of the solutions in comparison with the standard PSO. Comparisons of the adaptation time between hardware and software approaches have demonstrated the suitability of the FPGA implementation of the proposed HPOPSO for attending specific requirements of embedded system applications.

The rearrangement of genomes is an important tool for studying the evolution of genomes and specifically for the construction of phylogenies. A translocation splits and combines the strings of genes of a pair of chromosomes inside a genome and is considered a suitable operation for rearrangement of genomes with multiple chromosomes. The translocation distance between two genomes is the minimum number of translocations necessary to convert one of them into the other. Computing the translocation distance between two unsigned genomes, that is the case in which the direction of the genes between the chromosomes is not considered, is known to be an MV-hard optimization problem. Among several approximation algorithms that were proposed for solving this problem, the authors introduced in a previous work a genetic algorithm approach improved with opposition based learning and memetic mechanisms. In this paper, two parallel treatments of the sequential memetic approach are introduced for solving the translocation distance problem for unsigned genomes. The first approach, computes in parallel the fitness over all individuals of a population. This method intends speeding-up the sequential memetic algorithm. The second approach, processes in parallel multiple populations and was proposed for improving precision providing solutions with a less number of translocations than the sequential memetic algorithm. Several experiments were performed with randomly generated synthetic and biologically based genomes. Results show that the parallel approaches outperform the sequential memetic algorithm.

Many scientific and engineering applications require to perform a large number of arithmetic operations that must be computed in an efficient manner using a high precision and a large dynamic range. Commonly, these applications are implemented on personal computers taking advantage of the floating-point arithmetic to perform the computations and high operational frequencies. However, most common software architectures execute the instructions in a sequential way due to the von Neumann model and, consequently, several delays are introduced in the data transfer between the program memory and the Arithmetic Logic Unit (ALU). There are several mobile applications which require to operate with a high performance in terms of accuracy of the computations and execution time as well as with low power consumption. Modern Field Programmable Gate Arrays (FPGAs) are a suitable solution for high performance embedded applications given the flexibility of their architectures and their parallel capabilities, which allows the implementation of complex algorithms and performance improvements. This paper describes a parameterizable floating-point library for arithmetic operators based on FPGAs. A general architecture was implemented for addition/subtraction and multiplication and two different architectures based on the Goldschmidt’s and the Newton-Raphson algorithms were implemented for division and square root. Additionally, a tradeoff analysis of the hardware implementation was performed, which enables the designer to choose, for general purpose applications, the suitable bit-width representation and error associated, as well as the area cost, elapsed time and power consumption for each arithmetic operator. Synthesis results have demonstrated the effectiveness of the implemented cores on commercial FPGAs and showed that the most critical parameter is the dedicated Digital Signal Processing (DSP) slices consumption. Simulation results were addressed to compute the mean square error (MSE) and maximum absolute error demonstrating the correctness of the implemented floating-point library and achieving and experimental error analysis. The Newton-Raphson algorithm achieves similar MSE results as the Goldschmidt’s algorithm, operating with similar frequencies; however, the first one saves more logic area and dedicated DSP blocks.

A theory, called trs, for Term Rewriting Systems in the theorem Prover PVS is described. This theory is built on the PVS libraries for finite sequences and sets and a previously developed PVS theory named ars for Abstract Reduction Systems which was built on the PVS libraries for sets. Theories for dealing with the structure of terms, for replacements and substitutions jointly with ars allow for adequate specifications of notions of term rewriting such as critical pairs and formalization of elaborated criteria from the theory of Term Rewriting Systems such as the Knuth-Bendix Critical Pair Theorem. On the other hand, ars specifies definitions and notions such as reduction, confluence and normal forms as well as non basic concepts such as Noetherianity.

It has long been argued that the notion of substitution in the λ-calculus needs to be made explicit. This resulted in many calculi have been developed in which the computational steps of the substitution operation involved in β-contractions have been atomised. In contrast to the great variety of developments for making explicit formalisations of the Beta rule, less work has been done for giving explicit definitions of the conditional Eta rule. In this paper constructive Eta rules are proposed for both the λσand the λse-calculi of explicit substitutions. Our results can be summarised as follows: 1) we introduce constructive and explicit definitions of the Eta rule in the λσand the λse-calculi, 2) we prove that these definitions are correct and preserve basic properties such as subject reduction. In particular, we show that the explicit definitions of the eta rules coincide with the Eta rule for pure λ-terms and that moreover, their application is decidable in the sense that Eta redices are effectively detected (and contracted). The formalisation of these Eta rules involves the development of specific calculi for explicitly checking the condition of the proposed Eta rules while constructing the Eta contractum.

Elevator systems are administrated by an elevator group control system (EGCS) and micro-processed sub-systems implementing a local control system (LCS) for each elevator. This paper describes the validation of five dispatching algorithms for elevator systems that were implemented on Spartan 3 FPGA-based boards in an integrated approach reducing the area and improving performance. The overall system is composed of several LCS, which implement the dispatching algorithms, an RS485-based network and a virtual environment called virtual elevator interface system (VEI), which includes a simulator/monitoring system and an EGCS-based on fuzzy logic (FEGCS). The FEGCS runs on a PC and, under different traffic situations, determines the best algorithm to be run in each LCS in order to reduce the user waiting time and the power consumption. The novelty of this approach is that the LCSs are capable to run different dispatching algorithms independently, that are suitable for specific passenger traffic situations, while the FEGCS only must determine the best algorithm to be run in each LCS. The VEI allows the designer to test and validate in a flexible way the algorithm performance for different traffic situations.

We compare two different styles of Higher-Order Unification (HOU): the classical HOU algorithm of Huet for the simply typed λ-calculus and HOU based on the λσ-calculus of explicit substitutions. For doing so, first, the original Huet algorithm for the simply typed λ-calculus with names is adapted to the language of the λ-calculus in de Bruijn's notation, since this is the notation used by the λσ-calculus. Afterwards, we introduce a new structural notation called unification tree, which eases the presentation of the subgoals generated by Huet's algorithm and its behaviour. The unification tree notation will be important for the comparison between Huet's algorithm and unification in the λσ-calculus whose derivations are presented into a structure called derivation tree. We prove that there exists an important structural correspondence between Huet's HOU and the λσ-HOU method: for each (sub-)problem in the unification tree there exists a counterpart in the derivation tree. This allows us to conclude that the λσ-HOU is a generalization of Huet's algorithm and that solutions computed by the latter are always computed by the former method.

A variant of the Ford-Johnson or merge insertion sorting algorithm that we called four Ford-Johnson ("4FJ, for short) is presented and proved to execute exactly the same number of comparisons than the Ford-Johnson algorithm. The main advantage of our algorithm is that, instead of recursively working over lists of size the half of the input, as the Ford-Johnson algorithm does, "4FJ recursively works over lists of size the quarter of the input. This allows for implementations of data structures for coordinating the recursive calls of size only 33% of the ones needed for the Ford-Johnson algorithm.

Biological Sequence Comparison is one of the most important operations in Computational Biology since it is used to determine how similar two sequences are. Smith and Waterman proposed an exact algorithm (SW), based on dynamic programming, that is able to obtain the best local alignment between two sequences in quadratic time and space. In order to compare long biological sequences, SW is rarely used since the computation time and the amount of memory required becomes prohibitive. For this reason, heuristic methods like BLAST are widely used. Although faster, these heuristic methods do not guarantee that the best result will be produced. In this paper, we propose an exact parallel variant of the SW algorithm that obtains the best local alignments in quadratic time and reduced space. The results obtained in two clusters (8-machine and 16-machine) for DNA sequences longer than 32 KBP (kilo base-pairs) were very close to linear and, in some cases, superlinear. For very long DNA sequences (1.6 MBP), we were able to reduce execution time from 12.25 hours to 1.54 hours, in our 8-machine cluster. As far as we know, this is the first time 1.6 MBP sequences are compared with an exact SW variant. In this case, 30240 best local alignments were obtained.

A standard genetic algorithm (\(\mathcal{G\!A}_{{ \mathrm{S}}}\)) for sorting unsigned genomes by translocations is improved in two different manners: firstly, a memetic algorithm (\(\mathcal{G\!A}_{{ \mathrm{M}}}\)) is provided, which embeds a new stage of local search, based on the concept of mutation applied in only one gene; secondly, an opposition-based learning (\(\mathcal{G\!A}_{{ \mathrm{OBL}}}\)) mechanism is provided that explores the concept of internal opposition applied to a chromosome. Both approaches include a convergence control mechanism of the population using the Shannon entropy. For the experiments, both biological and synthetic genomes were used. The results showed that \(\mathcal{G\!A}_{{ \mathrm{M}}}\)outperforms both \(\mathcal{G\!A}_{{ \mathrm{S}}}\)and \(\mathcal{G\!A}_{{ \mathrm{OBL}}}\)as confirmed through statistical tests.

Translocation is a useful operation on strings with challenging questions in combinatorics of permutations and interesting applications in analysis of sequences. A translocation operation essentially is the interchange of prefixes and suffixes among two substrings of a string. For the case of genomes represented as strings, symbols that represent genes and chromosomes are modeled as substrings of the genomes; thus, translocation is an operation that models the interaction between chromosomes inside a genome. The translocation distance between two genomes is defined as the minimum number of translocations to convert one genome into another and has been proved to be a meaningful manner of modeling the evolutive distance between organisms. The particular case of unsigned genomes, those in which the orientation of the genes are not considered, is particularly difficult, while the signed case, in which the orientation of genes is considered, has been proved to be polynomially decidable. This paper presents an innovative Genetic Algorithm (GA) approach to solve the unsigned translocation distance problem. A distinguishing feature of the proposed GA is that it uses as fitness function the translocation distance for randomly generated signed versions of the input (that is an unsigned genome). Experiments over randomly generated strings (synthetic genomes) showed that the proposed GA approach computes answers that are better than those computed by an L5+e-approximation algorithm, the latter also implemented as part of this work.

Many algebraic operations can be efficiently implemented as pipe networks in arrays of functional units such as systolic arrays that provide a large amount of parallelism. However, the applicability of classical systolic arrays is restricted to problems with strictly regular data dependencies yielding only arrays with uniform linear pipes. This limitation can be circumvented by using reconfigurable systolic arrays or reconfigurable data path arrays, where the node interconnections and operations can be redefined even at run time. In this context, several alternative reconfigurable systolic architectures can be explored and powerful tools are needed to model and evaluate them. Well-known rewriting-logic environments such as ELAN and Maude can be used to specify and simulate complex application-specific integrated systems. In this article we propose a methodology based on rewriting-logic which is adequate to quickly model and evaluate reconfigurable architectures (RA) in general and, in particular, reconfigurable systolic architectures. As an interesting case study we apply this rewriting-logic modeling methodology to the space-efficient treatment of the Fast-Fourier Transform (FFT). The FFT prototype conceived in this way, has been specified and validated in VHDL using the Quartus II system.