Search

Recently, a number of reversible functional programming languages have been proposed. Common to several of these is the assumption of totality, a property that is not necessarily desirable, and certainly not required in order to guarantee reversibility. In a categorical setting, however, faithfully capturing partiality requires handling it as additional structure. Recently, Giles studied inverse categories as a model of partial reversible (functional) programming. In this paper, we show how additionally assuming the existence of countable joins on such inverse categories leads to a number of properties that are desirable when modelling reversible functional programming, notably morphism schemes for reversible recursion, a \(\dagger \)-trace, and algebraic \(\omega \)-compactness. This gives a categorical account of reversible recursion, and, for the latter, provides an answer to the problem posed by Giles regarding the formulation of recursive data types at the inverse category level.

Now that net theory had proved to be ready for widespread use, it no longer required Petri’s personal intervention. He could thus dedicate himself to the further development of the foundations. Ultimately, what he strived at, was a general axiomatization of concurrency and the theory of distributed systems, based on the concepts distributedness and independence. In his 1978 paper Concurrency as a Basis of System Thinking [16], he states that a central theme in this program is the systematic permeation of a sequence of conceptual levels and their interrelations (see Fig. 7.1).

Many variations of the notion of regions in transition systems, introduced by Ehrenfeucht and Rozenberg in the context of Elementary Net Systems, were proposed later in order to synthesize other classes of net systems and to establish corresponding representation theorems for initialized transition systems. Many striking similarities appear in the technical developments of those similar studies. The goal of this chapter is to provide a uniform theory of net system synthesis based on regions, such that all the considered variations may be retrieved as specific instantiations of this general scheme. In the uniform theory, each class of nets comes equipped with a deterministic transition system t, called a type of nets, which induces a net firing rule and hence captures the dynamic evolution of all nets in the class. The type of nets describes the behaviour of an archetypical (atomic) net of the considered class. We can then use the type of nets as a parameter to define the notions of t-nets (and t-net systems) and their marking (and reachability) graphs. The t-regions of an initialized transition system A are the morphisms from A into t; they define the places of the t-net synthesized from A. In the last section of the chapter, we pay specific attention to the types of Boolean nets, where markings are sets of places.

We introduce a new approach in black box group theory which deals with black box group problems in the category of black boxes and their morphisms. This enables us to enrich black box groups by actions of outer automorphisms such as Frobenius maps or graph automorphisms of simple groups of Lie type. As an application of this new technique, we present a number of new results, including a solution of an old problem about constructing unipotent elements in groups of Lie type of odd characteristic.

We present a Petri net model of a protocol for the distributed generation of id-based private keys. Those keys can then be used for secure communications. The components of the system are built as refinements of a common interface, by applying a formal operation based on a class of morphisms between Elementary Net Systems. It is then shown that we can derive behavioural properties of the composed system without building it explicitly, by exploiting properties of the given morphisms.

We characterize the infinite words determined by indexed languages. An infinite language L determines an infinite word α if every string in L is a prefix of α. If L is regular or context-free, it is known that α must be ultimately periodic. We show that if L is an indexed language, then α is a morphic word, i.e., α can be generated by iterating a morphism under a coding. Since the other direction, that every morphic word is determined by some indexed language, also holds, this implies that the infinite words determined by indexed languages are exactly the morphic words. To obtain this result, we prove a new pumping lemma for the indexed languages, which may be of independent interest.

Representation formats based on theory graphs have been successful in formalized mathematics as they provide valuable logic-compatible modularity and foster reuse. Theories - sets of symbols and axioms – serve as modules and theory morphisms - truth-preserving mappings from the (language of the) source theory to the target theory – formalize inheritance and applicability of theorems. The MMT [4] system re-developed the formal part of the OMDoc theory graph into a foundation-independent meta-system for formal mathematics and implemented it in the MMT API.

Properties of a \(k\)-vector space \(\mathrm {Hom}_{k}(U_{0}, V_{0})\) of linear maps between fixed \(k\)-vector spaces \(U_{0}\) and \(V_{0}\) are used to define perfect black visual cryptography schemes for sharing secret images, such images can be revealed by stacking qualified sets of transparencies induced by a linear combination of some basic \(k\)-linear maps. The use of this type of morphisms allows to generalize some of the schemes used up to date for sharing multiple secrets.

