Equational problems are fundamental in computer science, frequently arising as subproblems across diverse domains, including program analysis and learning from examples and counterexamples. This article focuses on equational problems in languages with binding operators, formulating them within the nominal framework and referring to them as Nominal Equational Problems . We provide a comprehensive definition of solutions for nominal equational problems and introduce a set of simplification rules for computing these solutions within the nominal ground term algebra. We rigorously prove that the simplification rules are sound , solution-preserving and complete . Moreover, we establish that, under a specific strategy for rule application, the simplification process always terminates, thereby providing an effective algorithm for solving nominal equational problems. Finally, we demonstrate the practical relevance of our results by showcasing how nominal equational problems can serve as a framework for learning from examples and counterexamples. We also illustrate their applicability in addressing sufficient completeness problems, emphasising their utility in theoretical and practical contexts.

We look at the generalization problem modulo some equational theories. This problem is dual to the unification problem: given two input terms, we want to find a common term whose respective two instances are equivalent to the original terms modulo the theory. There exist algorithms for finding generalizations over various equational theories. We focus on modular construction of equational generalization algorithms for the union of signature-disjoint theories. Specifically, we consider the class of regular and collapse-free theories, showing how to combine existing generalization algorithms to produce specific solutions in these cases. Additionally, we identify a class of theories that admit a generalization algorithm based on the application of axioms to resolve the problem. To define this class, we rely on the notion of syntactic theories, a concept originally introduced to develop unification procedures similar to the one known for syntactic unification. We demonstrate that syntactic theories are also helpful in developing generalization procedures similar to those used for syntactic generalization.

Abstract Interest in anti-unification, the dual problem of unification, is rising due to various new applications. For example, anti-unification-based techniques have been used recently in software analysis and related areas such as clone detection and automatic program repair. While syntactic forms of anti-unification have found many interesting uses, some aspects of modern applications are more appropriately modeled by reasoning modulo an equational theory. Thus, extending existing anti-unification methods to deal with important equational theories is the natural step forward. This paper considers anti-unification modulo pure absorption theories, i.e., where some function symbols are associated with a special constant satisfying the axiom $$f(x,\varepsilon _{f}) \,\approx \, f(\varepsilon _{f},x) \,\approx \, \varepsilon _{f}$$ f ( x , ε f ) ≈ f ( ε f , x ) ≈ ε f . We provide a sound and complete rule-based algorithm for such theories. Furthermore, we show that anti-unification modulo absorption is infinitary. Despite this, our algorithm terminates and produces a finitary algorithmic representation of the minimal complete set of solutions.

This talk discusses current extensions on the theory algebra from the NASA/PVSlibrary on formal developments for the Prototype Verification System (PVS). It discusses the approach to formalizing theorems of the ring theory and how they are applied to infer properties of specific algebraic structures. As cases of study, we will present recent formalizations on the theories of Euclidean Domains and Quaternions. Moreover, we will show how a general verification of Euclid’s division algorithm can be specialized to verify this algorithm for specific Euclidean Domains, and how the abstract theory of Quaternions can be parameterized to deal with the structure of Hamilton’s Quaternions.

Abstract 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.

Abstract This work extends a rule-based specification of nominal C-unification formalised in Coq to include ‘protected variables’ that cannot be instantiated during the unification process. By introducing protected variables, we are able to reuse the C-unification simplification rules to solve nominal C-matching (as well as equality check) problems. From the algorithmic point of view, this extension is sufficient to obtain a generalised C-unification procedure; however, it cannot be formally checked by simple reuse of the original formalisation. This paper describes the additional effort necessary in order to adapt the specification of the inference rules and reuse previous formalisations. We also generalise a functional recursive nominal C-unification algorithm specified in PVS with protected variables, effectively adapting this algorithm to the tasks of nominal C-matching and nominal equality check. The PVS formalisation is applied to test the correctness of a Python manual implementation of the algorithm.

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.

