Authors Filippo Bonchi and Damien Pous discuss "Hacking Nondeterminism with Induction and Coinduction," their Research Highlights article published in the February 2015 Communications of the ACM (cacm.acm.org/magazines/2015/2/182642).
00:00-00:25 VOICEOVER: You want coffee. The machine waits for you in its starting state. You put in a coin or a coffee pod to move it to a new state. You press a button, which brings it to its final state. You take the cup, and enjoy.
00:25-00:38 These two machines are equivalent. This candy machine is also essentially equivalent: You put money in, push a button, and get what you want.
00:38-00:53 So too can we compare theoretical machines such as text searches. Seeing how they're similar lets us eliminate redundancies, potentially leading to faster circuits, searches, and software.
00:53-01:11 Join us as we talk with two researchers in France, Filippo Bonchi and Damien Pous, as they show us new and faster ways to compare such theoretical machines, in Hacking Nondeterminism with Induction and Coinduction.
01:11-01:20 [Intro graphics/music]
01:20-01:46 At the École Normale Supérieure de Lyon, Filippo Bonchi and Damien Pous focus on the theoretical machines that drive the technological world. They specifically look at how they move from one state to the next until they reach their "final", or "accepting", states. Such machines are called "finite automata".
01:46-02:02 DR. POUS: The simplest real-world example is that of a coffee machine, a vending machine. Where this machine has some state, and you press a button, and the machine evolves to a new state, and possibly offers you some coffee, moving yet to another state.
02:02-02:15 In the world of computers, a regular expression search is another example of a nondeterministic finite automaton; or, as Drs. Bonchi and Pous call it in their paper, an NFA.
02:15-02:21 DR. POUS: A few As, then a B, then a few As, and this repeated at least one time.
02:21-02:25 Now let's compare *that* regular-expression search with another one.
02:25-02:49 DR. POUS: Here I have a state, the starting one, where I can do either A or B, and I remain in the same state. So I will do either A or B. Then I do one B, and I move to another state. And in this state, I can do as many As or Bs as I want. And this one is accepting.
02:49-02:58 You might notice that these two designs look pretty similar. That's because the searches could be used to get similar results, even though they looked quite different at first.
02:58-03:08 To prove their similarity, you first rearrange the two machines so there's always a clear path to the next step, in a process called "determinization".
03:08-03:19 Then you create a "bisimulation", by pairing up the states to see whether they match at each step. If so, you've proven that the two machines are essentially equivalent.
03:19-03:33 This is where optimization comes in. A technique developed by John Hopcroft and Richard Karp in 1971 showed that you can save time by drawing the bisimulation only up to a certain point.
03:33-03:47 DR. POUS: The thing is, this is not a pair which I have encountered so far... But this is a pair which I can relate using those three pairs here... This is almost a bisimulation, meaning, precisely, this is a bisimulation up to equivalence.
03:47-04:01 By looking at how states previously related to each other, you can create a bisimulation up to context, saving even more steps. A later development called "antichains" had similar results.
04:01-04:11 The innovation of Drs. Bonchi and Pous was to discover how these optimization techniques relate to each other -- and then to combine them.
04:11-04:24 DR. POUS: And what we realized, that we can do actually both... We can use both techniques together and we get what we call up to congruence, which is even more powerful in the sense that it can cut even more branches in the exploration.
04:24-04:44 DR. BONCHI: This is important also because it's kind of the meeting point of two principles which are very ubiquitous in computer science, which are induction and coinduction. So they meet together exactly in this bisimulation up to congruence.
04:44-04:54 Find out more in this month's Communications of the ACM, in the Research Highlights article, "Hacking Nondeterminism with Induction and Coinduction".
04:54-05:05 [Outro and credits]