Sturmian words are infinite words that have exactly n+1 factors of length n for every positive integer n. A Sturmian word sα,p is also defined as a coding over a two-letter alphabet of the orbit of point ρ under the action of the irrational rotation Rα : x → x + α (mod 1). A substitution fixes a Sturmian word if and only if it is invertible. The main object of the present paper is to investigate Rauzy fractals associated with two-letter invertible substitutions. As an application, we give an alternative geometric proof of Yasutomi's characterization of all pairs (α,p) such that sα,p is a fixed point of some non-trivial substitution.

The specification of the data structures used in EAT, a software system for symbolic computation in algebraic topology, is based on an operation that defines a link among different specification frameworks like hidden algebras and coalgebras. In this paper, this operation is extended using the notion of institution, giving rise to three institution encodings. These morphisms define a commutative diagram which shows three possible views of the same construction, placing it in an equational algebraic institution, in a hidden institution or in a coalgebraic institution. Moreover, these morphisms can be used to obtain a new description of the final objects of the categories of algebras in these frameworks, which are suitable abstract models for the EAT data structures. Thus, our main contribution is a formalization allowing us to encode a family of data structures by means of a single algebra (which can be described as a coproduct on the image of the institution morphisms). With this aim, new particular definitions of hidden and coalgebraic institutions are presented.

We explicit the link between the computer arithmetic problem of providing correctly rounded algebraic functions and some diophantine approximation issues. This allows to get bounds on the accuracy with which intermediate calculations must be performed to correctly round these functions.

For finitary set functors preserving inverse images, recursive coalgebras A of Paul Taylor are proved to be precisely those for which the system described by A always halts in finitely many steps.

This article is a case study in the implementation of a portable, proven and efficient correctly rounded elementary function in double-precision. We describe the methodology used to achieve these goals in the crlibm library. There are two novel aspects to this approach. The first is the proof framework, and in general the techniques used to balance performance and provability. The second is the introduction of processor-specific optimization to get performance equivalent to the best current mathematical libraries, while trying to minimize the proof work. The implementation of the natural logarithm is detailed to illustrate these questions.

Suppose ƒ : X* → X* is a morphism and u,v ∈ X*. For every nonnegative integer n, let zn be the longest common prefix of ƒn(u) and ƒn(v), and let un,vn ∈ X* be words such that ƒn(u) = znun and ƒn(v) = znvn. We prove that there is a positive integer q such that for any positive integer p, the prefixes of un (resp. vn) of length p form an ultimately periodic sequence having period q. Further, there is a value of q which works for all words u,v ∈ X*.

Numerical integration is an important operation for scientific computations. Although the different quadrature methods have been well studied from a mathematical point of view, the analysis of the actual error when performing the quadrature on a computer is often neglected. This step is however required for certified arithmetics.
We study the Newton-Cotes quadrature scheme in the context of multiple-precision arithmetic and give enough details on the algorithms and the error bounds to enable software developers to write a Newton-Cotes quadrature with bounded error.

Various static analyses of functional programming languages that permit infinite data structures make use of set constants like Top, Inf, and Bot, denoting all terms, all lists not eventually ending in Nil, and all non-terminating programs, respectively. We use a set language that permits union, constructors and recursive definition of set constants with a greatest fixpoint semantics in the set of all, also infinite, computable trees, where all term constructors are non-strict. This paper proves decidability, in particular DEXPTIME-completeness, of inclusion of co-inductively defined sets by using algorithms and results from tree automata and set constraints. The test for set inclusion is required by certain strictness analysis algorithms in lazy functional programming languages and could also be the basis for further set-based analyses.