Advanced Formal Language Theory, Spring 2025
ETH Zürich: Course catalog
Course Description
This course explores the connection between automata and formal logic. The lectures cover the algebraic characterization of the regular languages definable in many different logical theories, the complexity theory of boolean circuits, and the connection between the two. The interest in these topics has been recently rekindled due to their application in modern-day natural language processing. Both formal logic and circuit complexity are being used extensively to study the expressivity of transformers.
The emphasis is on rigor and depth rather than broad coverage. Students should expect a healthy dose of proof-writing and, thus, mathematical maturity is expected. In terms of background, the class will draw on techniques from discrete math, formal logic, automata theory and abstract algebra. While there are no hard prerequisites, having taken a class that covers these topics would be helpful.
The course is structured around the book Finite Automata, Formal Logic, and Circuit Complexity and the lectures are meant to guide you through the most important bits. The homework exercises, which comprise 100% of the grade, will require you to apply or extend the theory taught in class. The homework will be released throughout the semester in assignments with 3–4 questions each.
News
17.2. Class website is online!
17.2. The exercise session on 20.2. will not take place!
Syllabus and Schedule
On the Use of Class Time
Lectures
There are two slots for AFLT each week: Wednesdays 16:15-18:00 (HG D 5.2) and Thursdays 12:15-14:00 (ML F 39). The Wednesday slot will be used as lecture, in which we will generally cover new material. The Thursday slot will be an exercise session, in which we will walk through some exercises, recap concepts taught in the previous lectures, answer questions, or discuss in more detail the theory already taught. The lecture and the exercise session will generally be given in person and live broadcast on Zoom.
Lectures and exercise sessions will be recorded—link to the Zoom recordings will be posted on the course Moodle page.
We also regularly publish Ryan’s iPad class notes.
Note: This is the first time we are teaching this version of the course, so the syllabus and the course structure might change. Please check the website and Rocketchat regularly for announcements!
Tutorials
The Thursday slot will be used as an exercise session, in which we will solve together exercises similar to those from the assignments. You can use the tutorial session to ask questions about previously taught concepts. Additionally, the teaching staff will be available for questions on the course chat channels (see below).
Syllabus
Date | Topic | Reading | Materials |
---|---|---|---|
19. 2. 2025 | Course Logistics | Introductory Slides | |
19. 2. 2025 | Preliminaries, Automata, Regular Languages | Sections I.1, I.2 | |
26. 2. 2025 | Semigroups, Homomorphisms, Formal Logic | Sections I.3, Chapter II | |
05. 3. 2025 | Monadic Second-order Logic and Regular Languages | Chapter III | |
12. 3. 2025 | Model-theoretic Games, FO[<] and FO[+1] | Chapter IV | |
19. 3. 2025 | The Syntactic Monoid | Chapter V | |
26. 3. 2025 | First-Order Logic | Sections VI.1, VI.2 | |
2. 4. 2025 | The Hierarchy in FO | Sections VI.3, VI.4 | |
9. 4. 2025 | Modular Quantifiers | Chapter VII | |
16. 4. 2025 | Circuit Complexity, Circuit Complexity Classes | Sections VIII.1, VIII.2 | |
23. 4. 2025 | No class (Easter break) | ||
30. 4. 2025 | Circuit Complexity, Circuit Complexity Classes | Sections VIII.2, VIII.3 | |
7. 5. 2025 | Regular Languages and Circuit Complexity | Sections IX.1, IX.2 | |
14. 5. 2025 | Regular Languages and Circuit Complexity | Sections IX.3, IX.4 | |
21. 5. 2025 | The Krohn-Rhodes Theorem | Appendix A | |
28. 5. 2025 | Buffer/Recap |
Organisation
Live Chat
In addition to class time, there will also be a RocketChat
-based live chat hosted on ETH’s servers.
Students are free to ask questions of the teaching team and of others in public or private (direct message).
There are specific channels for each assignment as well as for asking general content questions and for announcements.
All data from the chat will be deleted from ETH servers at the course’s conclusion.
Important: There are a few important points you should keep in mind about the course live chat:
RocketChat
will be the main communications hub for the course. You are responsible for receiving all messages broadcast in theRocketChat
.- Your username should be
firstname.lastname
. This is required as we will only allow enrolled students to participate in the chat and we will remove users which we cannot validate. - Tag your questions as described in the document on How to use Rycolab Course RocketChat channels. The document also contains other general remarks about the use of
RocketChat
. - Search for answers in the appropriate channels before posting a new question.
- Ask questions on public channels as much as possible.
- Answer to posts in threads.
- The chat supports
LaTeX
for easier discussion of technical material. See How to useLaTeX
inRocketChat
. - We highly recommend you download the desktop app here.
This is the link to the main channel.
To make the moderation of the chat more easily manageable, we have created a number of other channels on RocketChat
.
The full list is:
- AFLT Main Channel for the general organisational discussions.
- AFLT Announcements Channel for the announcements by the teaching team.
- AFLT Content Questions for your questions about the content of the course.
Important: Please prepend your question with a “tag” about the content of your question in square brackets.
For example, if your question is about the content of Lecture 1 and specifically about the definition of a semigroup, please start your message with
[Lecture #1, Definition of a Semigroup]
. - AFLT Assignment 1 for discussing and asking questions about Assignment 1.
- AFLT Assignment 2 for discussing and asking questions about Assignment 2.
- AFLT Assignment 3 for discussing and asking questions about Assignment 3.
- AFLT Assignment 4 for discussing and asking questions about Assignment 4.
- AFLT Assignment 5 for discussing and asking questions about Assignment 5.
If you feel like you would benefit from any other channel, feel free to suggest it to the teaching team!
Grading
There will be no final exam for this course. Instead, we will release 5 assignments throughout the semester. You can cooperate on and discuss the assignments with your peers, but you must write up the solutions yourself.
Important: The deadline for the assignment submission will be shortly before the Summer examination period (1. 8. 2024).
The submissions will be done through the course Moodle page.
Keep in mind that due to how late in the semester the deadline is, we cannot extend it—we are counting on you to be organised and submit the work in time.
We require the solutions to be properly typeset.
We recommend using LaTeX
(with Overleaf
), but markdown
files with MathJax
for the mathematical expressions are also fine.
Assignments
Below you can find the assignment instructions.
Assignment instructions:
- Assignment 1
- Assignment 2
- Assignment 3
- Assignment 4
- Assignment 5
Contact
You can ask questions on the course chat server. Please post all content-related questions there, so others can see them and join the discussion. If you have questions which are not related to the course material and are not of general interest, please don’t hesitate to contact us directly, i.e., email Ryan with the TAs cc-ed.