We propose a new axiomatisation of the alpha-equivalence relation for nominal terms, based on a primitive notion of fixed-point constraint. We show that the standard freshness relation between atoms and terms can be derived from the more primitive notion of permutation fixed-point, and use this result to prove the correctness of the new $\alpha$-equivalence axiomatisation. This gives rise to a new notion of nominal unification, where solutions for unification problems are pairs of a fixed-point context and a substitution. Although it may seem less natural than the standard notion of nominal unifier based on freshness constraints, the notion of unifier based on fixed-point constraints behaves better when equational theories are considered: for example, nominal unification remains finitary in the presence of commutativity, whereas it becomes infinitary when unifiers are expressed using freshness contexts. We provide a definition of $\alpha$-equivalence modulo equational theories that take into account A, C and AC theories. Based on this notion of equivalence, we show that C-unification is finitary and we provide a sound and complete C-unification algorithm, as a first step towards the development of nominal unification modulo AC and other equational theories with permutative properties.

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.

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.

Sorting unsigned permutations by reversals is a difficult problem; indeed, it was proved to be [Formula: see text]-hard by Caprara ( 1997 ). Because of its high complexity, many approximation algorithms to compute the minimal reversal distance were proposed until reaching the nowadays best-known theoretical ratio of 1.375. In this article, two memetic algorithms to compute the reversal distance are proposed. The first one uses the technique of opposition-based learning leading to an opposition-based memetic algorithm; the second one improves the previous algorithm by applying the heuristic of two breakpoint elimination leading to a hybrid approach. Several experiments were performed with one-hundred randomly generated permutations, single benchmark permutations, and biological permutations. Results of the experiments showed that the proposed OBMA and Hybrid-OBMA algorithms achieve the best results for practical cases, that is, for permutations of length up to 120. Also, Hybrid-OBMA showed to improve the results of OBMA for permutations greater than or equal to 60. The applicability of our proposed algorithms was checked processing permutations based on biological data, in which case OBMA gave the best average results for all instances.

Sorting unsigned permutations by reversals is anNP-hard optimization problem with applications in computational molecular biology. Several approximation and metaheuristic algorithms were proposed, among them, in a previous work, a competitive genetic algorithm and its parallel version using island models were proposed. In this paper, focusing on improving accuracy, new island models are proposed by diversifying the distribution of genetic material between islands through static and dynamic communication topologies. In static topologies, communication between islands is predefined and maintained during the computation, while in dynamic topologies the communication is continuously modified. The proposed island models use parallelism in a global and a local level, in which respectively, the exchange of individuals between islands and the fitness computation occurs. Results from the experiments performed with randomly generated synthetic permutations show that parallel island models using both dynamic and static communication topologies outperform parallel approaches found in the literature in terms of run-time as well as accuracy.

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.

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.

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.

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.

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+ε-approximation algorithm, the latter also implemented as part of this work.

Sorting by reversals unsigned permutations is a problem exhaustively studied in the fields of combinatorics of permutations and bioinformatics with crucial applications in the analysis of evolutionary distance between organisms. This problem was shown to be NP-hard, which gave rise to the development of a series of approximation and heuristic algorithms. Among these approaches, evolutionary algorithms were also proposed, from which to the best of our knowledge a parallel version of the first proposed genetic algorithm computes the highest quality results. These solutions were not optimized for the case when the population reaches a degenerate state, that is when individuals of the population remain very similar, and the procedure still continues consuming computational resources, but without improving the individuals. In this paper, a memetic algorithm is proposed for sorting unsigned permutations by reversals, using the local search as a way to improve the fitness function image of the individuals. Also, the entropy of the population is controlled, such that, when a degenerate state is reached the population is restarted. Several experiments were performed using permutations generated from biological data as well as hundreds of randomly generated permutations of different size, from which some ones were chosen and used as benchmark permutations. Experiments have shown that the proposed memetic algorithm uses more adequately the computational resources and gives competitive results in comparison with the parallel genetic algorithm and outperforms the results of the standard genetic algorithm.

