A vocabulary to reason over, and blocks that snap together on it - #255
Closed
bkearns wants to merge 5 commits into
Closed
A vocabulary to reason over, and blocks that snap together on it#255bkearns wants to merge 5 commits into
bkearns wants to merge 5 commits into
Conversation
…reasoning The rule language could say anything and knew nothing. There was no vocabulary — no way to state that a part is part of a whole, that one person reports to another, or that calling something is a way of depending on it — so every rule had to invent its predicates and no two rules had to agree. Twenty-four predicates across business, technical and structural reasoning, each with the one line a person needs to pick it from a palette. The reasoning is GENERATED from what each relation is, not written out. Declaring part_of transitive is what produces its closure; declaring contains its inverse is what produces the other direction; declaring calls a kind of depends_on is what makes a call a dependency. Four rule shapes across two dozen relations is where an ontology quietly stops being consistent, because the twentieth one gets typed a little differently from the first. An inverse must be declared on both sides, and a test enforces it. A one-sided inverse is the shape that makes an ontology asymmetric without looking wrong: one direction reasons and the other silently does not. Constraints report rather than assert. An irreflexive relation yields a violation row, not a fact, because a part that is part of itself is a broken ontology and the engine should be able to say so rather than absorb it. WHICH IS WHERE THE INTERESTING BUG WAS. The transitive closure first carried an `X != Z` guard, which looks like it protects termination. It does not — the fact set is bounded by the square of the domain, so the fixpoint closes on its own. What the guard actually did was suppress p(X, X), which is precisely the evidence a cycle leaves and precisely what the irreflexivity check reads. A guard that hides the symptom it was meant to make safe is worse than no guard, and the cycle test is what caught it. Nothing about time is a predicate. "Recent" is a date comparison asked when the question is asked, not a fact somebody derived and then had to keep true — so created_at and its siblings are marked Computed, a test asserts that no computed predicate is ever derived, and another asserts that `recent` and its lookalikes are absent on purpose. If we can compute, we should not infer. The engine is the judge throughout: every generated rule is handed to parse_rules, and the whole set is handed to stratify, because generating rules per relation makes accidental recursion easy and an unstratifiable set derives nothing at all. 1574 workspace lib tests, clippy and fmt clean.
D8 asked for a Scratch-shaped composer whose block definitions come from
the server, so a new operator ships as a new block and every existing
client lays it out without knowing what it compiles to. This is that
catalogue and the two directions between blocks and rule text.
Four shapes, mirroring Scratch: a hat that starts a rule, booleans that
stack under it, reporters that fill operand holes, and a conclusion.
Small on purpose — a person learns four fits, not forty — and it is what
makes "malformed is unbuildable" true rather than aspirational.
Blocks compile to fragments over the ontology vocabulary rather than to
invented predicates, so the palette and the reasoning engine talk about
the same world. The time block compiles to a computation, not a fact:
created_at plus a comparison against the clock, because if we can compute
we should not infer.
Projection guesses and then PROVES. Whatever it reconstructs is compiled
again and returned only if it reproduces the input byte for byte, which
is D14's requirement enforced rather than asserted. A rule the palette
cannot express comes back as None — "beyond blocks" — never as half a
tree that is subtly not the rule.
Three things the tests found, each a real bug rather than a wrong
expectation.
A block can compile to SEVERAL comma-separated fragments; within_last
emits both the atom binding the timestamp and the comparison over it. The
first projection split the body on commas and matched one fragment at a
time, so that block could never be recovered. It now tries the longest
run first.
An unconstrained capture is a greedy template swallowing another block's
syntax: {relation}(E, "{other}") read `not tag(E, "secret")` as a
relation named "not tag", and the result looked plausible and was wrong.
Captures are now checked against what the slot could really hold.
And separating fresh variables out of the placeholder list silently
stopped substituting them, because one list was serving two opposite
ideas — a placeholder is filled from outside, a fresh variable is
generated. They are two functions now.
A quote in a slot is refused rather than escaped. It would close the
literal early and let the rest of the value become rule syntax, which is
injection by another name, and a quote in a path is a mistake worth
being told about.
1593 workspace lib tests, clippy and fmt clean.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Two layers the rules plane needs and neither editor could work without: a vocabulary to reason over, and a block palette to compose against it.
The vocabulary
The rule language could say anything and knew nothing — no way to state that a part is part of a whole, that one person reports to another, or that calling something is a way of depending on it. Every rule invented its own predicates and no two had to agree.
24 predicates across business, technical and structural reasoning, each with the one line a person needs to pick it from a palette.
The reasoning is generated from what each relation is. Declaring
part_oftransitive produces its closure; declaringcontainsits inverse produces the other direction; declaringcallsa kind ofdepends_onmakes a call a dependency. Four rule shapes across two dozen relations is where an ontology quietly stops being consistent, because the twentieth gets typed a little differently from the first.An inverse must be declared on both sides, enforced by a test — a one-sided inverse makes an ontology asymmetric without looking wrong.
Constraints report rather than assert: an irreflexive relation yields a violation row, not a fact, because a part that is part of itself is a broken ontology and the engine should say so rather than absorb it.
The interesting bug
The transitive closure first carried an
X != Zguard, which looks like it protects termination. It doesn't — the fact set is bounded by the square of the domain, so the fixpoint closes on its own. What it actually did was suppressp(X, X), which is precisely the evidence a cycle leaves and precisely what the irreflexivity check reads. A guard that hides the symptom it was meant to make safe is worse than no guard. The cycle test caught it.Compute, don't infer
Nothing about time is a predicate. "Recent" is a date comparison asked when the question is asked, not a fact somebody derived and then has to keep true.
created_atand its siblings are markedComputed; one test asserts no computed predicate is ever derived, another assertsrecentand its lookalikes are absent on purpose.The engine is the judge throughout: every generated rule goes to
parse_rules, and the whole set tostratify— generating rules per relation makes accidental recursion easy, and an unstratifiable set derives nothing at all.The block palette
Four shapes mirroring Scratch — a hat, booleans that stack, reporters that fill holes, a conclusion. Small on purpose: a person learns four fits, not forty, and it's what makes "malformed is unbuildable" true rather than aspirational.
Blocks compile to fragments over the vocabulary, so the palette and the reasoning engine talk about the same world.
Projection guesses, then proves. Whatever it reconstructs is compiled again and returned only if it reproduces the input byte for byte — D14's requirement enforced rather than asserted. A rule the palette can't express comes back as
None("beyond blocks"), never half a tree that is subtly not the rule.Three bugs the tests found
within_lastemits both the atom binding the timestamp and the comparison over it. Splitting the body on commas and matching one fragment at a time made that block unrecoverable. Now it tries the longest run first.{relation}(E, "{other}")readnot tag(E, "secret")as a relation namednot tag— plausible-looking and wrong. Captures are now checked against what the slot could really hold.A quote in a slot is refused, not escaped — it would close the literal early and let the rest become rule syntax, which is injection by another name.
Tests
1593 workspace lib tests. clippy
-D warningsand fmt clean. Live-cluster tests were not run.Not yet wired to an endpoint — this is the contract both the block composer and the NL editor build on.