Type-level corrections: a proposal that says the right thing in the wrong shape.
Every model asked about a type writes facts about the type symbol —
(eats penguin fish), (mortal penguin) — where the KB's idiom quantifies over the
type's instances. Measured across eight models on the shipped schema this is the
dominant remaining error class, and nothing else catches it: naming/problems passes
it (the names are all well-formed), wff passes it, the argIsa constraints pass it
(open-world — a type symbol carries no type membership, and an untyped argument cannot
violate), and it stores. The claim is usually right; only its shape is wrong.
So this rewrites rather than rejects. Each correction carries the sentence it came from, the one to store instead, the alternatives where more than one shape is defensible, and why — because for the most common case the choice between shapes is a semantic judgement no engine can make for the author:
| claim | shape | inference | exception possible? |
|---|---|---|---|
| definitional — what a penguin is | (genl penguin mortal) | free, off the cached closure | no |
| defeasible — what a penguin usually does | (set/defaultRule (implies (penguin ?x) (mortal ?x))) | forward chaining | yes, via exceptWhen |
The defeasible shape is the default, on asymmetric risk. A defeasible claim that
should have been definitional costs only the chaining it did not need. A definitional
claim that should have been defeasible cannot take an exceptWhen at all — a genl
edge admits no exception — so the only repair is retracting it and rebuilding the
closure. Guessing wrong in that direction is the expensive one, so it is not guessed.
Nothing here mutates: a correction is a proposal about a proposal. What to do with it — show both shapes, show only the rewrite, let the author edit it — is the caller's.
Type-level corrections: a proposal that says the right thing in the wrong shape. Every model asked about a *type* writes facts **about the type symbol** — `(eats penguin fish)`, `(mortal penguin)` — where the KB's idiom quantifies over the type's instances. Measured across eight models on the shipped schema this is the dominant remaining error class, and nothing else catches it: `naming/problems` passes it (the names are all well-formed), `wff` passes it, the argIsa constraints pass it (open-world — a type symbol carries no type membership, and an untyped argument cannot violate), and it stores. The claim is *usually right*; only its shape is wrong. So this rewrites rather than rejects. Each correction carries the sentence it came from, the one to store instead, the **alternatives** where more than one shape is defensible, and why — because for the most common case the choice between shapes is a semantic judgement no engine can make for the author: | claim | shape | inference | exception possible? | |---|---|---|---| | definitional — what a penguin *is* | `(genl penguin mortal)` | free, off the cached closure | no | | defeasible — what a penguin *usually does* | `(set/defaultRule (implies (penguin ?x) (mortal ?x)))` | forward chaining | yes, via `exceptWhen` | **The defeasible shape is the default, on asymmetric risk.** A defeasible claim that should have been definitional costs only the chaining it did not need. A definitional claim that should have been defeasible cannot take an `exceptWhen` at all — a `genl` edge admits no exception — so the only repair is retracting it and rebuilding the closure. Guessing wrong in that direction is the expensive one, so it is not guessed. Nothing here mutates: a correction is a proposal about a proposal. What to do with it — show both shapes, show only the rewrite, let the author edit it — is the caller's.
(apply-correction c)(apply-correction c alt)The [sentence context] entry a correction becomes — its :to, or the :alternatives
entry at alt. Returns nil for a correction with no :to (one that only reports),
so a caller cannot silently store the sentence it was warning about.
The `[sentence context]` entry a correction becomes — its `:to`, or the `:alternatives` entry at `alt`. Returns nil for a correction with no `:to` (one that only reports), so a caller cannot silently store the sentence it was warning about.
(correction kb sentence)The correction for one sentence, or nil when nothing here applies.
Passes compose: one that yields a :to hands it to the passes after it, so a
sentence that is malformed and states a relation of type symbols is repaired in
both respects instead of only the first. The result keeps the original :from,
joins every :why, names the chain in :rules, and carries the weakest
confidence in it — a chain is no surer than its least sure link.
A pass that claims a sentence without a :to ends the chain and drops the repair
accumulated so far: a partial fix whose result the engine would still refuse is
worse than no fix, and the joined :why still says everything found.
The correction for one sentence, or nil when nothing here applies. Passes **compose**: one that yields a `:to` hands it to the passes after it, so a sentence that is malformed *and* states a relation of type symbols is repaired in both respects instead of only the first. The result keeps the original `:from`, joins every `:why`, names the chain in `:rules`, and carries the **weakest** confidence in it — a chain is no surer than its least sure link. A pass that claims a sentence without a `:to` ends the chain and drops the repair accumulated so far: a partial fix whose result the engine would still refuse is worse than no fix, and the joined `:why` still says everything found.
(corrections kb entries)Corrections for a batch of [sentence context] entries — {:corrections [...] :unchanged [...]}, each correction carrying :index and :context so a caller can
point at the line it came from.
Read-only: nothing is stored, and a corrected sentence is not re-checked here, so a
caller that intends to store one should still run it through v/check.
Corrections for a batch of `[sentence context]` entries — `{:corrections [...]
:unchanged [...]}`, each correction carrying `:index` and `:context` so a caller can
point at the line it came from.
Read-only: nothing is stored, and a corrected sentence is *not* re-checked here, so a
caller that intends to store one should still run it through `v/check`.cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |