Search

This article contains a descriptive survey on the acceptability of equivalence-based translation of the menu of TECNO Android phones into the Yorùbá language, one of the three major languages in Nigeria. Words translated into Yorùbá were categorized into strategies of borrowing, semantic extension and composition and analysed from equivalence effect. In the follow-up survey, information and communication technology experts and general mobile phone users were carefully chosen and consulted for an assessment of the appropriateness of the translation. The study concluded that equivalence, the key term of linguistic translation theories, is still a viable concept in the translation of information and communication technology and equivalence-based translation into Yorùbá will not only promote the language but also contribute to effective communication in a multilingual global village that the world is fast becoming.

The thesis abstract, as a genre has a set of communicative functions mutually-understood by established members of the academic community. A vast majority of translation studies of source language (SL) and target language (TL) equivalence seems to have overlooked the inherent relationship between form and function when translating. The purpose of this study was to find out whether the Arab students would translate the English passive structures into their corresponding Arabic passive in order to maintain the pragma-generic functions associated with these constructions or would employ other translation replacements when translating English passives into Arabic. A further purpose was to find out what grammatical factors constrain the choice of these translation options. To fulfill these purposes, we investigated the voice choice in 90 MA thesis abstracts and their 90 Arabic translated versions written in English by the same MA students, drawn from the field of Linguistics. The data analysis revealed that when the Arab student-translators come across the English passive sentence, they resort to either of the following options: Transposing English passives into verbal nouns (masdar), or into pseudo-active verbs or active sentence structures, or into vowel melody passives, or omitting these passive structures.

This paper reports on patterns of verb choice in identifying relational clauses (e.g. ‘X is Y, Y is X’) in English technical manuals. While it is obvious that specific lexical verbs will feature in identifying clauses of different functions, e.g. mean (defining), call (naming), exemplify (exemplifying), less transparent is the distribution of these more specific verbs and the general or neutral verb be. The findings suggest that verb choice in (technical) identifying clauses is strongly associated with the degree of equivalence constructed between the two central nominal groups in the clause (the Token and Value). Equivalence relations are one-to-one (rather than one-to-many) and exhaustive (rather than semantically open). Major grammatical influences on equivalence include nominal group structure, ergativity of the clause, and the inclusion of features (e.g. interpersonal, logical or textual) that undermine the privileging of an experientially homogeneous world-view. The results challenge the notions that be and specific verbs are interchangeable and that be is an unmarked choice. On the contrary, the data reveal that under certain conditions be is the more marked choice. The results have practical implications for teachers and students of English (in particular, students of English for Academic and/or Specific Purposes) as well as translators.

Translation is a language activity that involves intercultural activities. The study’s focus is on subtitling as a didactic tool for relating exactness of information and cultural preservation: The Igbo language Mediascape example, by looking at the correctness of the subtitled expressions in context, in the movie used for the study. Language is a human form of communication in his sociocultural environment as well as culture which is people's way of life. The study adopted the frameworks of Gotlieb's strategy and Nida's equivalence to tackle the study’s problems. It also adopted the methodology of description and emergent design approach in the study. For the correctness of the source information expressions in context, it is discovered that by the use of Gotlieb's strategy and Nida's translation equivalence, the study was able to transfer right messages in the context in which they are used. It is discovered that the research objective of the study is achieved thereby attaining the signification of the study.

This article examines a question of the interest of scholars dealing with phraseology, terminology and translation, namely the task of translating and finding equivalents of idiomatic expressions, such as specialized phraseological units (henceforth SPUs), especially those in which a dead metaphor underlies. Among the unsolved questions that phraseology still struggles with to establish itself as a discipline on its own right there are two hindering factors that are related to terminology and translation: on the one hand, specialized phraseology is an under-explored and a not institutionalized line of research, to the point of being deemed a non-coherent research field (Kjær, 2007, p. 507). On the other hand, phraseology is considered to be a missing training subject in translation academic syllabi (Corpas Pastor, 2003, p. 222). Therefore, this study intends to offer descriptive data that could be used as a starting point for finding answers regarding the identification and even the creation of equivalents for SPUs that include dead metaphors among their lexical components. The aim of this article is two-fold, (i) it will offer a series of linguistic analyses (morphosyntactic and semantic) of the word forms in the SPUs being analyzed, and their equivalents and (ii) it will shed light on the translation techniques (Molina & Hurtado Albir, 2002, pp. 509-511) used to coin the equivalents of these SPUs.

