Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Synthesis of Computable Regular Functions of Infinite Words

V. Dave, E. Filiot, S. Krishna, N. Lhote

TL;DR

This paper proposes a decision procedure for the following synthesis problem: given a regular function f, is f computable and if it is, synthesize a Turing machine computing it and effectively characterise uniform continuity of regular functions, and relates it to the notion of uniform computability, which offers stronger efficiency guarantees.

Abstract

Regular functions from infinite words to infinite words can be equivalently specified by MSO-transducers, streaming $ω$-string transducers as well as deterministic two-way transducers with look-ahead. In their one-way restriction, the latter transducers define the class of rational functions. Even though regular functions are robustly characterised by several finite-state devices, even the subclass of rational functions may contain functions which are not computable (by a Turing machine with infinite input). This paper proposes a decision procedure for the following synthesis problem: given a regular function $f$ (equivalently specified by one of the aforementioned transducer model), is $f$ computable and if it is, synthesize a Turing machine computing it. For regular functions, we show that computability is equivalent to continuity, and therefore the problem boils down to deciding continuity. We establish a generic characterisation of continuity for functions preserving regular languages under inverse image (such as regular functions). We exploit this characterisation to show the decidability of continuity (and hence computability) of rational and regular functions. For rational functions, we show that this can be done in $\mathsf{NLogSpace}$ (it was already known to be in $\mathsf{PTime}$ by Prieur). In a similar fashion, we also effectively characterise uniform continuity of regular functions, and relate it to the notion of uniform computability, which offers stronger efficiency guarantees.

Synthesis of Computable Regular Functions of Infinite Words

TL;DR

This paper proposes a decision procedure for the following synthesis problem: given a regular function f, is f computable and if it is, synthesize a Turing machine computing it and effectively characterise uniform continuity of regular functions, and relates it to the notion of uniform computability, which offers stronger efficiency guarantees.

Abstract

Regular functions from infinite words to infinite words can be equivalently specified by MSO-transducers, streaming -string transducers as well as deterministic two-way transducers with look-ahead. In their one-way restriction, the latter transducers define the class of rational functions. Even though regular functions are robustly characterised by several finite-state devices, even the subclass of rational functions may contain functions which are not computable (by a Turing machine with infinite input). This paper proposes a decision procedure for the following synthesis problem: given a regular function (equivalently specified by one of the aforementioned transducer model), is computable and if it is, synthesize a Turing machine computing it. For regular functions, we show that computability is equivalent to continuity, and therefore the problem boils down to deciding continuity. We establish a generic characterisation of continuity for functions preserving regular languages under inverse image (such as regular functions). We exploit this characterisation to show the decidability of continuity (and hence computability) of rational and regular functions. For rational functions, we show that this can be done in (it was already known to be in by Prieur). In a similar fashion, we also effectively characterise uniform continuity of regular functions, and relate it to the notion of uniform computability, which offers stronger efficiency guarantees.

Paper Structure

This paper contains 27 sections, 16 theorems, 5 equations, 3 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Computability of functions over infinite words
  3. Examples
  4. Computability and continuity
  5. Beyond synchronous functions: regular functions
  6. Contributions
  7. Related work
  8. Changes from the conference version
  9. Languages, Automata and Transducers over $\omega$-Words
  10. Transducers
  11. Computability versus Continuity
  12. A Characterisation of Continuity and Uniform Continuity
  13. Topology preliminaries
  14. Deciding Continuity and Uniform Continuity
  15. Rational case
  16. ...and 12 more sections

Key Result

Theorem 2.1

A function $f\colon\Sigma^\omega\rightarrow \Gamma^\omega$ is regular if and only if it is 2DFTpla definable.

Figures (3)

  • Figure 1: A 2DFTpla with automaton on the right implementing the look-ahead.
  • Figure 2: Pattern characterising non-continuity of rational functions given by trim one-way Büchi transducers.
  • Figure 3: Pattern characterising non-uniform continuity of rational functions given by trim one-way Büchi transducers.

Theorems & Definitions (38)

  • Theorem 2.1
  • Example 2.2
  • Definition 3.1: Computability/Uniform computability
  • Definition 3.2: Continuity/Uniform continuity
  • Example 3.3
  • Theorem 3.4
  • proof
  • Remark 3.5
  • Proposition 4.1
  • proof
  • ...and 28 more