<p> This thesis determines necessary and sufficient conditions for an equational class to be modular and finds a modular property that is equivalent to permutability.</p> / Thesis / Master of Science (MSc)

No description available.

<p> Commutative semigroup equations are described, and rules of inference for them are given. Then a skeleton sublattice of the lattice of equational classes of commutative semigroups is described, and a partial description is given of the way in which the rest of the lattice hangs on the skeleton.</p> / Thesis / Doctor of Philosophy (PhD)

<p> In this thesis, we study the concept of injectivity in equational classes of (universal) algebras and in particular we are concerned with congruence distributive equational classes that have enough injectives. We show that every reasonable equationally complete congruence distributive equational class has enough injectives and we describe them completely. We then examine what equational subclasses of Lattices, Heyting algebras, and pseudo-complemented lattices have enough injectives.</p> / Thesis / Doctor of Philosophy (PhD)

The lattice of equational classes of idempotent semigroups is completely described. It is shown that every equational class of idempotent semigroups is determined by a single equation (in addition to the associative and idempotent equations). A method is presented for finding which class a given equation determines, and when the class determined by one equation is contained in the class determined by a second equation. / Thesis / Doctor of Philosophy (PhD)

Multi-stage programming (MSP) is a style of writing program generators---programs which generate programs---supported by special annotations that direct construction, combination, and execution of object programs. Various researchers have shown MSP to be effective in writing efficient programs without sacrificing genericity. However, correctness proofs of such programs have so far received limited attention, and approaches and challenges for that task have been largely unexplored. In this thesis, I establish formal equational properties of the multi-stage lambda calculus and related proof techniques, as well as results that delineate the intricacies of multi-stage languages that one must be aware of. In particular, I settle three basic questions that naturally arise when verifying multi-stage functional programs. Firstly, can adding staging MSP to a language compromise the interchangeability of terms that held in the original language? Unfortunately it can, and more care is needed to reason about terms with free variables. Secondly, staging annotations, as the term ``annotations'' suggests, are often thought to be orthogonal to the behavior of a program, but when is this formally guaranteed to be the case? I give termination conditions that characterize when this guarantee holds. Finally, do multi-stage languages satisfy extensional facts, for example that functions agreeing on all arguments are equivalent? I develop a sound and complete notion of applicative bisimulation, which can establish not only extensionality but, in principle, any other valid program equivalence as well. These results improve our general understanding of staging and enable us to prove the correctness of complicated multi-stage programs.

<p>Ova teza se bavi &curren;-kvazilinearnim varijetetima grupoida. Pokazano je da postoji ta&middot;cno dvadeset osam idempotentnih &curren;-kvazilinearnih varijeteta grupoida, od kojih dvadeset &middot;sest varijeteta imaju kona&middot;cnu bazu i te baze su i navedene, dok preostala dva varijeteta imaju inherentno beskona&middot;cnu bazu. U tezi je opisano ured enje svih idempotentnih &curren;-kvazilinearnih varijeteta grupoida i nalazimo male grupoide koji generi&middot;su svaki od navedenih varijeteta. Na kraju je pokazano da postoji kontinum mnogo &curren;-kvazilinearnih variejeteta grupoida.</p> / <p>The topic of this thesis are &curren;-quasilinear varieties of groupoids.<br />We show that there exist exactly twenty-eight idempotent &curren;-quasilinear varieties of groupoids, twenty-six of which are &macr;nitely based (and we explicitly<br />give &macr;nite bases for each of them), while two are inherently non&macr;nitely based.<br />We describe the ordering of these twenty-eight idempotent &curren;-quasilinear varieties of groupoids and &macr;nd small generating algebras for each of them. In<br />the end we show that there exist continuum many &curren;-quasilinear varieties of<br />groupoids, not all of which are even locally &macr;nite.</p>

In Arabic inna wa-aḫawātu-hā ‘inna and its related sisters’ are traditionally considered as verb-like particles. They are specified as introducing equational sentences and change their constituents’ case to a different pattern from what verbs do. Therefore, they are called nawāsiḫ in Arabic, or words that cause a shift to the accusative case (Ryding 2005). The medieval grammarians’ treatment of inna and its sisters as verb-like particles and of the equational sentence in general is based on the theory of ‘amal, ‘government’ which Sībawayhi has described it in his book Al-kitab. The theory presumes a grammatical operation (‘amal) in which an operator (‘āmil) assigns to a unique operand (ma’mūl) a grammatical function (Carter, 1973, 151). However, in modern linguistics, government is realized as a syntactic relation that imposes case agreement between the syntactic elements in the sentential structure. And this structure has a deep representation and surface representation. The Medieval treatment for the equational sentence introduced by inna is problematic, because it attributes to inna a verbal power to resolve the issue of the case assignment to the equational sentence which lacks an overt syntactic operator. Modern approaches to equational sentence differ totally from the traditional account. Some modern approaches propose a copula for the equational sentence; this copula is either covert or deleted. Other modern approaches propose a tense projection in deep structure that determines an equational sentence’s surface form. Neither sort of approach gives a reasonable explanation for the case assignment pattern, for the general properties of equational sentences, or for the status of inna. In this study, I propose a new approach focusing on the role of semantics in the assignment of case in equational sentences in Arabic. My hypothesis is based on a new interpretation to Sībawayhi’s description of the ‘ibtida’ sentence; according to this new interpretation ibtida’ is not a syntactic operator but rather a semantic one. I also propose that a sentence’s syntactic properties are sensitive to its semantic MODE, a specification of whether it expresses a topic-based proposition; or an event-based proposition. My new hypothesis is intended to apply to all varieties of Arabic including Classical Arabic, and Modern Standard Arabic, as well as the regional dialects of Arabic.

While there are efforts to establish a single international accounting standard, there are strong current and future needs to handle heterogeneous accounting methods and systems. We advocate a context-based approach to dealing with multiple accounting standards and equational ontological conflicts. In this paper we first define what we mean by equational ontological conflicts and then describe a new approach, using Constraint Logic Programming and abductive reasoning, to reconcile such conflicts among disparate information systems. In particular, we focus on the use of Constraint Handling Rules as a simultaneous symbolic equation solver, which is a powerful way to combine, invert and simplify multiple conversion functions that translate between different contexts. Finally, we demonstrate a sample application using our prototype implementation that demonstrates the viability of our approach. / Singapore-MIT Alliance (SMA)

We present a term rewriting procedure based on congruence closure that can be used with arbitrary equational theories. This procedure is motivated by the pragmatic need to prove equations in equational theories where confluence can not be achieved. The procedure uses context free grammars to represent equivalence classes of terms. The procedure rewrites grammars rather than terms and uses congruence closure to maintain certain congruence properties of the grammar. Grammars provide concise representations of large term sets. Infinite term sets can be represented with finite grammars and exponentially large term sets can be represented with linear sized grammars.