Pseudo-repetitions are a natural generalization of the classical notion of repetitions in sequences: they are the repeated concatenation of a word and its encoding under a certain morphism or antimorphism. We approach the problem of deciding whether there exists an anti-/morphism for which a word is a pseudo-repetition. In other words, we try to discover whether a word has a hidden repetitive structure. We show that some variants of this problem are efficiently solvable, while some others are NP-complete.

Next we will be considering repetitions of items in the input sequential data, and as a consequence, the final closed partial orders are not necessarily injective. As we will see, dealing with general partial orders makes the proper formalization with category theory a bit more difficult. To start with, we are forced to drop the injectivity of the morphisms in the general category of graphs, and this allows for many different ways of mapping a partial order over a sequence. Still another inconvenience, Theorem 5.1 of chapter 5 just holds for one of the directions in this new problem. Indeed, the maximal paths of the final closed partial orders do not necessarily coincide exactly with the intersections of the compatible input sequential data. Here we will try to formally justify the construction of our final closed partial orders for a set of data as the colimit transformation on path-preserving edges. Colimits will naturally generalize also the coproduct transformation of chapter 5, but as we shall see, proving that our final structure has the property of being maximally specific is still an unsolved combinatorial problem.

We say that an infinite word w is weakly abelian periodic if it can be factorized into finite words with the same frequencies of letters. In this paper we study properties of weak abelian periodicity, and its relations with balance and frequency. We establish necessary and sufficient conditions for weak abelian periodicity of fixed points of uniform binary morphisms. Also, we discuss weak abelian periodicity in minimal subshifts.

This paper describes a generalization of the usual category in which coalgebras are considered, and its application to modelling quantum systems and their physical symmetries. Following the programme of work initiated in [1], [2], we aim to model systems described by the laws of quantum physics using coalgebraic techniques. A broader notion of the morphisms of coalgebras is given, in which diagrams are allowed to commute only up to appropriate natural isomorphism. This relaxed setting is then shown to have analogues of coalgebraic notions such as bisimulations, with properties that parallel the usual coalgebraic ones closely. This new setting is then exploited to give coalgebraic models of quantum systems in which the conceptually important physical symmetries are given as automorphisms of a suitable coalgebra.

A non-erasing morphism is weakly unambiguous with respect to a pattern if no other non-erasing morphism maps the pattern to the same image. If the size of the target alphabet is at least three, then the patterns for which there exists a length-increasing weakly unambiguous morphism can be characterized using the concept of loyal neighbors of variables. In this article this characterization is generalized for patterns with constants. Two different generalizations are given for sets of patterns.

Let A be a finite alphabet and f : A *i¾?A * a morphism with an iterative fixed point f ω α, where α∈A. Consider the subshift ${\mathcal X}, T$ , where ${\mathcal X}$ is the shift orbit closure of f ω α and $T\colon{\mathcal X} \rightarrow{\mathcal X}$ is the shift operation. Let S be a finite alphabet that is in bijective correspondence via a mapping c with the set of nonempty suffixes of the images fa for a∈A. Let ${\mathcal S}\subset S^{\mathbb N}$ be the set of infinite words s=s n ni¾?0 such that $\pi{\rm s} := cs_{0}f{cs_{1}}f^{2}{cs_{2}}\cdots \in{\mathcal X}$ . We show that if f is primitive and fA is a suffix code, then there exists a mapping $H : {\mathcal S} \rightarrow{\mathcal S}$ such that ${\mathcal S}, H$ is a topological dynamical system and $\pi :{\mathcal S}, H \rightarrow {\mathcal X}, T$ is a conjugacy. We call ${\mathcal S}, H$ the suffix conjugate of i¾?, T. Furthermore, in the special case when f is the Fibonacci or the Thue-Morse morphism, we show that ${\mathcal S}, T$ is a sofic shift, that is, the language of ${\mathcal S}$ is regular.

Given an infinite word \(\ensuremath{\mathbf{x}} \) over an alphabet A, a letter b occurring in \(\ensuremath{\mathbf{x}} \), and a total order σ on A, we call the smallest word with respect to σ starting with b in the shift orbit closure \(\ensuremath{\mathcal{S}} _{\ensuremath{\mathbf{x}} }\) of \(\ensuremath{\mathbf{x}} \) an extremal word of \(\ensuremath{\mathbf{x}} \). In this paper we consider the extremal words of morphic words. If \(\ensuremath{\mathbf{x}} = g(f^{\omega}(a))\) for some morphisms f and g, we give a simple condition on f and g that guarantees that all extremal words are morphic. An application of this condition shows that all extremal words of binary pure morphic words are morphic. Our technique also yields easy characterizations of extremal words of the Period-doubling and Chacon words and a new proof of the form of the lexicographically least word in the shift orbit closure of the Rudin-Shapiro word.

