SU\G(𝔸)/K·U
Sign Up for free Log In

Finiteness and rational sequences, constructively

Authors

Tarmo Uustalu, Niccolò Veltri
Type: Article
Publication Date: 2017-01-01
Citations: 3
DOI: https://doi.org/10.1017/s0956796817000041

Abstract

Abstract Rational sequences are possibly infinite sequences with a finite number of distinct suffixes. In this paper, we present different implementations of rational sequences in Martin–Löf type theory. First, we literally translate the above definition of rational sequence into the language of type theory, i.e., we construct predicates on possibly infinite sequences expressing the finiteness of the set of suffixes. In type theory, there exist several inequivalent notions of finiteness. We consider two of them, listability and Noetherianness, and show that in the implementation of rational sequences the two notions are interchangeable. Then we introduce the type of lists with backpointers, which is an inductive implementation of rational sequences. Lists with backpointers can be unwound into rational sequences, and rational sequences can be truncated into lists with backpointers. As an example, we see how to convert the fractional representation of a rational number into its decimal representation and vice versa.

Locations

  • Journal of Functional Programming
    View

On Rational Recursive Sequences

2022-01-01
Lorenzo Clemente , Maria Donten-Bury , Filip Mazowiecki +1 more
We study the class of rational recursive sequences (ratrec) over the rational numbers. A ratrec sequence is defined via a system of sequences using mutually recursive equations of depth 1, … We study the class of rational recursive sequences (ratrec) over the rational numbers. A ratrec sequence is defined via a system of sequences using mutually recursive equations of depth 1, where the next values are computed as rational functions of the previous values. An alternative class is that of simple ratrec sequences, where one uses a single recursive equation, however of depth k: the next value is defined as a rational function of k previous values. We conjecture that the classes ratrec and simple ratrec coincide. The main contribution of this paper is a proof of a variant of this conjecture where the initial conditions are treated symbolically, using a formal variable per sequence, while the sequences themselves consist of rational functions over those variables. While the initial conjecture does not follow from this variant, we hope that the introduced algebraic techniques may eventually be helpful in resolving the problem. The class ratrec strictly generalises a well-known class of polynomial recursive sequences (polyrec). These are defined like ratrec, but using polynomial functions instead of rational ones. One can observe that if our conjecture is true and effective, then we can improve the complexities of the zeroness and the equivalence problems for polyrec sequences. Currently, the only known upper bound is Ackermanian, which follows from results on polynomial automata. We complement this observation by proving a PSPACE lower bound for both problems for polyrec. Our lower bound construction also implies that the Skolem problem is PSPACE-hard for the polyrec class.
View PDF Chat

Rational and fractional numbers: From quotient fields to recursive understanding.

1993-01-01
Thomas E. Kieren

Revisiting regular sequences in light of rational base numeration systems

2021-03-31
Michel Rigo , Manon Stipulanti
Regular sequences generalize the extensively studied automatic sequences. Let $S$ be an abstract numeration system. When the numeration language $L$ is prefix-closed and regular, a sequence is said to be … Regular sequences generalize the extensively studied automatic sequences. Let $S$ be an abstract numeration system. When the numeration language $L$ is prefix-closed and regular, a sequence is said to be $S$-regular if the module generated by its $S$-kernel is finitely generated. In this paper, we give a new characterization of such sequences in terms of the underlying numeration tree $T(L)$ whose nodes are words of $L$. We may decorate these nodes by the sequence of interest following a breadth-first enumeration. For a prefix-closed regular language $L$, we prove that a sequence is $S$-regular if and only if the tree $T(L)$ decorated by the sequence is linear, i.e., the decoration of a node depends linearly on the decorations of a fixed number of ancestors. Next, we introduce and study regular sequences in a rational base numeration system, whose numeration language is known to be highly non-regular. We motivate and comment our definition that a sequence is $\frac{p}{q}$-regular if the underlying numeration tree decorated by the sequence is linear. We give the first few properties of such sequences, we provide a few examples of them, and we propose a method for guessing $\frac{p}{q}$-regularity. Then we discuss the relationship between $\frac{p}{q}$-automatic sequences and $\frac{p}{q}$-regular sequences. We finally present a graph directed linear representation of a $\frac{p}{q}$-regular sequence. Our study permits us to highlight the places where the regularity of the numeration language plays a predominant role.

Revisiting regular sequences in light of rational base numeration systems

