vaelii.foreign.cyc — com.vaelii/vaelii-foreign 0.1.0

Translate an OpenCyc KB — the CycL assertion dump read by vaelii.foreign.cycl — into vaelii KB files, and load them.

Cyc and vaelii represent the same idea (a contextualized common-sense KB) with different spellings, so the translation is mostly a renaming plus a small table of sentence rewrites. Three things make it more than a rename:

• A role decides a term's spelling. vaelii's naming invariants encode a term's role in its symbol — a type is snake_case, a predicate camelCase, an individual CapitalCamelCase, a context ends in Context — while Cyc writes every constant CapitalCamelCase (predicates aside) and states the role as an assertion. So the role must be recovered first: pass 1 reads the whole dump and classifies every constant, pass 2 translates with that classification in hand. A constant's position is the evidence — arg 2 of isa is a collection, the head of a formula is a predicate, the microtheory slot is a context — backed by Cyc's own (isa X Collection) / (isa X Microtheory) declarations where they exist. Position is decisive because collection-hood is usually inherited in Cyc (a term is an instance of some metatype, not of Collection itself), so the explicit declarations alone would classify a fraction of the KB.

• Cyc says with a predicate what vaelii says with a record field. (isa P TransitiveBinaryPredicate) is vaelii's (transitive P); (genls A B) is (genl a b); (genlMt A B) is (genlContext AContext BContext); (arg1Isa P C) is (argIsa p 1 c); a :monotonic assertion is a {:strength :monotonic} premise. Everything without such a mapping stays an ordinary fact under its own (renamed) predicate — uninterpreted by the engine but stored, indexed and queryable, which is the honest outcome for vocabulary vaelii has no theory of.

• Some of the dump is not knowledge. SubL code (afterAdding hooks), forms the dumper could not resolve ((:nart 23227)), and assertions whose microtheory is itself unresolved are dropped, each with a counted reason. The report is part of the output: a conversion that silently dropped a tenth of the KB would look exactly like one that dropped nothing.

Output. A vaelii.foreign.corpus directory — plain vaelii sentence files, one s-expression per line, partitioned by context — with report.edn carrying the per-predicate converted/dropped counts and names.edn the Cyc constant -> vaelii term map. Cyc's :monotonic / :default marking is the corpus's strength split.

Entry points: convert! (dump -> directory) and load-dir! (directory -> kb), both also reachable from vaelii.foreign.convert's command line.

classify clj

(classify assertions)

