Mikołaj Bojańczyk

Przekształcenia automatowe • Transducers


This is the page for a transducer course, given at the University of Warsaw in 2024.

The tutorials are by Aliaume Lopez, you can find the problems here.

Grading

Your grade is based on points.

  • 5 points for each of the two homeworks
  • 1 point for learning the theory in each of the 13 lectures, tested at the oral exam
  • bonus points for star exercises

Therefore, if we ignore the star exercises, you can get 23 points. Since there is a lot of material, you do not need to get all points. Here are the thresholds for the various grades (see also the additional condition below):

  • 3: 9 points
  • 3+: 10 points
  • 4: 11 points
  • 4+: 13 points
  • 5: 15 points

Additional condition: regardless of the number of points you have, in order to pass you need to know at least 6 lectures for your oral exam.

Oral exam.

At the oral exam, you declare which of the lectures you have learned (but at least 6, as per the additional condition), and you will be asked some (not necessarily all) exam questions for your declared lectures. You can approach the oral exam as many times as you wish, but I will get annoyed if I have the feeling that you are abusing this (this does not happen in my experience). You can schedule the exam as you wish (up to July 5), but I would prefer if you used two either June 25 or July 2 for your first attempt; sign up here.

If you want a second attempt (sesja poprawkowa), then the homeworks will no longer count, but the lectures will be worth 1.5 points instead of 1.


Lectures

1. Mealy machines

Slides

  • Definition of Mealy machines
  • Closure under composition
  • The Krohn-Rhodes Theorem

Exam questions:

  • Define Mealy machines, and show that they are closed under composition
  • Prove the Krohn-Rhodes Theorem about Mealy machines

2. Rational functions

Slides

  • Unambiguous nondeterministic automata with output
  • Eilenberg Bi-machines
  • Their equivalence
  • A Krohn-Rhodes decomposition
  • Deciding equivalence

Exam questions:

  • Prove the equivalence between bi-mcahines and unambiguous nondeterministic automata with output
  • Prove the Krohn-Rhodes Theorem for this model (which is called rational functions)
  • Show that equivalence is decidable for rational functions

3. Enter logic

Slides

  • MSO = regular languages
  • MSO relabelings = letter-to-letter rational
  • the first-order fragment of MSO

Exam questions:

  • Prove that MSO=regular languages
  • Prove that a language is first-order definable if and only if it is recognised by a counter-free automaton

4. Two-way automata

Slides

  • Two-way automata with output (2DFA)
  • Closure under pre-composition
  • Decidable equivalence

Exam questions:

  • Warm-up: prove that 2DFA  are continuous
  • Prove that 2DFA are closed under composition
  • Prove that equivalence is decidable for 2DFA

5. MSO transductions

Slides

  • Definition of MSO transductions
  • Equivalence with previous two models

Exam questions:

  • Show that MSO transductions are closed under composition
  • Prove MSO transductions are the same as 2DFA

6. Streaming stream transducers

Slides

  • Definition of copy less streaming stream transducers (SST)
  • Equivalence with two-way automata with output

Exam questions:

  • Show that SST are the same as 2DFA = MSO transductions

7. List functions

Slides

  • Definition of the linear list functions
  • Their first-order fragment
  • Proof that they define the same functions as two-way transducers
  • Krohn-Rhodes decomposition for linear regular functions

Exam questions:

  • Define the linear list functions, and show that they are equivalent to 2DFA

8. Introduction to polyregular functions

Slides

  • Polynomial Krohn-Rhodes primes
  • Polynomial list functions
  • For-transducers
  • Equivalence of all three models

Exam questions:

  • Define the polynomial Krohn-Rhodes primes, and show that they are continuous
  • Define the polynomial list functions, and show how split and reverse are redundant
  • Define for-transducers, and show that each one can be converted into prenex normal form (all loops on the outside)
  • Prove (Krohn-Rhodes primes)* ⊆ polynomial list functions
  • Prove polynomial list functions ⊆ for-transducers
  • Prove for-transducers ⊆ (Krohn-Rhodes primes)*

9. Pebble transducers

Slides

  • Pebble transducers
  • Their equivalence to the polynomial list functions and for transducers

Exam questions:

  • Prove pebble ⊆ polynomial list functions

10. A functional programming language

Slides

  • Polynomial list functions with λ

Exam questions:

  • Define the syntax and semantics of the λ-calculus extension of polynomial list functions
  • What is β-reduction on λ-terms, and what are normal forms
  • Show that one step of β-reduction can be implemented by a for-transducer.

11. Polynomial interpretations 1

Slides

  • First-order interpretations on general structures
  • Difficulties with MSO interpretations

Exam questions:

  • Define first-order interpretations, and prove that they are closed under composition
  • Define MSO interpretations, and prove that they need not be closed under compositions

12. Polynomial interpretations 2

Slides

  • The Simon Theorem on factorizations
  • Using it to for quantifier elimination

Exam questions:

  • Prove the Simon Theorem
  • Prove quantifier elimination for MSO interpretations

13. Polynomial interpretations 3

Slides

  • Quantifier-free interpretations are polyregular

Exam questions:

  • Show that every quantifier-free interpretation, of tree-to-string type, is polyregular

 


Research projects

Here is a list of open problems about polyregular functions.