4 ms·
What things that SQLite does revolves around anything halting-problem related? Almost all SQLite queries are over a finite amount of data and have a well-speci
by Jweb_Guru 8y ago
What things that SQLite does revolves around anything halting-problem related? Almost all SQLite queries are over a finite amount of data and have a well-specified legal solution set that barely requires recursion; WITH RECURSIVE doesn't have to halt but still has a well-defined semantics where it does. I think even most optimization problems on SQL queries are decidable; you have to want to do quite interesting things (like prove query subsumption) before you get into undecidability territory.
- shakna 8y agoI see two main areas where the halting problem comes into play: SQLite involves extensive amounts of IO, it's a flat-file database most of the time, afterall. That is inherently unsafe, and can't be proven to terminate. SQLite also has an internal VM, for which it generates code (the source of the bug in this article). The VM is Turing-Complete, hence you can't always prove that it will terminate.
- Jweb_Guru 8y ago> SQLite involves extensive amounts of IO, it's a flat-file database most of the time, afterall. That is inherently unsafe, and can't be proven to terminate. Under reasonable assumptions about I/O (POSIX APIs and stuff), you can certainly prove termination of such operations. > SQLite also has an internal VM, for which it generates code (the source of the bug in this article). The VM is Turing-Complete, hence you can't always prove that it will terminate. You don't have to always prove any VM program will terminate. You just have to show termination-preserving refinement of the SQLite code generator (as I alluded to in my other post). You don't even need types for this.