2021-01-01
Michel Rigo , Manon Stipulanti
Regular sequences generalize the extensively studied automatic sequences. Let $S$ be an abstract numeration system. When the numeration language $L$ is prefix-closed and regular, a sequence is said to be … Regular sequences generalize the extensively studied automatic sequences. Let $S$ be an abstract numeration system. When the numeration language $L$ is prefix-closed and regular, a sequence is said to be $S$-regular if the module generated by its $S$-kernel is finitely generated. In this paper, we give a new characterization of such sequences in terms of the underlying numeration tree $T(L)$ whose nodes are words of $L$. We may decorate these nodes by the sequence of interest following a breadth-first enumeration. For a prefix-closed regular language $L$, we prove that a sequence is $S$-regular if and only if the tree $T(L)$ decorated by the sequence is linear, i.e., the decoration of a node depends linearly on the decorations of a fixed number of ancestors. Next, we introduce and study regular sequences in a rational base numeration system, whose numeration language is known to be highly non-regular. We motivate and comment our definition that a sequence is $\frac{p}{q}$-regular if the underlying numeration tree decorated by the sequence is linear. We give the first few properties of such sequences, we provide a few examples of them, and we propose a method for guessing $\frac{p}{q}$-regularity. Then we discuss the relationship between $\frac{p}{q}$-automatic sequences and $\frac{p}{q}$-regular sequences. We finally present a graph directed linear representation of a $\frac{p}{q}$-regular sequence. Our study permits us to highlight the places where the regularity of the numeration language plays a predominant role.
View PDF Chat

From Rational Functions to Regular Languages

2000-01-01
Elena Barcucci , Alberto Del Lungo , Andrea Frosini +1 more

A Range of Numeration Systems

2014-09-12
Michel Rigo

Revisiting regular sequences in light of rational base numeration systems

2021-11-29
Michel Rigo , Manon Stipulanti
View PDF Chat

Datatype defining rewrite systems for the ring of integers, and for natural and integer arithmetic in unary view.

2016-08-22
J.A. Bergstra , Alban Ponse
A datatype defining rewrite system (DDRS) is a ground-complete term rewriting system, intended to be used for the specification of datatypes. As a follow-up of an earlier paper we define … A datatype defining rewrite system (DDRS) is a ground-complete term rewriting system, intended to be used for the specification of datatypes. As a follow-up of an earlier paper we define two concise DDRSes for the ring of integers, each comprising only twelve rewrite rules, and prove their ground-completeness. Then we introduce DDRSes for a concise specification of natural number arithmetic and integer arithmetic in unary view, that is, arithmetic based on unary append (a form of tallying) or on successor function. Finally, we relate one of the DDRSes for the ring of integers to the above-mentioned DDRSes for natural and integer arithmetic in unary view.

Unraveling the gap between natural and rational numbers

2015-01-17
Wim Van Dooren , Erno Lehtinen , Lieven Verschaffel

Rational dependence in finite sets of numbers

1965-01-01
E. G. Straus
View PDF Chat

The Transition from Natural to Rational Number Knowledge

2017-01-01
Jo Van Hoof , Xenia Vamvakoussi , Wim Van Dooren +1 more

Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers

2024-09-29
Karol Pąk , Cezary Kaliszyk
The proper class of Conway's surreal numbers forms a rich totally ordered algebraically closed field with many arithmetic and algebraic properties close to those of real numbers, the ordinals, and … The proper class of Conway's surreal numbers forms a rich totally ordered algebraically closed field with many arithmetic and algebraic properties close to those of real numbers, the ordinals, and infinitesimal numbers. In this paper, we formalize the construction of Conway's numbers in Mizar using two approaches and propose a bridge between them, aiming to combine their advantages for efficient formalization. By replacing transfinite induction-recursion with transfinite induction, we streamline their construction. Additionally, we introduce a method to merge proofs from both approaches using global choice, facilitating formal proof. We demonstrate that surreal numbers form a field, including the square root, and that they encompass subsets such as reals, ordinals, and powers of $\omega$. We combined Conway's work with Ehrlich's generalization to formally prove Conway's Normal Form, paving the way for many formal developments in surreal number theory.
View PDF Chat

Rational functions via recursive schemes

2023-01-01
Siddharth Bhaskar , Jane Chandlee , Adam Jardine
We give a new characterization of the class of rational string functions from formal language theory using order-preserving interpretations with respect to a very weak monadic programming language. This refines … We give a new characterization of the class of rational string functions from formal language theory using order-preserving interpretations with respect to a very weak monadic programming language. This refines the known characterization of rational functions by order-preserving MSO interpretations.

Rational and Fractional Numbers: From Quotient Fields to Recursive Understanding: Thomas E. Kieren

2012-10-12

Constant-length substitutions and countable scrambled sets

2004-09-28
F. Blanchard , Fabien Durand , Alejandro Maass
View PDF Chat

Finite Arithmetic

1998-01-01
John Stillwell

Numbers

2014-10-09
Richard Bird
Numbers in Haskell are complicated because in the Haskell world there are many different kinds of number, including: Numbers in Haskell are complicated because in the Haskell world there are many different kinds of number, including:

Transfinite rationals

1945-01-01
John M. H. Olmsted
View PDF Chat

On inverse Goodstein sequences