The Dual Post Correspondence Problem asks, for a given word α, if there exists a non-periodic morphism g and an arbitrary morphism h such that gα=hα. Thus α satisfies the Dual PCP if and only if it belongs to a non-trivial equality set. Words which do not satisfy the Dual PCP are called periodicity forcing, and are important to the study of word equations, equality sets and ambiguity of morphisms. In this paper, a 'prime' subset of periodicity forcing words is presented. It is shown that when combined with a particular type of morphism it generates exactly the full set of periodicity forcing words. Furthermore, it is shown that there exist examples of periodicity forcing words which contain any given factor/prefix/suffix. Finally, an alternative class of mechanisms for generating periodicity forcing words is developed, resulting in a class of examples which contrast those known already.

In the design of concurrent and distributed systems, modularity and refinement are basic conceptual tools. We propose a notion of refinement/abstraction of local states for a basic class of Petri Nets, associated with a class of morphisms. The morphisms, from a refined system to an abstract one, associate suitable subnets to abstract local states. We define an operation of composition ruled by morphisms of that class. The main results concern behavioural properties preserved and reflected by the morphisms. In particular, we focus on the conditions under which reachable markings are preserved or reflected, and the conditions under which a morphism induces a weak bisimulation between net systems.

Weighted automata model quantitative aspects of systems like the consumption of resources during executions. Traditionally, the weights are assumed to form the algebraic structure of a semiring, but recently also other weight computations like average have been considered. Here, we investigate quantitative context-free languages over very general weight structures incorporating all semirings, average computations, lattices. In our main result, we derive the Chomsky-Schutzenberger Theorem for such quantitative context-free languages, showing that each arises as the image of the intersection of a Dyck language and a recognizable language under a suitable morphism. Moreover, we show that quantitative context-free languages are expressively equivalent to a model of weighted pushdown automata. This generalizes results previously known only for semirings.

The subword complexity of an infinite word counts the number of subwords of a given length, while the abelian complexity counts this number up to letter permutation. Although a lot of research has been done on the subword complexity of morphic words, i.e., words obtained as fixed points of iterated morphisms, little is known on their abelian complexity. In this paper, we undertake the classification of the asymptotic growths of the abelian complexities of fixed points of binary morphisms. Some general results we obtain stem from the concept of factorization of morphisms. We give an algorithm that yields all canonical factorizations of a given morphism, describe how to use it to check quickly whether a binary morphism is Sturmian, discuss how to fully factorize the Parry morphisms, and finally derive a complete classification of the abelian complexities of fixed points of uniform binary morphisms.

Any fuzzy set X in a classical set A with values in a complete (residuated) lattice Ω can be identified with a system of o-cuts Xo, o∈Ω. Analogical results were proved for sets with similarity relations with values in Ω (e.g. Ω-sets) which are objects of two special categories K=Set(Ω) or SetR(Ω) of Ω-sets and for fuzzy sets defined as morphisms from Ω-set into a special Ω-set (Ω,↔). These fuzzy sets can be defined equivalently as special cut systems (Co)o, called f-cuts. That equivalence then represents a natural isomorphism between covariant functor of fuzzy sets ${\cal F}_{\bf K}$ and covariant functor of f-cuts ${\cal C}_{\bf K}$. In the paper we are interested in relationships between sets of fuzzy sets and sets of f-cuts in an Ω-set (A,δ) in corresponding categories Set(Ω) and SetR(Ω), which are endowed with binary operations extended either from binary operations in the lattice Ω, or from binary operations defined in a set A by the generalized Zadeh's extension principle. We prove that the final binary structures are (under some conditions) isomorphic.

Stepan Holub (Discr. Math., 2009) gave the first polynomial algorithm deciding whether a given word is a nontrivial fixed point of a morphism. His algorithm works in quadratic time for large alphabets. We improve the algorithm to work in linear time. Our improvement starts with a careful choice of a subset of rules used in Holub’s algorithm that is necessary to grant correctness of the algorithm.Afterwards we show how to choose the order of applying the rules that allows to avoid unnecessary operations on sets. We obtain linear time using efficient data structures for implementation of the rules. Holub’s algorithm maintains connected components of a graph corresponding to specially marked positions in a word. This graph is of quadratic size for large alphabet. In our algorithm only a linear number of edges of this conceptual graph is processed.

