Arithmetical Datatypes, Fracterms, and the Fraction Definition Problem

Datatypes and abstract datatypes are positioned as results of importing aspects of universal algebra into computer science and software engineering. It is suggested that 50 years later, by way of a transfer in the opposite direction, outcomes of research on datatypes can be made available via elementary arithmetic. This idea leads to the notions of an arithmetical signature, an arithmetical datatype and an arithmetical abstract datatype and to algebraic specifications for such entities. The area of fractions in elementary arithmetic is chosen as an application area and while taking a common meadow of rational numbers as the basis, an arithmetical datatype equipped with an absorptive element. The use of datatypes and signatures makes syntax available for giving precise definitions in cases where lack of precision is common place. Fracterm is coined as the name for a fraction when primarily understood as a syntactic entity. The main contribution of the paper is to provide a detailed terminology of fracterms. Subsequently the fraction definition problem is stated, a distinction between explicit definitions of fractions and implicit definitions of fractions is made, and an outline of a survey of both forms of definitions of the notion of a fraction is given.

Formalization of Cognitive Modeling of Environment for Wayfinding

This paper outlines the formal representation of the environment in which it is assumed that a wayfinding process has been occurred through a street network. Wayfinding is a process in which people navigate themselves from an origin to a destination by their common sense geospatial knowledge. Naïve Geography is a field of study that investigates the body of knowledge that people have about the surrounding geospatial world and it deals with common sense knowledge of space. The image schemas which are needed for wayfinding with boundary relations method have been extracted and represented formally with algebraic specifications. These specifications are mentioned in the syntax of a functional programming language, Haskell. It allows us to execute written algebraic specifications and provide conditions for rapid prototyping and formal checks on consistency. These formal specifications are implemented for modeling street network of a part of Tehran, Capital city of Iran.

Bisimulation proof methods in a path-based specification language for polynomial coalgebras

What reasoning rules can be used for the deduction of bisimulation formulas in coalgebraic specifications is problematic because those rules used in algebraic specifications possibly cannot be applied to bisimulation formulas. Although some categorical bisimulation proof methods for coalgebras have been proposed, they are not based on specification languages of coalgebras so that they cannot be used as reasoning rules. In this paper, a specification language based on paths of polynomial functors is proposed to specify polynomial coalgebras. Paths of polynomial functors give detailed observations and transitions on the state space of coalgebras so that the techniques used in transition system specifications can be applied to such a path-based language. In particular, because bisimulations can be characterized by paths, the notions of progressions, respectful functions and faithful contexts can be defined based on paths, and then bisimulation up-to proof techniques, including bisimulation up-to bisimilarities and up-to contexts for transition systems can be transformed into reasoning rules in the language. Several examples illustrate how to reason syntactically about bisimulations in the language by using the rules induced by the bisimulation proof techniques.