Pass 1. Read every assertion and return {role #{constant …}} — the raw evidence, before precedence is applied. A microtheory that is itself a non-atomic term ((MtSpace (MtTimeDimFn Now)) — Cyc computes microtheories as well as naming them) is collected under :nat-context, to be minted a context symbol of its own: vaelii names a context with a symbol, so a computed one has to be reified exactly as a NAT is. A NART in a collection slot is collected under :nat-type for the same reason — vaelii writes a membership as (type Individual), so a collection Cyc computes needs a name before anything can be said to belong to it.

collection-args clj

Argument positions (1-based) whose filler must be a Cyc collection.

connectives clj

The CycL connectives vaelii writes the same way. Anything else structural makes the formula untranslatable rather than being flattened into something it does not say.

context-args clj

Argument positions whose filler must be a Cyc microtheory.

convert! clj

(convert! dump-path out-dir)

(convert! dump-path out-dir opts)

Convert the CycL dump at dump-path into a vaelii corpus under out-dir. Two passes over the dump: the first classifies every constant, the second writes the sentences. Returns the report map (also written as report.edn).

Options: :functional? imports Cyc's functional-predicate declarations as vaelii's functional (off — see metadata-metatypes); :editorial? keeps sharedNotes and myCreationPurpose (off); :code-rules? keeps the rules Cyc states in full and then implements in SubL (off — both are drop-flags); :limit reads only the first n assertions, for a quick sample.

declared-role clj

The role Cyc's own (isa X <metatype>) declares outright. Weaker evidence than position (a metatype is inherited far more often than it is stated), but it names roles position cannot — a function that never appears applied, a microtheory that never holds an assertion.

drop-flags clj

For each :filtered drop, the convert option that keeps it — or a string saying why there is none, which is the only other admissible entry.

A filtered drop is one this reader decided against on somebody else's behalf, so the person converting the KB gets to disagree. Where they cannot, that is a claim about the content and it has to be written down rather than left to the absence of a flag: SubL is executable code and vaelii has no form for code, so there is nothing to import it as and a flag would only produce a fact nobody could read.

A :code rule is the interesting one, and it is a flag rather than a justification because Cyc states the implication in full and then says it implements it in SubL instead of chaining it. The logical content is right there; whether the code does something the formula only approximates is a judgement about a particular KB, which is exactly the sort of thing a flag is for.

plugin-test/every-filtered-drop-is-either-reversible-or-explained requires an entry here for every reason drop-kinds calls :filtered, and requires each keyword to be an option vaelii.foreign.convert can actually set.

drop-kinds clj

What each of this reader's drop reasons is — see corpus/drop-kinds. A reason missing here counts as :unread.

The :filtered four are the deliberate ones: Cyc's afterAdding triggers hold SubL the engine runs rather than a claim it holds, sharedNotes and myCreationPurpose are the KB editors writing to each other, and a formula containing a SubL symbol anywhere is code however deeply it sits. Two of the four are reversible from the command line and two are not, which drop-flags says one reason at a time.

What is left in :unread is the honest remainder — a disjunction, an integrity constraint, a non-ground fact — and every one of those is a shape vaelii has no form for, not a shape this reader failed to read. :unresolved is the exception and belongs to the dump: a reference its own writer could not resolve.

excluded-predicates clj

Cyc predicates dropped wholesale, each under the reason it is dropped for — three unlike things that shared one :excluded count until the reasons were read back and nobody could tell them apart.

afterAdding / afterRemoving hold SubL code rather than knowledge; sharedNotes and myCreationPurpose are the KB editors' notes to each other; termOfUnit restates a NART's own definition, which this reader now writes itself (see nat-definitions) and vaelii would otherwise mint.

Only the editorial pair is a policy, and --editorial reverses it — see drop-flags.

function-args clj

Argument positions whose filler must be a Cyc function.

functional-metatypes clj

Cyc metatypes that map to vaelii's functional, behind :functional?.

load-dir! clj

(load-dir! kb dir)

(load-dir! kb dir opts)

Load the corpus at dir into kb — vaelii.foreign.corpus/load-dir! with this format's profiles, which is the whole of what is Cyc-specific about reading one back. See there for the options, the layering, and what a refusal count means.

logical-operators clj

CycL's connectives and quantifiers. They head formulas without being predicates, so the head-of-formula evidence must skip them.

metadata-metatypes clj

Cyc metatypes that are vaelii predicate metadata — a declaration the engine reads, not an ordinary type membership. functional is deliberately absent: Cyc's FunctionalPredicate constrains one argument position, while vaelii's functional merges a second value into the first through the equality closure, so importing the 4,332 functional declarations would rewrite terms wholesale on the strength of a mapping that is not quite the same claim. convert! takes :functional? true to import them anyway.

name-table clj

(name-table role-map nat-contexts nat-types)

The Cyc term -> vaelii term map, plus each term's role. Keyed by constant, and additionally by the whole form for the two kinds of non-atomic term that need a name of their own: a computed microtheory (a NART in the microtheory slot, minted a context symbol) and a computed collection (a NART in a collection slot, minted a type symbol, so (isa X (CityInCountryFn Canada)) has a functor to be written with).

Built in sorted order so a collision resolves the same way on every run, whatever order the dump was read in; the constants go first, so a minted name is the one that takes a suffix when it collides with a name Cyc actually wrote.

nameable-nat? clj

(nameable-nat? x)

Is x a non-atomic term this reader can mint a name for — (F a b …), a constant head over constants and literals?

Depth one only, and the reason is vaelii's, not Cyc's. A minted name is tied to its expression by (termOfUnit K E), and termOfUnit quotes: nothing inside E is reified. So a nested (CollectionIntersection2Fn (SomeFn X) Y) written into a termOfUnit keeps its inner NAT structural, while the same term reached through an ordinary argument position has its inner NAT reified first — two spellings of one expression, and the lookup that ties the name to the term misses. A term this reader cannot name is left structural, which is what it was before.

nat-definitions clj

(nat-definitions names)

(termOfUnit K E) for every computed collection in names — the sentence that ties the minted name to the expression it names.

Written into the corpus rather than left to the engine, which mints its own opaque nat/g19374: identical in behaviour, unreadable in a corpus, and different on every run — which is exactly what a diff between two converted corpora cannot see through. With the definition written, (genl (CityInCountryFn Canada) city) and (city_in_country_fn_canada CityOfEricksonCanada) are one term, and it is a term with a name somebody can look up in the source.

Computed microtheories get no such sentence. A context is only ever used as a context, where rename-term has already resolved the whole form to its symbol, so the structural spelling never reaches the engine and has nothing to be tied to.

predicate-args clj

Argument positions whose filler must be a Cyc predicate.

profiles clj

Named subsets of a corpus. :full loads everything; :ontology drops the natural-language and bookkeeping layers, which are the bulk of the corpus and none of its inference; :core keeps only Cyc's own upper vocabulary.

reader clj

This format's reader, as the seam (vaelii.impl.foreign) hands it out — declared by resources/vaelii/foreign.edn, and the whole surface a caller reaches through it.

rewrite-formula clj

(rewrite-formula names formula)

A whole CycL formula as a vaelii sentence — the connectives kept, every literal under them rewritten. Returns nil if any part has no vaelii reading.

rewrite-literal clj

(rewrite-literal names literal)

One CycL literal as a vaelii literal. This is the whole predicate mapping, and it runs on a rule's antecedents exactly as it runs on a standalone fact: a rule whose body kept Cyc's (isa ?x Dog) would never match the (dog Rover) the same translation stores. Returns nil for a literal with no vaelii reading.

role-precedence clj

[role evidence-key] in decreasing authority — the first rule that names a constant decides it.

A microtheory is never anything else. A term used as a formula head is a predicate whatever else is claimed of it, because vaelii refuses a functor that is not spelled as one: a wrong role there costs every fact about the term, while a wrong role anywhere else costs only the term's appearance. Then Cyc's own (isa X <metatype>) declarations, which are the most direct statement of role there is. Then position — a collection slot, a function slot, a predicate slot — and finally an individual by residue, Cyc's own default for a term that is neither a collection nor a relation.

roles clj

(roles evidence)

The single role each constant is given, resolving the pass-1 evidence by role-precedence.

translate clj

(translate {:keys [formula mt strength direction] :as assertion} names opts)

The vaelii sentences one CycL assertion becomes: {:sentences [...] :context C :strength s}, or {:dropped reason}. A :sentences vector rather than one sentence because a single Cyc assertion can state two vaelii things (a metadata declaration is also a type membership), and :context may be :topology for a sentence that belongs to the context wiring rather than to any one context.

A Cyc assertion is a clause, and its positive/negative literals are vaelii's own polarity, so the structural arms below are the clause shapes rather than a list of connectives that happen to be handled:

clause	CycL	vaelii
one positive literal	(P a b)	a fact
one negative literal	(not (P a b))	a fact at :false
one positive, n negative	(implies (and A B) C) / (or (not A) (not B) C)	a rule
all negative	(not (and A B))	— an integrity constraint
several positive	(or C1 C2)	— a real disjunction

The last two have no vaelii reading and are dropped under their own reasons rather than one shared :unsupported-connective, because they are refused for different reasons and only one of them is a candidate for ever being supported.

Reading the EL formula rather than the clause Cyc canonicalizes it to is deliberate: ¬A ∨ ¬B says nothing about which literal the author wrote as the conclusion, and (implies A (not B)) does. A rule direction that survives the trip is worth more than a normal form.

with-assertions clj

(with-assertions path f)

Call (f assertions) on the assertions at path, whichever form they are in.

Two things hold an OpenCyc KB and the translation reads either: the distribution's own binary dump directory (vaelii.foreign.units) and a CycL text re-dump of one (vaelii.foreign.cycl). Both yield the same {:formula :mt :strength :direction} maps, so nothing downstream of here knows which it got — and the binary one needs no external tool, which is why it is what convert! is normally pointed at.

The seq is only valid inside f; it reads from an open stream.