In previous sections we have seen how the nilpotent elements of \(\boldsymbol{\mathcal{G}}_{\mbox{ $\Gamma $}}\), given by the values of morphisms d ± [see (5.26) and (5.35)], give rise to very rich algebraic and geometric structures on J(X; L, d) (to be more precise on the relative tangent sheaf \(\mathcal{T}_{\pi }\)).

The Dual Post Correspondence Problem asks whether, for a given word α, there exists a pair of distinct morphisms σ,τ, one of which needs to be non-periodic, such that σ(α) = τ(α) is satisfied. This problem is important for the research on equality sets, which are a vital concept in the theory of computation, as it helps to identify words that are in trivial equality sets only. Little is known about the Dual PCP for words α over larger than binary alphabets, especially for so-called ratio-primitive examples. In the present paper, we address this question in a way that simplifies the usual method, which means that we can reduce the intricacy of the word equations involved in dealing with the Dual PCP. Our approach yields large sets of words for which there exists a solution to the Dual PCP as well as examples of words over arbitrary alphabets for which such a solution does not exist.

Diatonic Modes can be modeled through automorphisms of the free group F 2 stemming from special Sturmian morphisms. Following [1] and [2] we associate special Sturmian morphisms f with linear maps E(f) on a vector space of lattice paths. According to [2] the adjoint linear map E(f) ∗ is closely related to the linear map E(f ∗ ), where f and f ∗ are mutually related under Sturmian involution. The comparison of these maps is music-theoretically interesting, when an entire family of conjugates is considered. If one applies the linear maps E(f 1), ..., E(f 6) (for the six authentic modes) to a fixed path of length 2, one obtains six lattice paths, describing a family of authentic common finalis modes (tropes). The images of a certain path of length 2 under the application of the adjoint maps E(f 1) ∗ , ..., E(f 6) ∗ properly matches the desired folding patterns as a family, which, on the meta-level, forms the folding of Guido’s hexachord. And dually, if one applies the linear maps \(E(f_1^\ast), ..., E(f_6^\ast)\) (for the foldings of the six authentic modes) to a fixed path of length 2, one obtains six lattice paths, describing a family of authentic common origin modes (“white note” modes). The images of a certain path of length 2 under the application of the adjoint maps \(E(f_1^\ast)^\ast, ..., E(f_6^\ast)^\ast\) properly match the desired step interval patterns as a family, which, on the meta-level, forms the step interval pattern of Guido’s hexachord. This result conforms to Zarlino’s re-ordering of Glarean’s dodecachordon.

In this section we use the morphism d + defined in (5.26) for geometric purposes. Throughout this section we fix an admissible component \(\Gamma \) in C r (L, d) and assume that it is not quasi-abelian (see Definition 4.20).

Infinite words can be fixed points of morphisms, and if the morphism is primitive, then such a word determines a unique dynamical system: the set of infinite words which have the property that each finite subword occurs in the fixed point word. The map on the dynamical system is the shift. Two dynamical systems are isomorphic if there exists a bi-continuous bijection between them which preserves the dynamics. We call two primitive morphisms dynamically equivalent if their dynamical systems are isomorphic. The task is to decide when two morphisms are dynamically equivalent. A morphism is called uniform if all the images of the letters have the same length. A first result is that the number of morphisms of morphisms with the same length dynamically equivalent to a given uniform morphism is finite, if the morphisms are one-to-one and if we ignore changes of alphabet. We will present the equivalence class of the Toeplitz morphism 0i¾?01, 1i¾?00. This is joint work with Ethan Coven and Mike Keane.

There are several different approaches to the theory of data types. At the simplest level, polynomials and containers give a theory of data types as free standing entities. At a second level of complexity, dependent polynomials and indexed containers handle more sophisticated data types in which the data have an associated indices which can be used to store important computational information. The crucial and salient feature of dependent polynomials and indexed containers is that the index types are defined in advance of the data. At the most sophisticated level, induction-recursion allows us to define data and indices simultaneously.

