ABSTRACT: Proper fork algebras are algebras of binary relations over a structured set. The underlying set has changed from set of pairs to set closed under an injective fuction. In this paper we present a representation theorem for their abstract counterpart, that entails that proper fork algebras - whose underlying set is closed under an injective function - constitute a finitely based variety
ABSTRACT: A simple extension of Tarski’s calculus of binary relations is shown to have the expressive power of first-order logic. In contrast with Cylindric and Polyadic algebras, this extension introduces only finitely many operations and constants whose standard meaning is finitary.
ABSTRACT: We examine some alternative characterisations for fork algebras and their relational reducts. These alternative characterisations come from the consideration of special (pairs of) elements in relational algebras. Their adequacy comes from an analysis of the proof of representability, where it was implicit, as well as from properties of these special pairs of elements. This approach provides interesting insights and leads to (equational) presentations with convenient structures.
ABSTRACT: Fork algebras are extensions of relation algebras by a new binary operator, fork. This extension is motivated by programming needs [5], as a tool for reasoning about program behavior [6]. Their expressiveness was established in [11]: in any proper fork algebra (a standard model) every binary relation that is first-order definable is also denoted by a fork term. This shows that the expressive power of proper fork algebras encompasses that of first-order logic with equality. Here we complement this result by a representation theorem: every atomic abstract fork algebra is isomorphic to a proper one.
ABSTRACT: Fork algebras have interesting connections with Computing, Algebra and Logic. This paper presents a survey of ideas and results about fork algebras, with special emphasis on current developments and promising research lines.
ABSTRACT: We examine the set-theoretical nature of fork algebras, namely to what extent fork algebras of relations are really set-based. We show that every fork algebra of relations (FAR, for short) can be represented by a cartesian FAR by making use of the room provided by the neutral element I for relational composition. If one insists in taking I as the concrete identity (diagonal) relation, then such representation is not always possible: we show that there are many interesting FARs that cannot be represented by proper cartesian FARs.
ABSTRACT: A fork algebra is a relational algebra enriched with a binary operation, called fork, where the projections can be defined by terms. Fork algebras can be axiomatised by equations giving properties of the fork operation and the projections. We examine the interplay between these equations and obtain eight independent equational axiomatisations for fork algebras with orientation ranging from fork to projections.
ABSTRACT: We establish the independence of the fork axioms by examining their role and presenting expansions of (simple) algebras of relations that falsify each one of these fork equations while satisfying the other axioms. We aslo examine these algebras to obtain further information about the independence of these axioms.
ABSTRACT: We introduce and examine a tool for analysing logics. This algebraic tool, coming from some ideas introduced by J. Piaget, provides condensed information about a logic (with emphasis on the behavior of a unary symbol), as such, it can be employed for analysing and, to some extent, comparing logics. Keywords: Logic, interpretation, transformations, groups, monoids, homomorphism.
ABSTRACT: Logical, algebraic, programming language, grammatical and denotational formalisms are investigated with respect to their applicability to formal data base specification. On applying each formalism for the purpose that originally motivated its proposal, it is shown that they all have a fundamental and well integrated role to play in different parts of the specification process. An example is included to illustrate the methodoldgical aspects.
ABSTRACT: Formalisms based on graph transformations are used to specify data base applications. Starting from an informal description, two formal specifications - one queryoriented and the other update-oriented - are successively derived.
ABSTRACT: A methodology for the formalspecification of database applications is presented . Central to the methodology is the idea of proceeding through successive levels of "traces", which enables an initial algebra specification to be obtained from one based on preconditions and effects . Besides being executable these trace levels provide a way to go from a natural language specification to an algebraic one .
ABSTRACT: We examine some variants of modularity (preservation of faithfulness) by localizing them to a commutative diagram in a PI-institution. We address, by means of an algebraic approach, the question of when a specification is modular for a given pair of specifications. Motivated by design considerations, we extend this notion to families, which leads to simpler variants, with decoupled connections. 2001 Elsevier Science B.V. All rights reserved. Keywords: Formal specifications; Data types; Interpretations; Institution; Modularity; Families of specifications; Software engineering; Specification languages; Theory of computation
ABSTRACT: We generalise and clarify connections between variants of modularity (preservation of faithfulness) and interpolation by localising them to a diagram in an entailment system. The variants of modularity arise naturally from the idea of building specifications in steps. We establish, by an algebraic approach, connections between these variants and (the existence of) versions of interpolating specifications. We also extend these correspondences to specification and interpolating families, and clarify the role of pushout diagrams in this context. 2001 Elsevier Science B.V. All rights reserved. Keywords: Formal specifications; Modularity; Interpolation; Institution; Software engineering
ABSTRACT: Implementation of formal specifications is very important in formal software development and can be described in terms of simple logical concepts. Formal specifications are presentations of theories in many-sorted first-order logic, and an implementation of a formal specification on another formal specification amounts to an interpretation of the former into a conservative extension of the latter. Here we present and analyse some sort introducing constructs akin to those found in many programming languages. This is of importance because it occurs often in implementing formal specifications, when new sorts are 'constructed' from the concrete ones. We specify these constructs and show that these specifications provide extensions with behaviour close to that of the familiar extensions by definitions. Keywords: abstract data types, formal specifications, parameterised specifications, formal program development, implementation, sort constructs
ABSTRACT: Conservativeness is an important property of extensions. Its model-theoretic conterpart, expansiveness, provides a useful sufficient condition for conservativeness, but they are not equivalent, even under very severe restrictions. This paper examines the causes of this phenomenon, emphasizing extensions by constatns. Some simpler characteriztions for conservativeness are provided and finite conservative extensions are shown to be equivalent to Skolem extensions
ABSTRACT: Some methods for introducing new operations into logical specifications are examined, with emphasis on criteria for conservativeness, and compared with respect to their relative power. The motivation comes mainly from software development, especially methods using abstract data types, whose specifications and implementations can be dealt with in terms of theory presentations. Some of these methods are traditional in logic whereas others originate in program development. Criteria for the conservativeness of extensions produced by each method are established, and these methods are shown to fall into three classes with respect to their relative powers. Applications to program development by stepwise refinement are considered.
ABSTRACT: This paper analyzes the theory of area developed by Euclid in the Elements and its modern reinterpretation in Hilbert’s influential monograph Foundations of Geometry. Particular attention is bestowed upon the role that two specific principles play in these theories, namely the famous common notion 5 and the geometrical proposition known as De Zolt’s postulate. On the one hand, we argue that an adequate elucidation of how these two principles are conceptually related in the theories of Euclid and Hilbert is highly relevant for a better understanding of the respective geometrical practices. On the other hand, we claim that these conceptual relations unveil interesting issues between the two main contemporary approaches to the study of area of plane rectilinear figures, i.e., the geometrical approach consisting in the geometrical theory of equivalence and the metrical approach based on the notion of measure of area. Finally, in an appendix logical relations among equivalence, comparison and addition of magnitudes are examined schematically in an abstract setting.
ABSTRACT: A theory of magnitudes involves criteria for their equivalence, comparison and addition. In this article we examine these aspects from an abstract viewpoint, by focusing on the socalled De Zolt’s postulate in the theory of equivalence of plane polygons (“If a polygon is divided into polygonal parts in any given way, then the union of all but one of these parts is not equivalent to the given polygon”). We formulate an abstract version of this postulate and derive it from some selected principles for magnitudes. We also formulate and derive an abstract version of Euclid’s Common Notion 5 (“The whole is greater than the part”), and analyze its logical relation to the former proposition. These results prove to be relevant for the clarification of some key conceptual aspects of Hilbert’s proof of De Zolt’s postulate, in his classical Foundations of Geometry (1899). Furthermore, our abstract treatment of this central proposition provides interesting insights for the development of a well-behaved theory of compatible magnitudes.
ABSTRACT: Abstract: Finiteness is regarded a rather intuitive concept. There are no reports of problems or paradoxes directly related to it. On the other hand, infinity, its negation, has always been a source of inspiration for paradoxes and conceptual problems. Only in the mid-nineteenth century is that we had know the first precise definitions both of one and the other. Proposals for other definitions of these concepts continue to emerge until the early twentieth century. Among the definitions of one or another concept, it is worth mentioning those due to Peano, Dedekind Tarksi and Kolmogorov. It is known that even in ZFC (Zermelo-Fraenkel with Axiom of Choice) these definitions are equivalent. However, they are not equivalent in constructive / intuitionists theories. This can be partially explained by the use of non-classical negation, but there are models where even with a classical base, such concepts are not equivalent. To undertake a conceptual analysis of these cases, we try to consider them in the framework of Category Theory, more precisely Topos Theory. At the risk of not being much faithful to the development of this theory, we analyze Topos Theory as related to Set Theory, by a process known as categorification. Key words: Finiteness; Categorification; Category Theory; Topos Theory.
ABSTRACT: Abstract. A theory of magnitudes involves criteria for their comparison, equivalence and addition. We examine these aspects from an abstract viewpoint, stressing independence and definability. These considerations are triggered by the so-called De Zolt’s principle in the theory of equivalence of plane polygons. Keywords: Theory of magnitudes • comparison • equivalence • addition • independence • definability • geometry • De Zolt’s principle
ABSTRACT: A lógica não contém teoremas puramente existenciais: as únicas sentenças existenciais válidas são aquelas com análogas universais válidas. Aqui, mostramos que isto realmente é assim quando corretamente interpretado: toda validade ex- istencial possui uma análoga universal simples, que também é válida. Também caracterizamos validades universais e existenciais em termos de tautologias. palavras-chave Lógica; quantificação; validades existenciais; validades universais; tautologias
ABSTRACT: In this paper, we introduce a formalism to specify interactive storytelling genres in the context of digital entertainment, adopting an information systems approach. We view a genre as a set of plots, where a plot is a partially ordered sequence of events, taken from a fixed repertoire. In general, the specification of a genre should allow to determine whether a plot is a legitimate representative of the genre, and also to generate all plots belonging to the genre. The formalism divides the specification of a genre into static, dynamic and behavioral schemas, that reflect a plan recognition/plan generation paradigm. It leads to executable specifications, supported by LOGTELL, a prototype tool that helps users generate, modify and reuse plots that follow a genre specification. To illustrate the use of the formalism, we specify a simple Swords & Dragons genre and show plots generated by the tool.
ABSTRACT: The Knight of the Cart is far from being a straightforward knightly adventure. In this essay, we propose to uncover its underlying folktale structure, which in turn leads to a comparison with a tale in the same generic class, having an analogous subject matter (matiere) but opposite orientation (san) - the Indian epic Ramayana.
ABSTRACT: The mathematical notion of function exponentiation is used to introduce an iteration construct suitable to applicative languages. The elements of the construct are explained as well as its evaluation. A prototype Prolog implementation is included to illustrate the discussion.
ABSTRACT: Logics for 'generally' are intended to express some vague notions as 'generally', 'several', 'many', 'most', etc., by means of the new generalized quantifier \nabla and to reason about assertions with 'generally'(important issues in qualitative reasoning). We introduce the idea of functional interpretation for 'generally' and show that representative functions (akin to Skolem functions) enable elimination of \nabla and reduce consequence to classical theories. Thus, one can use proof procedures and theorem provers for classical first-order logic to reason about assertions involving 'generally'.
ABSTRACT: A new, simpler proof, based on intenialisation of interpretations , of the Modularisation Theorem for logical specifications (presentations of first-order theories) is presented. This result is a basic tool for composing implementation* and specialisation by parameter instantiation.
ABSTRACT: When working with an abstract data type it is often convenient to have the ability to execute its operations before a final implementation is available. Here we propose, a procedural formalism, which is based on cangnical forms and amounts to an implementation of the data type by a data type of terms. It is close enough to the algebraic specification, from which it can be easily derived. Its simple translation into some string manipulation language (here SNOBOL) provides executable versions of the operations.
ABSTRACT: A data type is often given by an informal model. Its formal specification is an important task, but also difficult and error-prone. Here a methodology for this task is presented. Its steps are, first, the election of a canonical form defining a canonical term algebra; second, a system of sound rewriting rules powerful enough to achieve the syntactical transformations of the canonical term algebra. The final translation of rewriting rules into equations is immediate. The methodology is illustrated by the detailed presentation of a simple example. KEY WORDS: Abstract data types; formal specification; canonical terms; rewriting systems; specification methodology.
ABSTRACT: A simple technique is presented for verifying that two abstract data type specifications are equivalent in that they have isomorphic initial algebras. The method uses normal forms to attempt reducing the number of equations to be checked. It is applied to a simple example and some extensions, and related problems are also discussed. KEY WORDS: Abstract data type; formal specific