Read an OpenCyc KB dump directory — server/cyc/run/units/<n>/ — as assertions.
This is the other end of vaelii.foreign.cycl: the same
{:formula :mt :strength :direction} maps, taken straight from the binary dump
instead of from a text re-dump of it, so vaelii.foreign.cyc translates either
without knowing which it got.
A dump is several files that only mean something together. Each holds a flat
sequence of records — a copyright string, then dump-id followed by that record's
fields — and every reference between them is an integer id resolved against another
file:
constant-shell.text "name" -> dump-id, in plain text: the whole name table
nart-hl-formula.cfasl nart id -> its HL formula, whose head is a function
clause-struc.cfasl clause-struc id -> a CNF, which is how a rule is stored
assertion.cfasl id, formula-data, mt, flags, arguments, plist
So the three small tables are read whole and the 780 MB assertion file streams
against them. constant-shell.text being text is not a convenience this reader
invented — the dump writes the name table twice, once as CFASL and once as text, and
the text one is complete.
A NART may name a NART defined later in the file. Resolving during the read would
render that forward reference as an unresolved marker and then propagate it into every
assertion mentioning the term, so the formulas are read with NART references left as
markers and expanded when an assertion is emitted — by which point every NART is in
the table. nart-depth-limit and nart-node-limit are what a NART that refers back
to itself would otherwise do.
What the counts are for. Nothing frames a CFASL object but its own opcode, so a
mis-sized payload desynchronizes the rest of the file instead of failing in place.
Each dump states its own record count in <name>-count.text, and a read that reaches
the end of the file is compared against it: a short read means the stream went out of
step, and it is an error rather than a smaller KB. A read that stopped early has no
such comparison to make — the stated count describes the whole file — so :limit
samples a dump without the check and only without it.
Provenance of the format, and which upstream sources may be used on it:
licenses/THIRD-PARTY.md.
Read an OpenCyc KB dump directory — `server/cyc/run/units/<n>/` — as assertions.
This is the other end of `vaelii.foreign.cycl`: the same
`{:formula :mt :strength :direction}` maps, taken straight from the binary dump
instead of from a text re-dump of it, so `vaelii.foreign.cyc` translates either
without knowing which it got.
**A dump is several files that only mean something together.** Each holds a flat
sequence of records — a copyright string, then `dump-id` followed by that record's
fields — and every reference between them is an integer id resolved against another
file:
constant-shell.text "name" -> dump-id, in plain text: the whole name table
nart-hl-formula.cfasl nart id -> its HL formula, whose head is a function
clause-struc.cfasl clause-struc id -> a CNF, which is how a rule is stored
assertion.cfasl id, formula-data, mt, flags, arguments, plist
So the three small tables are read whole and the 780 MB assertion file streams
against them. `constant-shell.text` being text is not a convenience this reader
invented — the dump writes the name table twice, once as CFASL and once as text, and
the text one is complete.
**A NART may name a NART defined later in the file.** Resolving during the read would
render that forward reference as an unresolved marker and then propagate it into every
assertion mentioning the term, so the formulas are read with NART references left as
markers and expanded when an assertion is *emitted* — by which point every NART is in
the table. `nart-depth-limit` and `nart-node-limit` are what a NART that refers back
to itself would otherwise do.
**What the counts are for.** Nothing frames a CFASL object but its own opcode, so a
mis-sized payload desynchronizes the rest of the file instead of failing in place.
Each dump states its own record count in `<name>-count.text`, and a read that reaches
the end of the file is compared against it: a short read means the stream went out of
step, and it is an error rather than a smaller KB. A read that stopped early has no
such comparison to make — the stated count describes the whole file — so `:limit`
samples a dump without the check and only without it.
Provenance of the format, and which upstream sources may be used on it:
`licenses/THIRD-PARTY.md`.(assertion [_id [formula-data mt flags _arguments plist]] narts clause-strucs)One assertion record as {:formula :mt :strength :direction}, or nil when its
formula has no reading.
Cyc's own monotonic-vs-default marking comes across as vaelii's assumption strength,
and a false truth value as the not the record's own :truth will carry.
One assertion record as `{:formula :mt :strength :direction}`, or nil when its
formula has no reading.
Cyc's own monotonic-vs-default marking comes across as vaelii's assumption strength,
and a false truth value as the `not` the record's own `:truth` will carry.(cnf-formula cnf truth)The formula a CNF states, given the assertion's truth.
Negative literals are the antecedent and positive ones the conclusion, so a clause
with both is an implication — and that is what carries a rule's direction across,
which a bare ¬A ∨ ¬B would not. All-negative is an integrity constraint and
several-positive a real disjunction; both come back as the formula they are, for the
translation to drop under its own reason.
truth is consulted only for a single ground positive literal, where it is the
difference between a fact and its negation.
The formula a CNF states, given the assertion's `truth`. Negative literals are the antecedent and positive ones the conclusion, so a clause with both is an implication — and that is what carries a rule's direction across, which a bare `¬A ∨ ¬B` would not. All-negative is an integrity constraint and several-positive a real disjunction; both come back as the formula they are, for the translation to drop under its own reason. `truth` is consulted only for a single ground positive literal, where it is the difference between a fact and its negation.
(constant-resolvers names)Resolvers that turn a constant handle into the cyc/Name symbol the translation reads.
A name the table does not hold reads back as a marker rather than as a symbol, so a dump missing a constant is dropped with a reason instead of spelling a term nil.
Resolvers that turn a constant handle into the `cyc/Name` symbol the translation reads. A name the table does not hold reads back as a marker rather than as a symbol, so a dump missing a constant is dropped with a reason instead of spelling a term nil.
(decode-flags flags)The {:gaf? :direction :truth :strength} an assertion's flags integer states.
The `{:gaf? :direction :truth :strength}` an assertion's flags integer states.
(dump-directory? dir)Whether dir looks like a KB dump directory rather than a re-dumped text file.
The name table and the assertions are what a read needs; a directory holding both is one this namespace can read.
Whether `dir` looks like a KB dump directory rather than a re-dumped text file. The name table and the assertions are what a read needs; a directory holding both is one this namespace can read.
(expand-narts x narts)Replace every (:nart id) marker in x with that NART's formula.
Two bounds, because a chain and a fan-out are different pathologies.
nart-depth-limit stops the chain: a NART naming a NART that names the first would
otherwise not terminate. nart-node-limit stops the width: a formula mentioning two
NARTs doubles at every hop, and nesting says nothing about how wide each level is.
Whichever runs out first, what is left keeps its markers and is dropped by the
translation — the same answer an unresolvable reference gets.
Replace every `(:nart id)` marker in `x` with that NART's formula. Two bounds, because a chain and a fan-out are different pathologies. `nart-depth-limit` stops the chain: a NART naming a NART that names the first would otherwise not terminate. `nart-node-limit` stops the width: a formula mentioning two NARTs doubles at every hop, and nesting says nothing about how wide each level is. Whichever runs out first, what is left keeps its markers and is dropped by the translation — the same answer an unresolvable reference gets.
(formula-of gaf? formula-data clause-strucs truth)The formula an assertion states, from its stored formula-data.
Four cases, and the one easy to miss is the first: a ground atomic formula may be
stored as a clause too, and then its formula is the clause's single positive
literal rather than the implication cnf-formula would build. 83,464 of OpenCyc
4.0's assertions are that shape, so reading the gaf bit without it leaves a
clause-struc reference where a fact should be.
The formula an assertion states, from its stored `formula-data`. Four cases, and the one easy to miss is the first: **a ground atomic formula may be stored as a clause too**, and then its formula is the clause's single positive literal rather than the implication `cnf-formula` would build. 83,464 of OpenCyc 4.0's assertions are that shape, so reading the gaf bit without it leaves a clause-struc reference where a fact should be.
How far a chain of NART references is followed before one reads back as its own marker.
A NART's formula may mention another NART, and nothing in a dump forbids a cycle, so the chain is bounded. 24 is deeper than any chain OpenCyc 4.0 actually states.
How far a chain of NART references is followed before one reads back as its own marker. A NART's formula may mention another NART, and nothing in a dump forbids a cycle, so the chain is bounded. 24 is deeper than any chain OpenCyc 4.0 actually states.
How many nodes one expansion may walk before the rest is left as it stands.
Depth bounds a chain and not the work: a NART whose formula mentions a NART twice doubles at every hop, so 24 levels of it is 16.7M nodes and a heap the read does not come back from. This counts what the walk actually touches, which is the quantity that has to stay finite. 100,000 is orders of magnitude past the largest formula OpenCyc 4.0 states, and small enough that a dump built to blow the expansion up costs a few megabytes instead of the process.
How many nodes one expansion may walk before the rest is left as it stands. Depth bounds a chain and not the work: a NART whose formula mentions a NART twice doubles at every hop, so 24 levels of it is 16.7M nodes and a heap the read does not come back from. This counts what the walk actually touches, which is the quantity that has to stay finite. 100,000 is orders of magnitude past the largest formula OpenCyc 4.0 states, and small enough that a dump built to blow the expansion up costs a few megabytes instead of the process.
(read-clause-strucs dir names)clause-struc.cfasl as a clause-struc-id -> CNF map.
A record is its CNF and then the assertions that use it; the CNF is (neg-lits pos-lits), which is how every rule in the KB is stored.
`clause-struc.cfasl` as a clause-struc-id -> CNF map. A record is its CNF and then the assertions that use it; the CNF is `(neg-lits pos-lits)`, which is how every rule in the KB is stored.
(read-constant-names dir)constant-shell.text as a dump-id -> name map.
The file is a copyright string, the constant count, then "Name" id a line at a
time. Read as text rather than as Lisp: a name is a quoted string and an id an
integer, and nothing else appears.
`constant-shell.text` as a dump-id -> name map. The file is a copyright string, the constant count, then `"Name" id` a line at a time. Read as text rather than as Lisp: a name is a quoted string and an id an integer, and nothing else appears.
(read-nart-formulas dir names)nart-hl-formula.cfasl as a nart-id -> HL formula map, NART references left as
markers for expand-narts to close over once the whole table is in hand.
`nart-hl-formula.cfasl` as a nart-id -> HL formula map, NART references left as markers for `expand-narts` to close over once the whole table is in hand.
(read-table dir name count-name field-count resolvers select)The dump file name as a dump-id -> field map, checked against its stated count.
count-name names the count file separately because one dump file does not share its
stem with its count: the NART formulas are nart-hl-formula.cfasl against
nart-count.text. select picks the field to keep out of each record's fields — a
clause-struc record carries its CNF and then the assertions using it, and only the CNF
is wanted.
The dump file `name` as a dump-id -> field map, checked against its stated count. `count-name` names the count file separately because one dump file does not share its stem with its count: the NART formulas are `nart-hl-formula.cfasl` against `nart-count.text`. `select` picks the field to keep out of each record's fields — a clause-struc record carries its CNF and then the assertions using it, and only the CNF is wanted.
(records in field-count resolvers)A lazy seq of [dump-id fields] for every record in the dump file name.
field-count is how many objects follow the id — 1 for a NART formula, 2 for a
clause-struc, 5 for an assertion — and is the whole of a record's shape. A record
whose id is not an integer means the stream is out of step, which stops the read
loudly rather than skipping.
A lazy seq of `[dump-id fields]` for every record in the dump file `name`. `field-count` is how many objects follow the id — 1 for a NART formula, 2 for a clause-struc, 5 for an assertion — and is the whole of a record's shape. A record whose id is not an integer means the stream is out of step, which stops the read loudly rather than skipping.
(rename-variables x names)Replace each ?varN in x with names[N], where the plist supplied one.
Replace each `?varN` in `x` with `names[N]`, where the plist supplied one.
(variable-names plist)The authored variable names in an assertion's plist, in HL-variable-id order.
A rule's literals carry ?var0, ?var1, … and the plist carries the names the rule
was written with — ("?RELN" "?COL") — so a rule can come across reading the way
its author wrote it.
Found by shape rather than by its key. The key is an index into a symbol table
the server installs at runtime, and a dump on disk carries no such table, so the index
is all a reader has and it is not a name. The value needs no table: a list of strings
that every one begins with ? is a variable-name list and nothing else in a plist is.
The authored variable names in an assertion's plist, in HL-variable-id order.
A rule's literals carry `?var0`, `?var1`, … and the plist carries the names the rule
was written with — `("?RELN" "?COL")` — so a rule can come across reading the way
its author wrote it.
Found by **shape** rather than by its key. The key is an index into a symbol table
the server installs at runtime, and a dump on disk carries no such table, so the index
is all a reader has and it is not a name. The value needs no table: a list of strings
that every one begins with `?` is a variable-name list and nothing else in a plist is.(with-assertions dir f)Read the KB dump directory dir, call (f assertions) on a lazy seq of its
assertion maps, and close the dump after.
The three name/NART/clause tables are read whole first — they are what an assertion's
ids mean — and then assertion.cfasl streams against them, so peak memory is the
tables and not the KB. The seq is only valid inside f, which is the same contract
vaelii.foreign.cycl/with-assertions keeps.
A read f took to the end of the file is checked against the count the dump states,
and a short one throws :units/count-mismatch rather than returning a smaller KB. A
read f stopped early is not: the stated count is the whole file's, so comparing a
deliberate sample against it would make every :limit look like a desynchronized
stream.
Read the KB dump directory `dir`, call `(f assertions)` on a lazy seq of its assertion maps, and close the dump after. The three name/NART/clause tables are read whole first — they are what an assertion's ids mean — and then `assertion.cfasl` streams against them, so peak memory is the tables and not the KB. The seq is only valid inside `f`, which is the same contract `vaelii.foreign.cycl/with-assertions` keeps. A read `f` took to the end of the file is checked against the count the dump states, and a short one throws `:units/count-mismatch` rather than returning a smaller KB. A read `f` stopped early is not: the stated count is the whole file's, so comparing a deliberate sample against it would make every `:limit` look like a desynchronized stream.
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 |