The preceding sections show that the Lie theoretic aspects of the Jacobian J(X; L, d) provide new methods and insights in the study of geometry of surfaces. Starting from this section we change the logic of our investigations—we make use of the sheaves of Lie algebras \(\boldsymbol{\mathcal{G}}_{\Gamma }\), for admissible components \(\Gamma \in {C}^{r}(L,d)\), to construct various objects (sheaves, complexes of sheaves, constructible functions), either on J(X; L, d) or on the Hilbert scheme X [d], which can serve as new invariants for vector bundles on X as well as for X itself. Our basic tool for this will be the morphisms d ± encountered in §5.1, (5.26), (5.35).

The morphism d + (resp. d −) considered in §5, (5.26) [resp. (5.35)], attaches intrinsically the nilpotent endomorphism d +(v) (resp. d −(v)) to every tangent vector v in T π.

Here we give an automated proof of the fact that a cubic curve admits at most one group law. This is achieved by proving the tight connection between the chord-tangent law of composition and any potential group law (as a morphism) on the curve. An automated proof of this is accomplished by implementing the rigidity lemma and the Cayley-Bacharach theorem of algebraic geometry as formal inference rules in Prover9, a first-order theorem prover developed by Dr. William McCune.

In this chapter we discuss Poisson–Lie groups and their infinitesimal counterparts Lie bialgebras. A Poisson–Lie group is a Lie group G which is equipped with a Poisson structure π, having the property that the product map on G is a morphism of Poisson manifolds. A Lie bialgebra is a Lie algebra which is at the same time a Lie coalgebra, the algebra and coalgebra structures satisfying some compatibility relation. We show that there is a functor which associates to every Poisson–Lie group a Lie bialgebra and that every finite-dimensional Lie bialgebra is the Lie bialgebra of some Poisson–Lie group, which can be chosen to be connected and simply connected. Using dressing actions, we shortly discuss the symplectic leaves of Poisson–Lie groups.

In the two preceding sections we considered sl 2 -triples of \(\boldsymbol{\mathcal{G}}_{\Gamma }\) arising from nilpotent elements d +(v), for v being tangent vectors in the relative tangent sheaf \(\mathcal{T}_{\pi }\) and d + is the morphism defined in (5.26).

This chapter contains such important concepts as sheaves of modules and algebras on schemes, quasi coherence and coherence for these sheaves, Spec of a sheaf of algebras on a scheme, reduced structure and the generalization of the field of functions from the classical theory to the algebra of fractions for a scheme. Also treated here are irreducible components of Noetherian schemes, embeddings, the graph and the diagonal in the category of schemes, and finally, separated morphisms and separated schemes.

Brouwer, Heyting, and Kolmogorov have proposed to define constructive proofs as algorithms, for instance, a proof of A ⇒B as an algorithm taking proofs of A as input and returning proofs of B as output. Curry, De Bruijn, and Howard have developed this idea further. First, they have proposed to express these algorithms in the lambda-calculus, writing for instance λfA ⇒A ⇒BλxA (f x x) for the proof of the proposition (A ⇒A ⇒B) ⇒A ⇒B taking a proof f of A ⇒A ⇒B and a proof x of A as input and returning the proof of B obtained by applying f to x twice. Then, they have remarked that, as proofs of A ⇒B map proofs of A to proofs of B, their type $\mbox{\em proof}(A \Rightarrow B)$ is $\mbox{\em proof}(A) \rightarrow \mbox{\em proof}(B)$. Thus the function proof mapping propositions to the type of their proofs is a morphism transforming the operation ⇒ into the operation →. In the same way, this morphism transforms cut-reduction in proofs into beta-reduction in lambda-terms.

We let \(\tilde{S{m}}_{k}\)denote the category of smooth k-schemes and whose morphisms are the smooth morphisms. We start with the following standard definition.

Meta-modeling has become the key technology to define domain-specific modeling languages for model-driven engineering. However, these modeling languages can change quite frequently which requires the evolution of their meta-models as well as the co-evolution (or migration) of their models. In this paper, we present an approach towards meta-model model co-evolution based on graph transformation concepts that targets to consider this challenge in a formal setting. Models are specified as graphs while model relations, especially type-instance relations, are defined by graph morphisms specifying type conformance of models to their meta-models. We present a basic approach to automatic deduction of model migrations from meta-model evolution steps which are specified by single transformation rules. Throughout that migration process, type conformance is ensured permanently. A first implementation is given using existing technology, namely the Eclipse Modeling Framework (EMF) and the EMF model transformation tool Henshin which is based on graph transformation concepts. Our evolution approach is presented at two small evolution scenarios for Petri nets and state machines.

