commit 7af03ccf3a312952643dc7d6530117cd3b1e363d
parent ca2b3b3302975a9ff4b691ae3c7c4ec4b7e46960
Author: quantumish <freifeld.david@gmail.com>
Date: Sat, 25 Jul 2026 22:11:06 -0700
Format code for readability, add prompt for queries
Diffstat:
5 files changed, 141 insertions(+), 50 deletions(-)
diff --git a/install.sh b/install.sh
@@ -5,6 +5,3 @@ cd smlnj && config/install.sh && cd ..
wget -O words.txt https://github.com/InnovativeInventor/dict4schools/raw/master/safedict_full.txt
export PATH=$(pwd)/smlnj/bin:$PATH
ml-build minisql.cm Main.main minisql-image
-
-
-
diff --git a/ltl.md b/ltl.md
@@ -2,38 +2,77 @@
## What is LTL?
> [!NOTE]
-> Github's inline $\LaTeX$ is somewhat limited in what it allows you to write, so some of this notation is really just abusing similar-looking symbols.
+> Github's inline $\LaTeX$ is somewhat limited in what it allows you to write,
+> so some of this notation is really just abusing similar-looking symbols.
-Linear temporal logic is an extension of propositional logic that allows for reasoning over arbitrary time streams. The two core operators it provides are the _next_ operator $\circ \varphi$ that is true iff $\varphi$ is true at the next state and the _until_ operator $\varphi \cup \psi$ that is true iff $\psi$ is true at some future or current state and $\varphi$ is true at all states preceding it.
+Linear temporal logic is an extension of propositional logic that allows for
+reasoning over arbitrary time streams. The two core operators it provides are
+the _next_ operator $\circ \varphi$ that is true iff $\varphi$ is true at the
+next state and the _until_ operator $\varphi \cup \psi$ that is true iff $\psi$
+is true at some future or current state and $\varphi$ is true at all states
+preceding it.
The two main operators then allow you to build up more complex operators:
-- The _eventually_ operator $\diamondsuit$ which is defined as $\diamondsuit \varphi = true \cup \varphi$
+- The _eventually_ operator $\diamondsuit$ which is defined as
+ $\diamondsuit \varphi = true \cup \varphi$
- The _henceforth_ operator $\square$ defined as $\lnot \diamondsuit \lnot \varphi$
-- The _weak until_ operator $\varphi \text{ W } \psi$ defined as $(\varphi \cup \psi) \lor \square \varphi$ which relaxes the constraint of the until operator that the second condition must be satisfied at some point.
-- The _release_ operator $\varphi \text{ R } \psi$ is defined as $\lnot(\lnot\varphi \cup \lnot \psi)$ which is true iff $\psi$ always holds until "released" by $\varphi$ being true.
-(the names for these operators can vary - what I've written here is the verbiage `minisql` uses)
-
-LTL is used primarily for formal verification of systems (which you could imagine in many cases would need to encode time-dependent constraints) and also is partially what the TLA language is built on top of! Probably the most interesting application I saw for it was encoding invariants about parallelism in [Michigan State's slides](https://www.cse.msu.edu/~cse814/Lectures/14_introLTL.pdf) on the topic. Say for example you have a critical section of code guarded by a mutex. Let $\text{inCS}_X$ denote a process $X$ being in the critical section:
-- Mutual exclusion is expressed by: $\square(\lnot \text{inCS}_A \lor \lnot\text{inCS}_B)$ (in English: it is always true that either A is or B is not in the critical section)
-- You can also express that $A$ doesn't monopolize the lock: $\square(\text{inCS}_A \implies \diamondsuit \lnot\text{inCS}_A)$ (in English: it is always true that $A$ holding the lock implies it will eventually not hold the lock).
-
-Those slides also include some cool formalizations of fairness guarantees for the dining philosophers problem!
+- The _weak until_ operator $\varphi \text{ W } \psi$ defined as
+ $(\varphi \cup \psi) \lor \square \varphi$ which relaxes the constraint of
+ the until operator that the second condition must be satisfied at some point.
+- The _release_ operator $\varphi \text{ R } \psi$ is defined as
+ $\lnot(\lnot\varphi \cup \lnot \psi)$ which is true iff $\psi$ always
+ holds until "released" by $\varphi$ being true.
+
+(the names for these operators can vary - what I've written here is the verbiage
+`minisql` uses)
+
+LTL is used primarily for formal verification of systems (which you could
+imagine in many cases would need to encode time-dependent constraints) and also
+is partially what the TLA language is built on top of! Probably the most
+interesting application I saw for it was encoding invariants about parallelism in
+[Michigan State's slides](https://www.cse.msu.edu/~cse814/Lectures/14_introLTL.pdf)
+on the topic. Say for example you have a critical section of code guarded by a
+mutex. Let $\text{inCS}_X$ denote a process $X$ being in the critical section:
+
+- Mutual exclusion is expressed by:
+ $\square(\lnot \text{inCS}_A \lor \lnot\text{inCS}_B)$
+ (in English: it is always true that either A is or B is not in the critical
+ section)
+
+- You can also express that $A$ doesn't monopolize the lock:
+ $\square(\text{inCS}_A \implies \diamondsuit \lnot\text{inCS}_A)$
+ (in English: it is always true that $A$ holding the lock implies it will
+ eventually not hold the lock).
+
+Those slides also include some cool formalizations of fairness guarantees for the
+dining philosophers problem!
## Adding Support (this can be skipped)
-Adding support for the core of LTL is actually not that hard: `minisql` does predicate filtering via the higher-order function `filter`, which normally looks something like this in SML:
+Adding support for the core of LTL is actually not that hard: `minisql` does
+predicate filtering via the higher-order function `filter`, which normally looks
+something like this in SML:
```sml
fun filter f [] = []
| filter f (x::xs) = if f x then x::(filter f xs) else (filter f xs)
```
-Since SML has singly-linked lists ("cons cells") as the first class list construct, it becomes very easy to pass in the rest of the list to our predicate function `f`:
+
+Since SML has singly-linked lists ("cons cells") as the first class list construct,
+it becomes very easy to pass in the rest of the list to our predicate function `f`:
+
```sml
fun filterWith f [] = []
| filterWith f (x::xs) = if f(x, xs) then x::(filter f xs) else (filter f xs)
```
-The parser is also implemented in a fashion where adding more unary and binary constructs isn't a big ask. The execution engine now has to track where it "started" (the row that is actually being checked against the predicate), but otherwise these future-oriented predicates can be computed pretty easily by recursing on the rest of the list.
+The parser is also implemented in a fashion where adding more unary and binary
+constructs isn't a big ask. The execution engine now has to track where it "started"
+(the row that is actually being checked against the predicate), but otherwise these
+future-oriented predicates can be computed pretty easily by recursing on the rest of
+the list.
-Once we implement support for next and until, we can just have the parser automatically translate the more complex queries to be in terms of the two basic primitives via "artificial" constructors like:
+Once we implement support for next and until, we can just have the parser
+automatically translate the more complex queries to be in terms of the two basic
+primitives via "artificial" constructors like:
```sml
fun Eventually x = Until(True, x)
fun Henceforth x = Not(Eventually(Not x))
@@ -43,20 +82,29 @@ fun StrongRelease (x, y) = Not(WeakUntil(Not x, Not y))
```
## Queries
-Now we can mess with some queries! Note that all of this data can be generated via `randgen.py`: calling `python randgen.py cities` will generate the cities dataset, `python randgen.py sequsers` the sequential user dataset, etc.
+Now we can mess with some queries! Note that all of this data can be generated via
+`randgen.py`: calling `python randgen.py cities` will generate the cities dataset,
+`python randgen.py sequsers` the sequential user dataset, etc.
### Simple Queries
-Let's start with a simple dataset: say we have a simple business with one product that can meet with up to one client businesses a day. These clients have a limited number of actions as described by the following FSM:
+Let's start with a simple dataset: say we have a simple business with one product
+that can meet with up to one client businesses a day. These clients have a limited
+number of actions as described by the following FSM:
<p align="center">
<img src="./fsm.png">
</p>
-"New" is short for a client coming in contact with our business, "buy" is them buying our product, "com" is them complaining about it, "ret" is them returning it, and "leave" is them vowing to never work with us again.
+"New" is short for a client coming in contact with our business, "buy" is them buying
+our product, "com" is them complaining about it, "ret" is them returning it, and
+"leave" is them vowing to never work with us again.
-`sequsers.json` is a table where each row represents what happened in a day and the rows are laid out chronologically (e.g. first day is the first row).
+`sequsers.json` is a table where each row represents what happened in a day and the
+rows are laid out chronologically (e.g. first day is the first row).
-Let's try the simplest possible LTL query: maybe we're interested in predicting what events could indicate that a client is going to buy our product. To do that we'd want all events that _precede_ a buy order:
+Let's try the simplest possible LTL query: maybe we're interested in predicting what
+events could indicate that a client is going to buy our product. To do that we'd want
+all events that _precede_ a buy order:
```
$ ./minisql
SELECT * FROM sequsers WHERE NEXT action = 'buy' LIMIT 10;
@@ -72,7 +120,9 @@ buy | Clamative Corp. | 75337 |
new | Macrospore Corp. | 86109 |
buy | Attendant Corp. | 18739 |
```
+
Is this correct? Let's peek at the first 15 rows of the actual data using `viewer.py`:
+
```python
$ python viewer.py sequsers.json 15
{'action': 'new', 'name': 'Irrevocablaginable Corp.', 'headcount': 65498}
@@ -91,6 +141,7 @@ $ python viewer.py sequsers.json 15
{'action': 'new', 'name': 'Dampnesses Corp.', 'headcount': 50746}
{'action': 'new', 'name': 'Protopectinase Corp.', 'headcount': 55577}
```
+
The first two buy actions line up with our output!
Let's try some more sample queries:
@@ -107,7 +158,9 @@ SELECT name, headcount FROM sequsers WHERE action = 'new' UNTIL action = 'buy';
SELECT * FROM sequsers WHERE NEXT (action = 'leave' AND headcount > 10000);
```
-Okay, let's try actually doing the query mentioned in the challenge ("get all customers who returned product within 2 weeks"). The best we can do with plain old linear temporal logic is something like:
+Okay, let's try actually doing the query mentioned in the challenge ("get all
+customers who returned product within 2 weeks"). The best we can do with plain old
+linear temporal logic is something like:
```sql
SELECT * FROM sequsers WHERE action = 'buy' AND (action = 'leave' WITHIN 14);
```
@@ -117,33 +170,54 @@ fun Within (x, 0) = x
| Within (x, i) = Or(Next(x), Next(Within(x, i-1)))
```
-Yet this isn't really what we want: all this results in is all events that are within 14 events of some client returning our product. We just want the event where said client bought it (if it is within 14 events!). Unfortunately vanilla LTL doesn't support this as it is very much future-oriented and applies predicates independent of time to several states across a time stream.
+Yet this isn't really what we want: all this results in is all events that are within
+14 events of some client returning our product. We just want the event where said
+client bought it (if it is within 14 events!). Unfortunately vanilla LTL doesn't
+support this as it is very much future-oriented and applies predicates independent of
+time to several states across a time stream.
### Temporally Dependent Queries
-Some variants of LTL solve the problem we had earlier by introducing operators that let you refer to _past_ values. This is a bit overkill for our concerns and it also would make the code a bit less pleasant. Instead, `minisql` introduces the notion of the "current" row for use in predicates.
+Some variants of LTL solve the problem we had earlier by introducing operators that
+let you refer to _past_ values. This is a bit overkill for our concerns and it also
+would make the code a bit less pleasant. Instead, `minisql` introduces the notion of
+the "current" row for use in predicates.
For example, we can query all users who returned our product with:
```sql
-SELECT * FROM sequsers WHERE action = 'buy' AND EVENTUALLY (name = cur.name AND action = 'return');
+SELECT * FROM sequsers WHERE action = 'buy' AND EVENTUALLY
+ (name = cur.name AND action = 'return');
```
-While `name` and `action` columns will refer to the columns of the state currently being checked at any point in the timestream, `cur.name` refers to the column of the current state.
+While `name` and `action` columns will refer to the columns of the state currently
+being checked at any point in the timestream, `cur.name` refers to the column of the
+current state.
We can also write the earlier query now:
```sql
-SELECT * FROM sequsers WHERE action = 'buy' AND ((name = cur.name AND action = 'return') WITHIN 14);
+SELECT * FROM sequsers WHERE action = 'buy' AND
+ ((name = cur.name AND action = 'return') WITHIN 14);
```
-In general this expands the number of actually meaningful predicates we can make. Say we're interested in all the complaints that come from companies who have shrunk their headcounts since they bought our product (maybe they're just haggling to cut expenses...)
+In general this expands the number of actually meaningful predicates we can make. Say
+we're interested in all the complaints that come from companies who have shrunk their
+headcounts since they bought our product (maybe they're just haggling to cut
+expenses...)
```sql
-SELECT name FROM sequsers WHERE action = 'buy' AND EVENTUALLY (name = cur.name AND (action = 'return' AND headcount < cur.headcount));
+SELECT name FROM sequsers WHERE action = 'buy' AND EVENTUALLY
+ (name = cur.name AND (action = 'return' AND headcount < cur.headcount));
```
### The Query You Asked For
-Okay, but there's still a big constraint on our data here: only one event can happen per day (or alternatively our only notion of time is the event number). Let's now consider `users.json` which is exactly the same as `sequsers.json` except for the fact that there is now a `time` column with the time of the event as a Unix timestamp. Combining the very limited time operations provided by `minisql` with the temporally dependent queries lets us finally do this the _right_ way.
+Okay, but there's still a big constraint on our data here: only one event can happen
+per day (or alternatively our only notion of time is the event number). Let's now
+consider `users.json` which is exactly the same as `sequsers.json` except for the
+fact that there is now a `time` column with the time of the event as a Unix
+timestamp. Combining the very limited time operations provided by `minisql` with the
+temporally dependent queries lets us finally do this the _right_ way.
To get all clients who bought and returned their product within two weeks, write
```sql
-SELECT name, headcount FROM users WHERE action = 'buy' AND EVENTUALLY (name = cur.name AND (action = 'return' AND time - cur.time < 2 weeks));
+SELECT name, headcount FROM users WHERE action = 'buy' AND EVENTUALLY
+ (name = cur.name AND (action = 'return' AND time - cur.time < 2 weeks));
```
On my randomly generated copy, this returns
```
@@ -162,4 +236,6 @@ $ python viewer.py users.json 1000 | grep Mathurin
{'time': 1789821027, 'action': 'leave', 'name': 'Mathurin Corp.', 'headcount': 20720}
```
-This is not hardcoded: the parser will recognize any of "seconds", "minutes", "hours", "days", or "weeks" and the query engine prevents you from mixing up integers and timestamps, but beyond that the time system is not fully realized.
+This is not hardcoded: the parser will recognize any of "seconds", "minutes",
+"hours", "days", or "weeks" and the query engine prevents you from mixing up integers
+and timestamps, but beyond that the time system is not fully realized.
diff --git a/minisql.sml b/minisql.sml
@@ -271,6 +271,7 @@ fun display ((rows, cols) : rowvals list * columnref list) =
(* Main execution loop of program. *)
fun loop () : unit =
let
+ val () = print "minisql> "
val input = Option.valOf (TextIO.inputLine TextIO.stdIn)
handle Option => raise Parse
in
diff --git a/randgen.py b/randgen.py
@@ -7,19 +7,26 @@ import time
WORDS = [l.strip() for l in open("./words.txt").readlines()]
def cities():
- states = ['Alabama', 'Alaska', 'Arizona', 'Arkansas', 'California', 'Colorado', 'Connecticut', 'Delaware', 'Florida', 'Georgia', 'Hawaii', 'Idaho', 'Illinois', 'Indiana', 'Iowa', 'Kansas', 'Kentucky', 'Louisiana', 'Maine', 'Maryland', 'Massachusetts', 'Michigan', 'Minnesota', 'Mississippi', 'Missouri', 'Montana', 'Nebraska', 'Nevada', 'New Hampshire', 'New Jersey', 'New Mexico', 'New York', 'North Carolina', 'North Dakota', 'Ohio', 'Oklahoma', 'Oregon', 'Pennsylvania', 'Rhode Island', 'South Carolina', 'South Dakota', 'Tennessee', 'Texas', 'Utah', 'Vermont', 'Virginia', 'Washington', 'West Virginia', 'Wisconsin', 'Wyoming']
- regions = ["South", "West", "Southwest", "North", "East", "Northeast", "Middle", "Midwest", "Mideast", "Nowhere"]
-
-
- print(random.choice(states))
-
- # print(WORDS[:10])
+ states = ['Alabama', 'Alaska', 'Arizona', 'Arkansas', 'California',
+ 'Colorado', 'Connecticut', 'Delaware', 'Florida', 'Georgia',
+ 'Hawaii', 'Idaho', 'Illinois', 'Indiana', 'Iowa', 'Kansas',
+ 'Kentucky', 'Louisiana', 'Maine', 'Maryland', 'Massachusetts',
+ 'Michigan', 'Minnesota', 'Mississippi', 'Missouri', 'Montana',
+ 'Nebraska', 'Nevada', 'New Hampshire', 'New Jersey', 'New Mexico',
+ 'New York', 'North Carolina', 'North Dakota', 'Ohio', 'Oklahoma',
+ 'Oregon', 'Pennsylvania', 'Rhode Island', 'South Carolina',
+ 'South Dakota', 'Tennessee', 'Texas', 'Utah', 'Vermont',
+ 'Virginia', 'Washington', 'West Virginia', 'Wisconsin', 'Wyoming']
+ regions = ["South", "West", "Southwest", "North", "East", "Northeast",
+ "Middle", "Midwest", "Mideast", "Nowhere"]
data = []
for i in range(10000):
+ name1 = random.choice(WORDS).capitalize()
+ name2 = random.choice(WORDS).capitalize()
data.append({"state": random.choice(states),
"region": random.choice(regions),
- "name": f"{random.choice(WORDS).capitalize()} {random.choice(WORDS).capitalize()}",
+ "name": f"{name1} {name2}",
"pop": random.randint(1000000, 1000000000),
"pop_male": random.randint(10000, 1000000),
"pop_female": random.randint(10000, 1000000)})
@@ -46,7 +53,8 @@ class Customer:
return "buy"
if "buy" in self.past_actions:
if "return" not in self.past_actions:
- self.past_actions.append(random.choice(["return", "complain"]))
+ action = ["return", "complain"]
+ self.past_actions.append(random.choice())
else:
self.past_actions.append("leave")
return self.past_actions[-1]
@@ -73,8 +81,10 @@ def customers(seq=True):
f = open(f"./{'seq' if seq else ''}users.json", "w")
f.write(json.dumps(data))
f.close()
-
-if sys.argv[1] == "cities":
+
+if len(sys.argv) < 2:
+ print("usage: randgen.py [cities/sequsers/users]")
+elif sys.argv[1] == "cities":
cities()
elif sys.argv[1] == "sequsers":
customers()
diff --git a/readme.md b/readme.md
@@ -1,15 +1,22 @@
# minisql
> simple sql querying over json files
-`minisql` is a small program that lets you query flat JSON files with relatively simple SELECT queries. It also supports a number of extended queries based off of linear temporal logic for interacting with temporal data: see [LTL.md](https://github.com/quantumish/minisql/blob/master/ltl.md) for a writeup on the inclusion of these features!
+`minisql` is a small program that lets you query flat JSON files with relatively
+simple SELECT queries. It also supports a number of extended queries based off
+of linear temporal logic for interacting with temporal data: see
+[LTL.md](https://github.com/quantumish/minisql/blob/master/ltl.md) for a writeup
+on the inclusion of these features!
## install
Run `install.sh` which will automatically install SML locally and compile `minisql`.
-## usage
-Run `./minisql` to run queries. No need for a command line argument: simply use the name of the JSON file you want to query as the name of the table in your query and `minisql` will parse it on the fly.
+## usage
+Run `./minisql` to run queries. No need for a command line argument: simply use the
+name of the JSON file you want to query as the name of the table in your query and
+`minisql` will parse it on the fly.
-You can generate some sample data to play with by running `randgen.py`. See `ltl.md` for more info.
+You can generate some sample data to play with by running `randgen.py`. See `ltl.md`
+for more info.
Example query (over the file `cities.json` in the current directory):
```
