Nominal Equational Problems

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.

SSIF: Subsumption-based Sub-term Inference Framework to audit Gene Ontology

Motivation The Gene Ontology (GO) is the unifying biological vocabulary for codifying, managing and sharing biological knowledge. Quality issues in GO, if not addressed, can cause misleading results or missed biological discoveries. Manual identification of potential quality issues in GO is a challenging and arduous task, given its growing size. We introduce an automated auditing approach for suggesting potentially missing is-a relations, which may further reveal erroneous is-a relations. Results We developed a Subsumption-based Sub-term Inference Framework (SSIF) by leveraging a novel term-algebra on top of a sequence-based representation of GO concepts along with three conditional rules (monotonicity, intersection and sub-concept rules). Applying SSIF to the October 3, 2018 release of GO suggested 1938 unique potentially missing is-a relations. Domain experts evaluated a random sample of 210 potentially missing is-a relations. The results showed SSIF achieved a precision of 60.61, 60.49 and 46.03% for the monotonicity, intersection and sub-concept rules, respectively. Availability and implementation SSIF is implemented in Java. The source code is available at https://github.com/rashmie/SSIF. Supplementary information Supplementary data are available at Bioinformatics online.

The Arab Gift

This chapter focuses on the Arabs' contributions to the modern number system. It first considers the role played by Abu Jafar Muhammad ibn Musa al-Khwārizmī, the greatest Arab mathematician of his day, learned of the new Indian numbers from the Arabic translation of Brahmagupta's Brahmasphutasiddhanta, and wrote a textbook on arithmetic using the new Indian numbers. In around 820 AD, al-Khwārizmī wrote The Book of Restoration and Equalization. It was translated into Latin under the title Algebra et Almucabala, and that is how the term “algebra” came to be understood as what it is today. The chapter also looks at the Indian astronomer Kanka, who visited the House of Wisdom in Baghdad in 770 AD and brought with him many manuscripts from India, including the Brahmasphutasiddhanta.

Program Algebra over an Algebra

Summary We introduce an algebra with free variables, an algebra with undefined values, a program algebra over a term algebra, an algebra with integers, and an algebra with arrays. Program algebra is defined as universal algebra with assignments. Programs depend on the set of generators with supporting variables and supporting terms which determine the value of free variables in the next state. The execution of a program is changing state according to successor function using supporting terms.

Foundation for Model Integration: Semantic Backplane

One of the primary goals of the Adaptive Vehicle Make (AVM) program of DARPA is the construction of a model-based design flow and tool chain, META, that will provide significant productivity increase in the development of complex cyber-physical systems. In model-based design, modeling languages and their underlying semantics play fundamental role in achieving compositionality. A significant challenge in the META design flow is the heterogeneity of the design space. This challenge is compounded by the need for rapidly evolving the design flow and the suite of modeling languages supporting it. Heterogeneity of models and modeling languages is addressed by the development of a model integration language – CyPhy – supporting constructs needed for modeling the interactions among different modeling domains. CyPhy targets simplicity: only those abstractions are imported from the individual modeling domains to CyPhy that are required for expressing relationships across sub-domains. This “semantic interface” between CyPhy and the modeling domains is formally defined, evolved as needed and verified for essential properties (such as well-formedness and invariance). Due to the need for rapid evolvability, defining semantics for CyPhy is not a “one-shot” activity; updates, revisions and extensions are ongoing and their correctness has significant implications on the overall consistency of the META tool chain. The focus of this paper is the methods and tools used for this purpose: the META Semantic Backplane. The Semantic Backplane is based on a mathematical framework provided by term algebra and logics, incorporates a tool suite for specifying, validating and using formal structural and behavioral semantics of modeling languages, and includes a library of metamodels and specifications of model transformations.

A CORRESPONDENCE BETWEEN BALANCED VARIETIES AND INVERSE MONOIDS

There is a well-known correspondence between varieties of algebras and fully invariant congruences on the appropriate term algebra. A special class of varieties are those which are balanced, meaning they can be described by equations in which the same variables appear on each side. In this paper, we prove that the above correspondence, restricted to balanced varieties, leads to a correspondence between balanced varieties and inverse monoids. In the case of unary algebras, we recover the theorem of Meakin and Sapir that establishes a bijection between congruences on the free monoid with n generators and wide, positively self-conjugate inverse submonoids of the polycyclic monoid on n generators. In the case of varieties generated by linear equations, meaning those equations where each variable occurs exactly once on each side, we can replace the clause monoid above by the linear clause monoid. In the case of algebras with a single operation of arity n, we prove that the linear clause monoid is isomorphic to the inverse monoid of right ideal isomorphisms between the finitely generated essential right ideals of the free monoid on n letters, a monoid previously studied by Birget in the course of work on the Thompson group V and its analogues. We show that Dehornoy's geometry monoid of a balanced variety is a special kind of inverse submonoid of ours. Finally, we construct groups from the inverse monoids associated with a balanced variety and examine some conditions under which they still reflect the structure of the underlying variety. Both free groups and Thompson's groups Vn,1 arise in this way.

EQUATIONAL THEORIES GENERATED BY HYPERSUBSTITUTIONS OF TYPE (n)

Hypersubstitutions map n-ary operation symbols to n-ary terms. Such mappings can be uniquely extended to mappings defined on the set of all terms. It turns out that the kernels of hypersubstitutions are fully invariant congruence relations on the (absolutely free) term algebra of the considered type. For an arbitrary type τ = (n), n ≥ 1, i.e. if one has only one n-ary operation symbol, we will describe all these congruence relations. The results will be applied to solve the hyperunification problem. Further we will give some generalizations to arbitrary types.