In the following subsections, we introduce the mathematical formalisms that underpin modelling, metamodelling and ontologies. Basic to a mathematical formalism are set theory and morphisms. First we consider, in Sect. 2.1, how set theory can represent modelling concepts. In Sect. 2.2, we look at mappings (functions) between pairs of sets–whether such a mapping is one-to-one, onto or both can be critical in understanding many of the ‘problems’ identified in the software engineering modelling literature

In this first chapter of Part 2 we give a general, rapid introduction to the required language from category theory.

This chapter gives more of the important properties of morphisms, and explains scheme theoretic images, finiteness conditions and the “Sorite”.

This paper introduces an abstract notion of fragments of monadic second-order logic. This concept is based on purely syntactic closure properties. We show that over finite words, every logical fragment defines a lattice of languages with certain closure properties. Among these closure properties are residuals and inverse $\mathcal C$-morphisms. Here, depending on certain closure properties of the fragment, $\mathcal C$ is the family of arbitrary, non-erasing, length-preserving, length-multiplying, or lengthreducing morphisms. In particular, definability in a certain fragment can often be characterized in terms of the syntactic morphism. This work extends a result of Straubing in which he investigated certain restrictions of first-order formulae. As motivating examples, we present (1) a fragment which captures the stutter-invariant part of piecewise-testable languages and (2) an acyclic fragment of Σ2. As it turns out, the latter has the same expressive power as two-variable first-order logic FO2.

In graph transformation, a match just represents an occurrences of a rule's left-hand side in the host graph. This is expressed by a morphism preserving the graph structure. However, there are situations where occurrences are bound by additional constraints. These can either be implicit, such as the gluing conditions of the DPO, or explicit such as negative application conditions. In this paper we study another type of implicit condition based on the reflection of structure. Morphisms reflecting some of the structures of their targets are abstractly characterised as open maps in the sense of Joyal, Nielsen, and Winskel. We show that under certain restrictions on the rules, DPOs preserve open maps. We establish an encoding of open maps into negative application conditions and study concurrency properties of the new approach.

We study pattern avoidance in the context of partial words. The problem of classifying the avoidable unary patterns has been solved, so we move on to binary, ternary, and more general patterns. Our results, which are based on morphisms (iterated or not), determine all the ternary patterns’ avoidability indices or at least give bounds for them.

The categorical framework of $\mathcal M$-adhesive transformation systems does not cover graph transformation with relabelling. Rules that relabel nodes are natural for computing with graphs, however, and are commonly used in graph transformation languages. In this paper, we generalise $\mathcal M$-adhesive transformation systems to $\mathcal M,\mathcal N$-adhesive transformation systems, where $\mathcal N$ is a class of morphisms containing the vertical morphisms in double-pushouts. We show that the category of partially labelled graphs is $\mathcal M,\mathcal N$-adhesive, where $\mathcal M$ and $\mathcal N$ are the classes of injective and injective, undefinedness-preserving graph morphisms, respectively. We obtain the Local Church-Rosser Theorem and the Parallelism Theorem for graph transformation with relabelling and application conditions as instances of results which we prove at the abstract level of $\mathcal M,\mathcal N$-adhesive systems.

The chapter starts by treating affine and projective morphisms, then proceeds to proper morphisms. The important valuational criteria for separated and for proper are then given. Very ample sheaves and the Segre embedding are treated, in the context of tensor products of graded Open image in new window -modules.

It has been shown [6] that, within the McAlister inverse monoid [10], whose elements can be seen as overlapping one-dimensional tiles, the class of languages recognizable by finite monoids collapses compared with the class of languages definable in Monadic Second Order Logic (MSO). This paper aims at capturing the expressive power of the MSO definability of languages of tiles by means of a weakening of the notion of algebraic recognizability which we shall refer to as quasi-recognizability. For that purpose, since the collapse of algebraic recognizability is intrinsically linked with the notion of monoid morphism itself, we propose instead to use premorphisms, monotonic mappings on ordered monoids that are only required to be sub-multiplicative with respect to the monoid product, i.e. mapping φ so that for all x and y, φ(xy)≤φ(x) φ(y). In doing so, we indeed obtain, with additional but relatively natural closure conditions, the expected quasi-algebraic characterization of MSO definable languages of positive tiles. This result is achieved via the axiomatic definition of an original class of well-behaved ordered monoid so that quasi-recognizability implies MSO definability. An original embedding of any (finite) monoid S into a (finite) well-behaved ordered monoid ${\mathcal Q}(S)$ is then used to prove the converse.