Confluence is a key property of rewriting calculi that guarantees uniqueness of normal-forms when they exist. Metaconfluence is even more general, and guarantees confluence on open/meta terms, i.e. terms with holes, called metavariables that can be filled up with other (open/meta) terms. The difficulty to deal with open terms comes from the fact that the structure of metaterms is only partially known, so that some reduction rules became blocked by the metavariables. In this work, we establish metaconfluence for a family of calculi with explicit substitutions (ES) that enjoy preservation of strong-normalization (PSN) and that act at a distance. For that, we first extend the notion of reduction on metaterms in such a way that explicit substitutions are never structurally moved, i.e. they also act at a distance on metaterms. The resulting reduction relations are still rewriting systems, i.e. they do not include equational axioms, thus providing for the first time an interesting family of lambda-calculi with explicit substitutions that enjoy both PSN and metaconfluence without requiring sophisticated notions of reduction modulo a set of equations.

Synthesis of musical instruments or human voice is a time consuming process which requires theoretical and experimental knowledge about the synthesis engine. Commonly, performers need to deal with synthesizer interfaces and a process of trial and error for creating musical sounds similar to a target sound. This drawback can be overcome by adjusting automatically the synthesizer parameters using optimization algorithms. In this paper a hybrid particle swarm optimization (PSO) algorithm is proposed to solve the frequency modulation (FM) matching synthesis problem. The proposed algorithm takes advantage of a shuffle process for exchanging information between particles and applies the selective passive congregation and the opposition-based learning approaches to preserve swarm diversity. Both approaches for injecting diversity are based on simple operators, preserving the easy implementation philosophy of the particle swarm optimization. The proposed hybrid particle swarm optimization algorithm was validated for a three-nested FM synthesizer, which represents a 6-dimensional multimodal optimization problem with strong epistasis. Simulation results revealed that the proposed algorithm presented promising results in terms of quality of solutions.

A mechanical proof of the Knuth–Bendix Critical Pair Theorem in the higher-order language of the theorem prover PVS is described. This well-known theorem states that a Term Rewriting System is locally confluent if and only if all its critical pairs are joinable. The formalization of this theorem follows Huet’s well-known structure of proof in which the restriction on strong normalization or Noetherian was dropped and the result presented as a lemma. In order to formalize the Knuth–Bendix Critical Pair Theorem we rely on previously developed PVS theories for abstract reduction systems, named ars, and term rewriting systems, named trs, which were built upon the PVS libraries for finite sequences and sets. On the one hand, the theory trs is composed of subtheories for dealing with the structure of terms, for replacements of subterms and substitutions and jointly with the theory ars it allows for adequate specifications of elaborate notions of term rewriting systems such as the one of critical pairs. On the other hand, ars specifies basic definitions and notions of abstract reduction systems such as reduction, termination, normal forms, and confluence as well as non basic concepts such as strong normalization.

High computational cost for solving large engineering optimization problems point out the design of parallel optimization algorithms. Population based optimization algorithms provide parallel capabilities that can be explored by their implementations done directly in hardware. This paper presents a hardware implementation of Particle Swarm Optimization algorithms using an efficient floating-point arithmetic which performs the computations with high precision. All the architectures are parameterizable by bit-width, allowing the designer to choose the suitable format according to the requirements of the optimization problem. Synthesis and simulation results demonstrate that the proposed architecture achieves satisfactory results obtaining a better performance in therms of elapsed time than conventional software implementations.

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.

FELIX is a new design space exploration tool and graphical integrated development environment (IDE) for the programming of coarse-grained reconfigurable architectures. Its main and novel advantage is the use of rewriting rules and logical strategies for the automated generation of alternative functionally equivalent implementations from a single mathematical specification. The user selection of the rewriting logic strategies to be applied determines the resulting implementations, making it possible to quickly generate, simulate and evaluate alternative implementations that are logically equivalent. The FELIX system includes an interface to the KressArray Xplorer for hardware design-space exploration. The current version of the tool is targeted for the pact extreme processing platform (XPP), with support for additional architectures planned in future versions.

No abstract available.

Suffix trees are the fundamental data structure of combinatorial pattern matching on words. Suffix trees have been used in order to give optimal solutions of a great variety of problems on static words, but for practical situations, such as in a text editor, where the incremental changes of the text make dynamic updating of the corresponding suffix trees necessary, this data structure alone has not been used with success. We prove that, for dynamic modifications of order O(1) of words of length n, any suffix tree updating algorithm requires O(n) worst-case running time, as for the full reconstruction of the suffix tree. Consequently, we argue that this data structure alone is not appropriate for the solution of combinatorial problems on words that change dynamically.