A design point is inessential when it does not contribute to an optimal design, and can therefore be safely discarded from the design space. We derive three inequalities for the detection of such inessential points in c-optimal design: the first two are direct consequences of the equivalence theorem for c-optimality; the third one is derived from a second-order cone programming formulation of c-optimal design. Elimination rules for A-optimal design are obtained as a byproduct. When implemented within an optimization algorithm, each inequality gives a screening test that may provide a substantial acceleration by reducing the size of the problem online. Several examples are presented with a multiplicative algorithm to illustrate the effectiveness of the approach.

We fill a gap in the literature regarding `transport of structure' for (n+2)-angulated, n-exact, n-abelian and n-exangulated categories appearing in (classical and higher) homological algebra. As an application of our main results, we show that a skeleton of one of these kinds of categories inherits the same structure in a canonical way, up to equivalence. In particular, it follows that a skeleton of a weak (n+2)-angulated category is in fact what we call a strong (n+2)-angulated category. When n=1 this clarifies a technical concern with the definition of a cluster category. We also introduce the notion of an n-exangulated functor between n-exangulated categories. This recovers the definition of an (n+2)-angulated functor when the categories concerned are (n+2)-angulated, and the higher analogue of an exact functor when the categories concerned are n-exact., Comment: v3: 24 pages; minor typographical changes; accepted in Journal of Algebra

Formal criteria of theoretical equivalence are mathematical mappings between specific sorts of mathematical objects, notably including those objects used in mathematical physics. Proponents of formal criteria claim that results involving these criteria have implications that extend beyond pure mathematics. For instance, they claim that formal criteria bear on the project of using our best mathematical physics as a guide to what the world is like, and also have deflationary implications for various debates in the metaphysics of physics. In this paper, I investigate whether there is a defensible view according to which formal criteria have significant non-mathematical implications, of these sorts or any other, reaching a chiefly negative verdict. Along the way, I discuss various foundational issues concerning how we use mathematical objects to describe the world when doing physics, and how this practice should inform metaphysics. I diagnose the prominence of formal criteria as stemming from contentious views on these foundational issues, and endeavor to motivate some alternative views in their stead.

Google Translate (GT) is the most widely used translator application in the world. The function of GT is not merely as tools but has become a means in personal communication, learning and business matters. This paper aims to examine the GT accuracy in translating culinary texts. This paper used a semiotic approach to analyze the equivalence of GT from the source language to the target language. The data source as the object of study is French culinary texts retrieved from the internet. It can be concluded that the accuracy of GT in culinary texts lies in words, phrases and sentences. GT does not yet have good accuracy in translating culture between source and target languages. In the semiotic perspective, the GT translation model is the translation from the source language form to the target language form (signifier) by maintaining the concept (meaning). GT does not yet have a translation feature in a cultural context. The advancement in information technology shows that GT, as a human-robot, can replace human translators.

This paper aims to explore how translators translate both the connotative and denotative meanings of near-synonyms from the Quran into English language. The article will shed light on the phenomenon of near-synonymy, as well as its connotative and denotative meanings and how the translator’s background could have influenced their translation. There has been a dearth of attention on the translation of near-synonyms in the Quran; accordingly, this study examines three pairs of near-synonyms from the Quran and their particular translations in the following three English translations of the Quran itself : 1) The Koran Interpreted by Arberry; 2) The Quran: A New Translation by Abdel Haleem; and 3) The Sublime Quran by Bakhtiar. These translations were chosen due to the significant differences in style and translators’ backgrounds. The analysis aims to highlight the difference in meaning of each pair of near-synonyms by distinguishing both their connotative and denotative meanings. This will be followed by an examination of the translations to recognise whether the near-synonyms were accurately translated in these given instances or lost some, or even all, of their meaning during the translation process and discuss if translator’s background could have influence on it. Based on the discussion and analysis of these examples, it is evident that all three translations failed to distinguish between the pair of near-synonyms and to capture the accurate meaning throughout the Quran, leading to a semantic void. It is similarly clear that the linguistic complexity of the Holy Quran has created a challenging mission for translators, which has ultimately led to loss of accuracy and meaning. The results have shown that each translator chose their own approach based on their translational goal or their educational and personal backgrounds. Keywords: Quran; Near-Synonyms; Quran Translation; Connotative Meaning; Equivalence

Finitary Idealized Concurrent Algol (FICA) is a prototypical programming language combining functional, imperative, and concurrent computation. There exists a fully abstract game model of FICA, which in principle can be used to prove equivalence and safety of FICA programs. Unfortunately, the problems are undecidable for the whole language, and only very rudimentary decidable sub-languages are known. We propose leafy automata as a dedicated automata-theoretic formalism for representing the game semantics of FICA. The automata use an infinite alphabet with a tree structure. We show that the game semantics of any FICA term can be represented by traces of a leafy automaton. Conversely, the traces of any leafy automaton can be represented by a FICA term. Because of the close match with FICA, we view leafy automata as a promising starting point for finding decidable subclasses of the language and, more generally, to provide a new perspective on models of higher-order concurrent computation. Moreover, we identify a fragment of FICA that is amenable to verification by translation into a particular class of leafy automata. Using a locality property of the latter class, where communication between levels is restricted and every other level is bounded, we show that their emptiness problem is decidable by reduction to Petri net reachability., Comment: 18 pages plus appendices

Automata theory based on quantum logic has been established by Ying. Nondeterministic fuzzy finite automata theory has been proposed by Cao, and further generalized by Pan et al. In this paper, we propose the notion of nondeterministic finite automaton based on quantum logic whose underlying structure is a complete orthomodular lattice l, called nondeterministic l-valued finite automaton (Nl-FA, for short). We show that nondeterministic l-valued finite automata, deterministic l-valued finite automata, and nondeterministic l-valued finite automata with e-moves are equivalent if and only if l satisfies the distributive law. Next, two l-valued relations in terms of language equivalence are given. Some properties of the two l-valued relations under various operations such as reversal, union, product, and concatenation, are investigated. Finally, we give the degree of the closeness between two Nl-FAs with the same set of states to reflect the robustness, and obtain some interesting results. The theory developed in this paper enriches the automata theory based on quantum logic.

A decidability proof for bisimulation equivalence of first-order grammars is given. It is an alternative proof for a result by S\'enizergues (1998, 2005) that subsumes his affirmative solution of the famous decidability question for deterministic pushdown automata. The presented proof is conceptually simpler, and a particular novelty is that it is not given as two semidecision procedures but it provides an explicit algorithm that might be amenable to a complexity analysis., Comment: version accepted to JCSS

The paper analyses Latvian and German somatic idioms in the dictionaries by K. Ulmann and K. Ulmann / G. Braže. Up to now the researchers of Latvian phraseology have not focused to analyse these theme – especially in diachronic aspect. The paper presents the most fixed somatic idioms in the Latvian and German and their equivalence types. The author compares with the meanings of idioms from the first dictionary (1638) to modern electronic dictionary “Modern Latvian dictionary”. KEY WORDS: the dictionaries by K. Ulmann and K. Ulmann / G. Braže, somatic idioms, somatic components, the equivalence types of German–Latvian somatic idioms. DOI: http://dx.doi.org/10.15181/rh.v19i0.1329

This paper aims to explain the concept of Tarkib Isnadi in Arabic grammar and describe the equivalent concept and its components in Indonesian grammar. In the realm of Arabic grammar, Tarkib Isnadi is a core component in the structure of clauses or sentences in Arabic. A good understanding of Tarkib Isnadi in Arabic and its equivalent in Indonesian will make it easier for Arabic learners (L2) who come from native Indonesian speakers (L1) to identify clause and sentence structures in various Arabic discourses. The methods used in data analysis in this study are distribution and identity-referential methods. Based on observations, it is found that the concept of Tarkib Isnadi in Arabic has a concept equivalent to a clause in Indonesian because both have the core constituents or pillars of the sentence. On the other hand, there are also some differences in the concept of Tarkib Isnadi in Arabic with the concept of clauses in Indonesian. The difference mainly lies in terms of the formation of the concept and the filling components of their syntactic functions.

El examen de los nombres con sentido locativo del español y del chino se prestan a un análisis contrastivo, que entre otros aspectos pone de manifiesto la complejidad y riqueza de los procesos morfológicos que intervienen en la formación léxica, y permiten observar las relaciones que se establecen entre los mecanismos más sistemáticos y productivos de ambos códigos. Se comprueba la equivalencia entre los núcleos nominales de la composición sintagmática del español con los formantes locativos del chino. Aunque, en español no parece darse un caso claro de gramaticalización semejante al que ha experimentado algún formante locativo del chino y, por otra parte, se argumenta que mientras algunos formantes del chino alcanzan cierta autonomía léxica en determinados contextos, otros se corresponden funcionalmente con los elementos sufijales del español.

Language models trained on billions of tokens have recently led to unprecedented results on many NLP tasks. This success raises the question of whether, in principle, a system can ever “understand” raw text without access to some form of grounding. We formally investigate the abilities of ungrounded systems to acquire meaning. Our analysis focuses on the role of “assertions”: textual contexts that provide indirect clues about the underlying semantics. We study whether assertions enable a system to emulate representations preserving semantic relations like equivalence. We find that assertions enable semantic emulation of languages that satisfy a strong notion of semantic transparency. However, for classes of languages where the same expression can take different values in different contexts, we show that emulation can become uncomputable. Finally, we discuss differences between our formal model and natural language, exploring how our results generalize to a modal setting and other semantic relations. Together, our results suggest that assertions in code or language do not provide sufficient signal to fully emulate semantic representations. We formalize ways in which ungrounded language models appear to be fundamentally limited in their ability to “understand”.

In this article the semantic structures of constructing American blog discourse are analyzed. Those structures are based upon semantic relations between propositions in the text of the blogs and aim to enhance coherence in this discourse. The results show that particular types of interpropositional relations are used on macro-semantic level for different subgenres of blogs (the semantic relations of equivalence, comparison, contrast, ‘part-whole’/’whole-part’, implication/causality, chronological order and spatial order relations). In particular, these interpropositional relations differ in the subgenres, such as political, business, socio-cultural, technology, and sports. In addition, the analysis brings out the different percentage of their usage.Manuscript received 23.04.2020

The human brain, which can be programmed through a multiplicity of practices, is the foundation of NLP. Language teachers can effectively program their students for improved language output if made aware of the Neuro-functioning of the brain. This new-fangled aspect of language teaching is, hitherto, an uncharted area in the Pakistani teaching context. The current study seeks to look into the existing estate of English language pedagogy in Pakistani scenario with the assistance of the NLP Milton Model, based on the employment of the language patterns by famous hypnotist-Milton Erickson. The focal point of this model is- presupposition, mind read, lost performative, unspecified verb, comparative deletion, cause and effect, universal quantifier, complex equivalence, modal operator, nominalization, and unspecified referential index. It has implications, to a great extent, in ELT to generate preferred results. For this study, the sample population is chosen through purposive sampling technique and encompasses language skills’ classes; whereas, the five English Language institutions were preferred through random sampling method. This study, accordingly, underpins the exploitation of NLP as a toolkit for effectual language pedagogy. Besides, it also advocates copious ways for meaningful, motivational, and momentous communication between language teachers and learners.

Nowadays, people can easily access everything with one-click away. For example, when you want to read an article in foreign language which you are not familiar with, then you just need to open Google Translate and within seconds, you will get the translation of it. To deal with that reality, a translator has to differentiate himself from machine translation which is increasingly used by the public. Therefore, the translator is required to produce an equivalent and natural translation in the Target Language. This research aims to provide understanding of translation equivalence on video transcripts conducted by students in Movie Translation (Subtitling) course. This study uses qualitative approach, content analysis method, and purposive sampling to collect data. In short, there are two types of translation equivalence used by students, formal and dynamic. Formal equivalence focuses on the similarity of the form and meaning of the message from Source Language to Target Language, while dynamic one focuses on the naturalness of expression in the Target Language.

Semantics is meaning communicated through language (Saeed I.J.). Semantics is the study of relationship between words and their meanings; it is directly linked with the conceptual meaning of words, and the associative meaning. Semantic sieve as a concept is an innovative phenomenon. This linguistic phenomenon is a process whereby a word is dispersed through a semantic tunnel which in some cases produces different meaning. This is explained through different models. The semantic sieve is related to translation, where the deep structure of words differs from the surface structure. There are some concepts and words in Akan and English that are absent in Russian, others are known in Akan but virtually absent in the English language.

Discourse theorists often defend their discursive stance on ‘reality’ and the material with reference to Laclau and Mouffe’s quote that, while an “earthquake or the falling of a brick…exist externally to thought,” they cannot “constitute themselves as objects outside any discursive conditions of emergence”. While fully endorsing this statement, we argue that it does not licence discourse theorists to consider discursive formations divorced from their material context, but obliges us to account for the constraints and affordances of the material conditions on the structuring of the discursive field itself. Drawing on previous work, we argue that material conditions may render discourse systems incommensurate, such that they cannot be articulated through chains of equivalence within a radically restructured field. We suggest as a way forward the concept of the nomadic politician continually traversing between equivalential systems in order to reconfigure and renegotiate key signifiers within the materially-constrained discursive fields of each.

We consider an object calculus in which open terms interact with the environment through interfaces. The calculus is intended to capture the essence of contextual interactions of Middleweight Java code. Using game semantics, we provide fully abstract models for the induced notions of contextual approximation and equivalence. These are the first denotational models of this kind.

Let V be an n-dimensional linear space over an algebraically closed base field. We provide a general method for classifying, up to equivalence, all bilinear maps f : V × V → V such that d i m ( r a...

In this paper, we develop a technique which enables us to obtain several results from the theory of Γ-semigroups as logical implications of their semigroup theoretical analogues.

Reflex is a process-oriented language that provides a design of easy-to-maintain control software for programmable logic controllers. The language has been successfully used in a several reliability critical control systems, e. g. control software for a silicon single crystal growth furnace and electronic equipment control system. Currently, the main goal of the Reflex language project is to develop formal verification methods for Reflex programs in order to guarantee increased reliability of the software created on its basis. The paper presents the formal operational semantics of Reflex programs extended by annotations describing the formal specification of software requirements as a necessary basis for the application of such methods. A brief overview of the Reflex language is given and a simple example of its use – a control program for a hand dryer – is provided. The concepts of environment and variables shared with the environment are defined that allows to disengage from specific input/output ports. Types of annotations that specify restrictions on the values of the variables at program launch, restrictions on the environment (in particular, on the control object), invariants of the control cycle, pre- and postconditions of external functions used in Reflex programs are defined. Annotated Reflex also uses standard annotations assume, assert and havoc. The operational semantics of the annotated Reflex programs uses the global clock as well as the local clocks of separate processes, the time of which is measured in the number of iterations of the control cycle, to simulate time constraints on the execution of processes at certain states. It stores a complete history of changes of the values of shared variables for a more precise description of the time properties of the program and its environment. Semantics takes into account the infinity of the program execution cycle, the logic of process transition management from state to state and the interaction of processes with each other and with the environment. Extending the formal operational semantics of the Reflex language to annotations simplifies the proof of the correctness of the transformation approach to deductive verification of Reflex programs developed by the authors, transforming an annotated Reflex program to an annotated program in a very limited subset of the C language, by reducing a complex proof of preserving the truth of program requirements during the transformation to a simpler proof of equivalence of the original and the resulting annotated programs with respect to their operational semantics.

We obtain a weak homotopy equivalence type result between two topological groups associated with a Kirchberg algebra: the unitary group of the continuous asymptotic centralizer and the loop group of the automorphism group of the stabilization. This result plays a crucial role in our subsequent work on the classification of poly-$\mathbb{Z}$ group actions on Kirchberg algebras. As a special case, we show that the $K$-groups of the continuous asymptotic centralizer are isomorphic to the $KK$-groups of the Kirchberg algebra., 32 pages

Reachability analysis is a fundamental program analysis with a wide variety of applications. We present FlowCFL, a type-based reachability analysis that accounts for mutable heap data. The underlying semantics of FlowCFL is Context-Free-Language (CFL)-reachability. We make three contributions. First, we define a dynamic semantics that captures the notion of flow commonly used in reachability analysis. Second, we establish correctness of CFL-reachability over graphs with inverse edges (inverse edges are necessary for the handling of mutable heap data). Our approach combines CFL-reachability with reference immutability to avoid the addition of certain inverse edges, which results in graph reduction and precision improvement. The key contribution of our work is the formal account of correctness, which extends to the case when inverse edges are removed. Third, we present a type-based reachability analysis and establish equivalence between a certain CFL-reachability analysis and the type-based analysis, thus proving correctness of the type-based analysis.

We determine the possible functions that can occur, up to asymptotic equivalence, as growth functions of semigroups, hereditary languages, and algebras.

This paper examines the relationship between the companion forms of regular matrix polynomials with singular leading coefficients. When two such polynomials have the same underlying finite and infinite Jordan structures, it is shown that their companion forms are connected by a strict equivalence transformation that can be parameterized using the commutant of the companion forms' common Weierstrass canonical form. The process developed herein for generating such parameterized transformations is applied to the useful class of diagonalizable quadratic polynomials.

Several formalisms for language syntax specification exist in literature. In this paper, we prove that longstanding syntactical transformations between context-free grammars and algebraic signatures are adjoint functors and/or adjoint equivalences that preserve the abstract syntax of the generated terms. The main result is a categorical equivalence between the categories of algebras (i.e., all the possible semantics) over the objects in these formalisms up to the provided syntactical transformations, namely that all these language specification frameworks are essentially the same from a semantic perspective.

This research is a study on cultural word translation strategies from Indonesian into Japanese. The purposes of the study are: firstly, identifying cultural words that do not have any equivalence between the source language (TSu) secondly, investigating the translation strategies used for those words with no equivalence; and thirdly, finding out the meaning shift occurring in the process of translation. The research employs a descriptive qualitative method. The strategies used by the translator include: 1) translation using more general terms, 2) translation using loan words or loan words with explanation, 3) translation using paraphrase. Two meaning shifts are found: 1) shift from generic to more specific or vice versa, and 2) shift because of different cultural point of view.

We show basic results on super-manifolds and super Lie groups over a complete field of characteristic $\ne 2$, extensively using Hopf-algebraic techniques. The main results are two theorems. The first main theorem shows a category equivalence between super Lie groups and Harish-Chandra pairs, which is applied especially to construct the Hopf super-algebra of all analytic representative functions on a super Lie group. The second constructs homogeneous super-manifolds by a new Hopf-algebraic method, showing their remarkable property., Comment: Added an article, [4], and two remarks, Remarks 3.8 and 7.3

Cobordism of virtual string links on n strands is a combinatorial generalization of link cobordism. There exists a bijection between virtual string links on n strands up to cobordisms and elements of the direct product of n ( n − 1) copies of the integers. This paper also shows that virtual string links up to unwelded equivalence are classified by those groups. Finally, the related theory of welded string link cobordism is defined herein and shown to be trivial for string links with one component.

International audience; We identify a new decidable class of security protocols, both for reachability and equivalence properties. Our result holds for an unbounded number of sessions and for protocols with nonces. It covers all standard cryptographic primitives. Our class sets up three main assumptions. (i) Protocols need to be "simple", meaning that an attacker can precisely identify from which participant and which session a message originates from. We also consider protocols with no else branches (only positive test). (ii) Protocols should be type-compliant, which is intuitively guaranteed as soon as two encrypted messages of the protocol cannot be confused. (iii) Finally, we define the notion of a dependency graph, which, given a protocol, characterises how actions depend on the other ones (both sequential dependencies and data dependencies are taken into account). Whenever the graph is acyclic, then the protocol falls into our class. We show that many protocols of the literature belong to our decidable class, including for example some of the protocols embedded in the biometric passport.

In this study, the recursive three-step filter method introduced by Gillijns and Moor (2007) is proved strictly to be equivalent to the augment Kalman filter (AKF) when the covariance of process noise about the input approaches infinity. This result indicates that if the information about the exogenous input is unknown, the AKF can also be used to simultaneously obtain the state and exogenous input estimation. Numerical examples illustrate the authors' main results.

Bisimulation is a concept that captures behavioural equivalence of states in a transition system. In [Linan Chen, Florence Clerc, and Prakash Panangaden, Bisimulation for feller-dynkin processes, in: Proceedings of the Thirty-Fifth Conference on the Mathematical Foundations of Programming Semantics, Electronic Notes in Theoretical Computer Science 347 (2019) 45–63.], we proposed two equivalent definitions of bisimulation on continuous-time stochastic processes where the evolution is a flow through time. In the present paper, we develop the theory further: we introduce different concepts that correspond to different behavioural equivalences and compare them to bisimulation. In particular, we study the relation between bisimulation and symmetry groups of the dynamics. We also provide a game interpretation for two of the behavioural equivalences. We then compare those notions to their discrete-time analogues.

Algebras can be used to interpret the behaviour of effectful programs. In particular, we use Eilenberg-Moore algebras given over a complete lattices of truth values, which specify answers to queries about programs. The algebras can be used to formulate a quantitative logic of behavioural properties, specifying a congruent notion of program equivalence coinciding with a notion of applicative bisimilarity. Many combinations of effects can be interpreted using these algebras. In this paper, we specify a method of generically combining effects and the algebras used to interpret them. At the core of this method is the tensor of complete lattices, which combines the carrier sets of the algebras. We show that this tensor preserves complete distributivity of complete lattices. Moreover, the universal properties of this tensor can then be used to properly combine the Eilenberg-Moore algebras. We will apply this method to combine the effects of probability, global store, cost, nondeterminism, and error effects. We will then compare this method of combining effects with the more traditional method of combining equational theories using interaction laws.

Kozen introduced probabilistic propositional dynamic logic (PPDL) in 1985 as a compositional framework to reason about probabilistic programs. In this paper we study expressiveness for PPDL and provide a series of results analogues to the classical Hennessy-Milner theorem for modal logic. First, we show that PPDL charaterises probabilistic trace equivalence of probabilistic automata (with outputs). Second, we show that PPDL can be mildly extended to yield a characterisation of probabilistic state bisimulation for PPDL models. Third, we provide a different extension of PPDL, this time characterising probabilistic event bisimulation.

We investigate a version of the Green correspondence for categories of complexes, including homotopy categories and derived categories. The correspondence is an equivalence between a category defined over a finite group G and the same for a subgroup H, often the normalizer of a p-subgroup of G. We present a basic formula for deciding when categories of modules or complexes have a Green correspondence and apply it to many examples. In several cases the equivalence is an equivalence of triangulated categories, and in special cases it is an equivalence of tensor triangulated categories.

Character equivalence and offensive word rank in subtitling context are understudied on the previous studies on euphemisation strategies. The exclusion of these two concerns leaves the prior constructed euphemisation strategies unable to explain how shifts on narrative identity might occur and how taboo words are functionally negotiated. In addressing this issue, the study investigates the relationship between offensive word levels with character equivalence and narrative identity, types of euphemisation strategies , and the strategies' implementation. The data were collected from the English and Indonesian versions of four films containing taboo words, which were analyzed by applying the theories of offensiveness rank by Ofcom, constructed in English as a foreign language context, and character equivalence by Petrucci. T he findings indicate tha t offensive word translation suffers a rank shift on offensive word ranks Departing from these findings. We propose euphemisation strategies with offensive word rank and character equivalence as the primary narrative basis with mediality and subtitling standard as the primary mechanical basis. Those strategies are downgrading, degrading, sidegrading, outgrading, ingrading, and retrograding. The reasons of euphemisation strategy implementation are bipolarly divided into aesthetics and mechanics in relation to distances and perspectives of the applied offensive words.

In this paper, we study the problem of formal verification for Answer Set Programming (ASP), namely, obtaining a formal proof showing that the answer sets of a given (non-ground) logic program P correctly correspond to the solutions to the problem encoded by P, regardless of the problem instance. To this aim, we use a formal specification language based on ASP modules, so that each module can be proved to capture some informal aspect of the problem in an isolated way. This specification language relies on a novel definition of (possibly nested, first order) program modules that may incorporate local hidden atoms at different levels. Then, verifying the logic program P amounts to prove some kind of equivalence between P and its modular specification. Under consideration for acceptance in TPLP., Comment: Paper presented at the 36th International Conference on Logic Programming (ICLP 2019), University Of Calabria, Rende (CS), Italy, September 2020, 16 pages

The current study aims to examine through lexical stylistic analysis and comparison, the differences and the disparateness of meaning and style in rendering the Quranic verbal irony into English, in the work of Mohammed. A.S Abdel Haleem, Mohammed. M Pickthall and Mohammed Khan and Mohammed Taj Al-Din Al-Hilali . Also, the study aims to investigate how the three translators deal with the Quranic verbal irony in their translations into English. This has its powerful consequence in attaining a better understanding on the part of the Holy Quran translators and subsequently of English language receptors in general and for non- Arabic Muslims in particular, where the Qur’anic verbal irony concerned. Also, the study aims to identify the translation strategies employed by the three translators in rendering the Quranic verbal. irony Moreover, the study revealed that the Qur’anic verbal irony is conspicuous occurrence in the Holy Quran and that the process of rendering them into English is generally problematic for the reasons such as linguistic and cultural divergences and discrepancies. Finally, the study gives two ideas; firstly, the equivalence in translation should be examined as a concept that holds a place on a scale that can begin very equivalent to inequivalent. Secondly, better translation of the Holy Quran should bear intelligibility in terms of a total impact of the Message on the language receptor.

Article presents an approach to correctness validation of autotuning optimizational transformations. Autotuner is considered as dynamic discrete system and validation is reduced to verification of characteristic of equivalence by result of representation of initial and optimized program versions in autotuning formal model. In partial cases this validation can be done automatically using source code and rewriting rules technique. Problems in programming 2020; 2-3: 368-374

In this paper, we introduce the notion of a noncommutative Poisson bialgebra, and establish the equivalence between matched pairs, Manin triples and noncommutative Poisson bialgebras. Using quasi-representations and the corresponding cohomology theory of noncommutative Poisson algebras, we study coboundary noncommutative Poisson bialgebras which leads to the introduction of the Poisson Yang-Baxter equation. A skew-symmetric solution of the Poisson Yang-Baxter equation naturally gives a (coboundary) noncommutative Poisson bialgebra. Rota-Baxter operators, more generally O -operators on noncommutative Poisson algebras, and noncommutative pre-Poisson algebras are introduced, by which we construct skew-symmetric solutions of the Poisson Yang-Baxter equation in some special noncommutative Poisson algebras obtained from these structures.

Community detection in static networks solely emphasizes the clustering accuracy, while evolving community detection in dynamic networks simultaneously takes into account both the clustering accuracy and clustering drift. The available evolutionary clustering algorithms are criticized for failing to fully characterize dynamics of networks and to accurately balance the clustering accuracy and clustering drift. To solve these problems, we propose a co-regularized evolutionary nonnegative matrix factorization for evolving communities in dynamic networks (Cr-ENMF). Specifically, both the network and communities at the previous time step are utilized to characterize the clustering drift, which are incorporated into the objective function of Cr-ENMF by regularization. We show that the well-known temporal smoothness framework for evolutionary clustering is a special case of the proposed framework, and prove the equivalence between Cr-ENMF and evolutionary clustering. Thereafter, an iterative strategy is presented to optimize the objective function. The experimental results over both artificial and real world dynamic networks illustrate that Cr-ENMF outperforms state-of-the-art approaches.

The introduction of the Automated Teller Machine (ATM) by financial institutions has changed the face of banking globally, Nigeria inclusive. The mechanism has provided a kind of collective sigh-of-relief to both the bank and their customers, offering convenient, speedy and round the clock services. However, it is not without some inherent challenges as many bank customers who are not proficient in English language found the ATM cumbersome and unfriendly. Attempting to provide solution to these challenges, some banks in Nigeria have developed and introduced the indigenous language version of the Automated Teller Machine options. Yet, user’s response did not reflect the anticipated level of enthusiasm as a result of operational complexities and translation equivalence challenges especially for the Yoruba menu option. In view of this, this work makes an attempt to present an improved translation model introducing Yoruba tone marking to assist those who do not understand the English language, but are monolingual only in Yoruba language to effectively interact with the system. Specifically, an attempt is made to translate the menu option of Automated Teller Machine in conformity with the phonological and morphological processes in Yorùbá, following the natural strategy of lexical expansion in the Yorùbá language itself. Phrases and sentences of translation were conducted, employing equivalent model. The data (content) considered were arranged bearing in mind the principle of relatedness for proper reference and analysis. During translation, the strategies of morphological processes of semantic extension, borrowing, nominalization, indigenization and composition were used. The system framework designed to test the model was found to reflect the anticipated level of user’s enthusiasm. The research work does not only assist those who are not proficient in English language to effectively interact with the system, but also overcomes the challenges of the present design and consequently widens the scope of ATM usage in the interior parts of the country.

The aim of this paper is to introduce the notion of cat$^{\bf {1}}-$groupoids which are the groupoid version of cat$^{\bf {1}}-$groups and to prove the categorical equivalence between crossed modules over groupoids and cat$^{\bf {1}}-$groupoids. In section 4 we introduce the notions of crossed squares over groupoids and of cat$^{\bf {2}}-$groupoids, and then we show their categories are equivalent. These equivalences enable us to obtain more examples of groupoids.

Many tight frames of interest are constructed via their Gramian matrix (which determines the frame up to unitary equivalence). Given such a Gramian, it can be determined whether or not the tight frame is projective group frame, i.e., is the projective orbit of some group $G$ (which may not be unique). On the other hand, there is complete description of the projective group frames in terms of the irreducible projective representations of $G$. Here we consider the inverse problem of taking the Gramian of a projective group frame for a group $G$, and identifying the cocycle and constructing the frame explicitly as the projective group orbit of a vector $v$ (decomposed in terms of the irreducibles). The key idea is to recognise that the Gramian is a group matrix given by a vector $f\in\mathbb{C}^G$, and to take the Fourier transform of $f$ to obtain the components of $v$ as orthogonal projections. This requires the development of a theory of group matrices and the Fourier transform for projective representations. Of particular interest, we give a block diagonalisation of (projective) group matrices. This leads to a unique Fourier decomposition of the group matrices, and a further fine-scale decomposition into low rank group matrices., 26 pages