2023-01-01
Patrick Uftring
In the late 1980s, Abrusci, Girard and van de Wiele defined a variant of Goodstein sequences: the so-called inverse Goodstein sequence. In their work, they show that it terminates precisely … In the late 1980s, Abrusci, Girard and van de Wiele defined a variant of Goodstein sequences: the so-called inverse Goodstein sequence. In their work, they show that it terminates precisely at the Bachmann-Howard ordinal. This reveals that a proof of this fact requires substantial consistency strength. Moreover, the authors could show that sequences of this kind terminate even if the hereditary base change at the heart of their construction is replaced by a generalization using arbitrary dilators. We show in a weak base system that this more general result is, in fact, equivalent to one of the most famous strong set existence principles from reverse mathematics: $\Pi^1_1$-comprehension. Moreover, the ordinal at which such sequences terminate is, in a fundamental way, isomorphic to the $1$-fixed point of their dilator, a new concept introduced by Freund and Rathjen. This yields explicit notation systems and a general method for specifying such ordinals. Also, using the notation systems provided by $1$-fixed points, we can reproduce the result that the Goodstein sequence terminates at the Bachmann-Howard ordinal in a weak system. Additionally, we perform a similar computation for a variant of Goodstein sequences, which terminates at a predicative ordinal.
View PDF Chat

Predicatively unprovable termination of the Ackermannian Goodstein process

2019-10-30
Toshiyasu Arai , David Fernández‐Duque , Stanley S. Wainer +1 more
The classical Goodstein process gives rise to long but finite sequences of natural numbers whose termination is not provable in Peano arithmetic. In this manuscript we consider a variant based … The classical Goodstein process gives rise to long but finite sequences of natural numbers whose termination is not provable in Peano arithmetic. In this manuscript we consider a variant based on the Ackermann function. We show that Ackermannian Goodstein sequences eventually terminate, but this fact is not provable using predicative means.
View PDF Chat

Finite sets in homotopy type theory

2018-01-08
Dan Frumin , Herman Geuvers , Léon Gondelman +1 more
We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. … We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. We use higher inductive types to define the type K(A) of "finite sets over type A" à la Kuratowski without assuming that K(A) has decidable equality. We show how to define basic functions and prove basic properties after which we give two applications of our definition.
View PDF Chat

Finite sets in homotopy type theory

2017-12-22
Dan Frumin , Herman Geuvers , Léon Gondelman +1 more
We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. … We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. We use higher inductive types to define the type K(A) of "finite sets over type A" à la Kuratowski without assuming that K(A) has decidable equality. We show how to define basic functions and prove basic properties after which we give two applications of our definition.
View PDF Chat

Foundations of regular coinduction

2021-10-01
Francesco Dagnino
Inference systems are a widespread framework used to define possibly recursive predicates by means of inference rules. They allow both inductive and coinductive interpretations that are fairly well-studied. In this … Inference systems are a widespread framework used to define possibly recursive predicates by means of inference rules. They allow both inductive and coinductive interpretations that are fairly well-studied. In this paper, we consider a middle way interpretation, called regular, which combines advantages of both approaches: it allows non-well-founded reasoning while being finite. We show that the natural proof-theoretic definition of the regular interpretation, based on regular trees, coincides with a rational fixed point. Then, we provide an equivalent inductive characterization, which leads to an algorithm which looks for a regular derivation of a judgment. Relying on these results, we define proof techniques for regular reasoning: the regular coinduction principle, to prove completeness, and an inductive technique to prove soundness, based on the inductive characterization of the regular interpretation. Finally, we show the regular approach can be smoothly extended to inference systems with corules, a recently introduced, generalised framework, which allows one to refine the coinductive interpretation, proving that also this flexible regular interpretation admits an equivalent inductive characterisation.
View PDF Chat

Free iterative theories: a coalgebraic view

2003-04-01
Ji � Ad�mek , Stefan Milius , J. Velebil
Every finitary endofunctor of $\Set$ is proved to generate a free iterative theory in the sense of Elgot. This work is based on coalgebras, specifically on parametric corecursion, and the … Every finitary endofunctor of $\Set$ is proved to generate a free iterative theory in the sense of Elgot. This work is based on coalgebras, specifically on parametric corecursion, and the proof is presented for categories more general than just $\Set$.

On streams that are finitely red

2012-10-10
Marc Bezem , Keiko Nakata , Tarmo Uustalu
Mixing induction and coinduction, we study alternative definitions of streams being finitely red. We organize our definitions into a hierarchy including also some well-known alternatives in intuitionistic analysis. The hierarchy … Mixing induction and coinduction, we study alternative definitions of streams being finitely red. We organize our definitions into a hierarchy including also some well-known alternatives in intuitionistic analysis. The hierarchy collapses classically, but is intuitionistically of strictly decreasing strength. We characterize the differences in strength in a precise way by weak instances of the Law of Excluded Middle.
View PDF Chat