Relational Algebra

Honest by Construction

The engine treats authored expected rows as assertions, not truth.

highlighted = computed this step

Honest by construction

Honesty note: set algebra not SQL bag/NULL, tiny finite tables, no product/perf claims. The engine treats authored expected rows as assertions checked against recompute. Note: the authored assertion is never the source of truth.

recompute boundary\text{recompute boundary}

A correct expected assertion passes

A correct expected assertion matches the recomputed output and the lesson can render the result. The checked row count here is 3. Note: the rendered table is still produced from recompute.

checked rows=3\text{checked rows}=3

set algebra not SQL bag/NULL, tiny finite tables, no product/perf claims

Joinjoin sid=sidarity 3 rows 3Studentsarity 2 rows 3Enrollarity 2 rows 3
joinsidnamecourses1AnnDBs1AnnOSs2BoDB

A wrong expected assertion is rejected

The self-test also tries a wrong authored row and the compiler rejects it at the trust boundary. There is no diagram for the rejection because rejected output never becomes renderable lesson data. Note: this is the protection that keeps prose from becoming the answer.

wrong expected rejected\text{wrong expected rejected}

Summary

The final answer falls out of bottom-up recompute, with expected rows serving only as checked assertions. Bag or multiset behavior and NULL are deferred to the next book.

honesty summary\text{honesty summary}