DKE Library — Specification

1.1 Conformance language

MUST / MUST NOT state a requirement; violating one is an error, though not always one a machine catches — §5.4 says exactly which are checked. SHOULD states a strong recommendation with a stated cost for departing. MAY states a permission. A conformant producer is any program that writes facts a published module reasons over, whether or not it uses dkepy.

2.1 Naming

• A kind name is scoped to its module: code.Function and finance.Function are different kinds and never read each other’s data.
• Kind names are CapitalizedWords. Field names are lower_snake_case.
• A producer MUST write the kind name exactly as the module declares it. Case and spelling are the whole of the matching; nothing corrects a near miss. §5.4 names the one check that catches this and the ones that do not.
• A subject identifies one thing of that kind. Subjects are the producer’s to choose, MUST be stable across loads for the same thing, and MUST be used consistently: §3.3 gives the case where a display name in a subject position silently corrupts every answer.

2.2 Value classes

A field declares one of the writable value classes of the DKE Python language — string, int, bool, and the others given in the Python Specification §5. This document adds no value classes and no coercions. A producer SHOULD write the declared class; a mismatch is not caught by any library-level check (§5.4).

2.3 Three ways a field gets its value

This distinction is load-bearing throughout §3, and getting it wrong is the most common way a store produces confident wrong answers.

A producer MUST NOT write a derived field or a rule conclusion. They are maintained for you and carry a derived provenance rather than a source, so a conclusion is always distinguishable from something you were told.

2.4 Absence is a value

Several rules in §3 read the absence of a field, not its contents. This is the sharpest edge in the library, so it is stated as a requirement rather than as advice:

A producer MUST write an absence-read field only where the thing it records is actually true, and MUST NOT write a placeholder, an empty string, or a default into one.

Writing such a field everywhere does not make a rule fire everywhere — it silences the rule everywhere, and the store then answers every question with the same list while nothing reports a fault. §3.3 names which fields these are. checkup distinguishes “nothing reaches these” from “nothing was looked for”; §4.4 says how.

3.1 What a module may declare

Five declaration forms, all of which become part of your store the moment you import the module:

A module MUST NOT contain anything else that persists. Module semantics in general — how import resolves, how namespacing works, what re-submitting does — are the language’s, in the Python Reference §9.

Every standing rule in code ranges over one kind. The language allows more — a rule may bind subjects of several kinds and relate them (Python Reference §8.8) — but code asks each of its questions of a field on the subject being asked about. That is why several fields in §3.3 look redundant: an observation another kind also records is recorded again on the side that reads it.

3.2 The published modules

Twenty-four modules are published, each served at https://dke.langsyn.com/source/<name>/ under its version, with a latest alias:

code reasons about whatever codebase you load. It describes no particular one, and it ships no facts.

3.3 code — declared fields

A producer writes these. Fields marked absence-read are governed by §2.4.

Function

Class — name: string, module: string, methods: int, language: string (optional, as on Function).

Call — caller: string, callee: string, site: string.

caller and callee MUST hold the subject of a Function, never its display name. The queries compare; they cannot tell a name from a subject. A display name here makes every function look uncalled, and nothing reports an error.

UnresolvedCall — caller: string (a Function subject), site: string, text: string (the callee as written).

A call whose target could not be named. No edge is asserted here, and a producer MUST NOT assert one. A missing edge is a known gap; a guessed edge is a wrong answer the queries cannot tell from a fact. Absent-tolerant: record none and everything else works, with dispatch_sites() returning nothing.

Rationale — subject: string (the Function or Class it explains), marker: string, text: string, site: string.

Stated, never inferred. Which comments count is the producer’s decision. Whatever convention is chosen, it SHOULD be one an author had to type on purpose: a convention wide enough to sweep ordinary comments turns every line into a fact and the query into noise.

Import — importer: string, imported: string, root: string.

Dependency — name: string, version: string, direct: bool, pinned: bool.

Counterpart — name: string, left: string, right: string, relation: string, left_covers: int, right_covers: int.

Two functions that have to agree. Stated, never inferred — agreement is a claim about intent and no call graph can see it. relation names what is being counted, because it differs per pair; left_covers and right_covers count members of that set and are comparable to each other and to nothing else. This is the one kind no producer LangSyn publishes writes (§5.2).

3.4 code — derived fields

Maintained by the engine. A producer MUST NOT write one.

Both directions of the gap are kept, each reading as a positive magnitude where it applies, because a query cannot negate a claim’s value.

3.5 code — standing rules

Each holds continuously: its conclusion is in force exactly while its condition holds over your data, and withdraws itself when the condition stops holding.

Two notes that are contract rather than commentary:

• The thresholds are values, not percentiles. > 10, > 200, > 20, > 5 select whatever your store has, and select nothing when your store has nothing. A percentile would always name someone, including in a codebase with no hub at all. They are yours to argue with; they are not adaptive.
• A rule cannot be all absences. untested and uncalled_fn carry a positive premise (lines > 0, lines >= 0) as a range, not a filter — a rule whose every premise is an absence has no set to work over and is refused.

3.6 code — queries

Called by name after import code. Every one answers over the facts you have loaded, and over nothing else.

impact_of walks to a fixed depth, not until nothing new is reached. That is a stated bound, not an approximation to be improved: the language guarantees termination and a reachability closure is not something it will run.

An empty answer is an answer. It means no loaded fact satisfies the question — which is different from the question being unanswerable, and different again from the field being empty because nobody wrote it. §4.4.

3.7 identity — declared fields

You write these; no producer in dkepy writes them.

Record

Same, Possibly, Different — each a statement, with a: string and b: string holding the names of the two records it is about. A statement’s own name carries no meaning and only keeps two statements apart.

Names are matched exactly. A name a statement uses and no Record carries is not an error: it is a record to every rule below. unrecorded() (§3.9) lists such names.

3.8 identity — standing rules

Each holds continuously: its conclusion is in force exactly while its condition holds over your data, and withdraws itself when the condition stops holding. Four rules conclude a relation, a three-segment path read as SameEntity.x.y, rather than a field.

Four notes that are contract rather than commentary:

• The relations are not namespaced. SameEntity and PossiblySame are read by those bare names in every unit, and are never identity.SameEntity. A unit that declares a class of either name reads its own class by that name.
• SameEntity is closed; PossiblySame is not. A record in any chain of Same statements is related to every record the chain reaches, itself included. A possibility relates exactly the two records a statement names.
• A Different statement withdraws nothing. It and every Same statement it contradicts stand together; the contradiction is concluded, not resolved.
• The closure is quadratic in an entity. An entity of n records holds n² SameEntity conclusions.

3.9 identity — queries

Called by name after import identity. Every one answers over the facts you have loaded, and over nothing else.

3.10 argument — declared fields

You write these; no producer in dkepy writes them.

Claim

Support, Attack, Weakening — each a statement, with by: string naming the claim that supports, attacks or weakens, and target: string naming the claim it bears on. A statement’s own name carries no meaning and only keeps two statements apart. A statement bears on nothing until both fields are written.

Names are matched exactly. A name a statement uses and no Claim carries is not an error: it is a claim to every rule below. unrecorded() (§3.12) lists such names.

3.11 argument — standing rules

Each holds continuously: its conclusion is in force exactly while its condition holds over your data, and withdraws itself when the condition stops holding.

Four notes that are contract rather than commentary:

• Two steps, then silence. A claim is unattacked, undefended or reinstated, or it is named by none of the three: it is open. Claims that attack one another, and the claims such a chain reaches, are open. No answer says an open claim falls.
• A weakening decides nothing. It concludes weakened and takes part in no other rule.
• A support is not a defence. It takes part only in premise_attacked.
• No relation is concluded. Every field argument derives is on one of its own kinds.

3.12 argument — queries

Called by name after import argument. Every one answers over the facts you have loaded, and over nothing else. Each answers a sorted list of names.

3.13 agenda — declared fields

You write these; no producer in dkepy writes them.

Goal

Commitment

Obligation

Prohibition

Names are matched exactly. A name a commitment serves and no Goal carries is not an error: it is a goal to every rule below. unrecorded() (§3.15) lists such names.

3.14 agenda — standing rules

Each holds continuously: its conclusion is in force exactly while its condition holds over your data, and withdraws itself when the condition stops holding.

Two standing constraints are reported by checkup and refuse no write. nothing_forbidden_committed is violated by each Commitment that is forbidden and has no done_at, and nothing_forbidden_owed by each such Obligation.

Four notes that are contract rather than commentary:

• No rule reads the present. Every rule compares recorded values with each other. What depends on the time is a query, and takes the time as at.
• A prohibition is not enforced. It concludes forbidden and violates a constraint; it removes and refuses nothing.
• late needs both dates. An item with no done_at, or no due, is never late, whatever the time.
• No relation is concluded. Every field agenda derives is on one of its own kinds.

3.15 agenda — queries

Called by name after import agenda. Every one answers over the facts you have loaded, and over nothing else. Each answers a sorted list except previous_dues, which keeps the order the dates were given. A commitment is named Commitment.<name> and an obligation Obligation.<name>. An item is open at at when it has no done_at, or its done_at is later than at.

3.16 quantum — declared fields

quantum has two halves that share nothing but the subject. The simulation half declares one kind, State, and is otherwise functions over values (§3.18). The reasoning half declares the rest. dke.quantum.device (§4.5) writes Device, PhysicalQubit and Native; dke.quantum.provenance writes Result and a circuit’s digest; the module records its own Op facts when it is imported. You write the rest.

State

Gate

Qubit

Coupler

Op

The module records qubits and diagonal for h, x, y, z, s, t, rx, ry, rz, cnot, cz, sx, id, ecr, swap and rzz when it is imported, under the source quantum. Record another operation the same way.

Device

PhysicalQubit

Native

Circuit

Result

Names are matched exactly. A qubit is compared by its name and is never bound as a subject, since a compiled circuit names its qubits by number.

3.17 quantum — standing rules

Each holds continuously: its conclusion is in force exactly while its condition holds over your data, and withdraws itself when the condition stops holding. The rules over two gates relate only gates of one circuit: a gate’s circuit is its track, and the gates that name no circuit share the empty track.

Two standing constraints are reported by checkup and refuse no write. every_pair_coupled is violated by each Gate that is uncoupled, and every_gate_legal by each Gate that is illegal.

Five notes that are contract rather than commentary:

• Four relations are concluded. RunsBefore, MustPrecede and CommutesWith relate two gates, the earlier first, and RunsAs relates a gate to the native operation it runs as. Every other conclusion is a field of a Gate or a Result. The queries of §3.18 read the relations.
• A gate is judged by one set of rules. A gate whose circuit names a device is judged by the device’s own qubits and operations, and uncoupled never holds for it. A gate whose circuit names no device is judged by the couplers alone.
• A device with no facts runs nothing. A circuit naming a device the store holds no facts for has every gate off_device and not_native, which is also how a misspelt device name shows itself.
• A digest holding two values holds the result through neither. When two sources disagree about a digest, every comparison with the other value concludes its reason, and the result does not hold.
• No rule reads the present. What depends on the time is a query, and takes the time as at.

3.18 quantum — queries

Called by name after import quantum. Qubit q is bit q of an amplitude’s index, so qubit 0 is the lowest bit; a state of n qubits is a list<complex> of 2ⁿ amplitudes. A step, as advance, advance_chacha, overlap, clifford, rev_code, rev_same and rev_meets take one, is a tuple of a gate’s name, the qubits it acts on and an angle that only the rotations read, or ("measure", [q], 0.0); a reversible circuit’s steps are x, cnot, ccx, z, cz, ccz, swap and cswap, with a theta of 0.0, and ("mx", [q], 0.0), which measures q in the X basis and leaves it 0, with the controlled forms x_if, cnot_if, ccx_if, z_if, cz_if, ccz_if, swap_if and cswap_if, which take the measured qubit first and then the gate’s own qubits.

The functions over a state read and write no fact:

These read or write a state kept in the store as State.<name>:

These answer over the facts you have loaded, each a sorted list:

3.19 pqc — declared fields

dke.pqc.cbom (§4.5) writes an algorithm’s quantum and strength and a use’s system and algorithm from a cryptographic bill of materials. You write the rest. Every year is a calendar year, written as an int, and every boundary is the first year WITHOUT something.

Horizon

Algorithm

Data

System

Deadline

Use

3.20 pqc — derived fields

migrate_by is the first year the use must no longer rely on its algorithm, and start_by the last year to start moving it.

3.21 pqc — standing rules

Each holds continuously, as in §3.17.

Two standing constraints are reported by checkup and refuse no write. no_late_plan is violated by each Use that is late, and no_missed_deadline by each Use that misses.

Two notes that are contract rather than commentary:

• Disagreement is reasoned about, not resolved. When two sources give a field two values, every value is reasoned about: a use is late or misses a deadline if any value on record makes it so, and its deadline is the earliest year of any value of any deadline that covers it, one source’s year. unsettled() names each such use, by its own fields and the horizon, shelf life and migration time it is reasoned about with; a deadline’s year is not among them, and why on the use’s deadline names the year that placed it.
• No rule reads the present. A question that depends on the year takes it as at.

3.22 pqc — queries

Called by name after import pqc. Every one answers use names, sorted, except priority, which answers them in order.

3.23 harmony — declared fields

The five writing scripts of §3.26 write Voice, Key, Degree, Note, Bar and Tone under the source "harmony", and you may write the same fields yourself. A pitch is a MIDI note number: 60 is middle C and each step is a semitone. A pitch class is a pitch taken within the octave, 0 for C up to 11 for B. A beat is one chord, numbered from 1 in order. Rhythm is counted in a unit you choose, such as a sixteenth, from 0 at the start of the piece.

Voice

Key

Degree

Note

Fifths, Octaves and Crossing declare no field. Each is a relation between two notes, Fifths.a.m for notes a and m, concluded by the rules of §3.25 and never written. They are declared so that reading one that does not stand answers empty.

Bar

Tone

3.24 harmony — derived fields

% takes the sign of its right side, as in Python, so i1 to i3 are always 0 to 11. That is an interval within the octave, a compound interval counting as its simple form: 7 is a fifth or a twelfth, and 0 a unison or an octave. A note that has crossed below the voice it is compared with reads the interval the other way up.

3.25 harmony — standing rules

Each holds continuously, as in §3.17. A rule over two or three Notes binds them as a, c and m, or as b for a chord’s bass note, in the order the cell names them.

harmony declares no standing constraint. Four notes that are contract rather than commentary:

• Consecutive means both voices move. A fifth or an octave held by one voice while the other leaps is not marked. Fifths and octaves in contrary motion are marked, and so is a twelfth followed by a fifth.
• A chord takes every reading inside it. Each chord rule reads exactly the intervals it names, so a dominant seventh is also a major triad, a chord with both a major and a minor third above its bass is read as both, and a chord of no shape named here has no reading.
• Disagreement is reasoned about, not resolved. When two sources give a field two values, every value is reasoned about, and a mark stands if any value on record makes it so. A fold reads every value too, so a tone whose duration a second source writes, even the same duration, would be added twice to its bar’s filled; tones and claims count the tones and their claims over the one binding the fold reads, and while the claims are more, the bar is disputed and no filled is concluded for it. A tone with no duration is in neither count, and a tone whose onset holds two values starts in each bar it names, each of those fills being one source’s. The rules that ask for something to be missing are answered for the note rather than for each value: chromatic holds of a note only when no value of its pc is a degree of its key, and major_open, minor_open and seventh_open read a chord only when no value on record supplies the interval they leave out.
• No rule hears the music. Every rule compares numbers. What the rules do not check is listed in the Library Reference: hidden fifths and octaves, doubling, resolution, melodic intervals and more than four voices.

3.26 harmony — queries

Called by name after import harmony. Only filled_of refuses because sources disagree, and only a disputed bar: otherwise a reader answers one value by the rule its row states, and unsettled() names what is in disagreement.

3.27 physics — declared fields

The writing scripts of §3.30 write Quantity, Factor, Resistor and Group under the source "physics", and Unit under the source each is given, and you may write the same fields yourself. A unit is named by letters, digits and underscores, such as "N", "lbf_s" or "m_per_s2". Its dimension is the powers of five base dimensions it is made of: mass, length, time, electric current and temperature. A newton, a kilogram metre per second squared, is mass 1, length 1 and time -2. A unit’s factor is what one of it is in the SI unit of the same dimension. A unit whose zero is not SI’s, such as a degree Celsius, is not a factor and is not written. An equation is checked as a product of powers: write every power on its left side positive and every power on its right side negative, so F = m a is F to the 1, m to the -1 and a to the -1.

Unit

Quantity

Factor

Equation

Resistor

Group

3.28 physics — derived fields

Quantity.si is the quantity’s value in the SI unit of its dimension, and converted its value in the unit it expects. converted takes the ratio of the two factors first, so a value expected in its own unit comes back as it was, and it is a real wherever the value in the expected unit is one, for any factors from 10^-150 to 10^150. Each is absent until the rules have concluded the fields it reads, so a quantity in a unit the list does not hold has neither. A factor’s s fields are its share of each base dimension, and an equation sums them. A resistor’s siemens is its conductance, and a group’s parallel is the resistance of a parallel group, the reciprocal of the conductances its resistors sum to.

3.29 physics — standing rules

Each holds continuously, as in §3.17. A rule over a Quantity and a Unit binds them as q and u, a rule over a Factor as f, an Equation as e, a Group as g and a Resistor as r.

physics declares no standing constraint. Five notes that are contract rather than commentary:

• Only a unit in the list is reasoned about. A quantity in a unit no Unit names gets no factor, no dimension and no si; it is marked unknown, and checks() names it. An equation with a factor in such a unit is judged neither consistent nor unbalanced.
• Consistent is not true. A consistent equation has the same dimensions on both sides. It is not thereby a law: E = m v and E = m v² differ in dimension, but E = m v² and E = 2 m v² do not.
• Disagreement is reasoned about, not resolved. When two sources give a field two values, every value is reasoned about, and unsettled() names the fact.
• A sum is not drawn from a member bound to it twice. A sum reads every value of what it sums, so a factor whose share two values give, or a resistor whose ohms a second source writes, even the same ohms, would be added twice, a result no circuit or equation has. The _factors, _resistors and _claims fields count the members and their claims over the one binding the sum reads, and while the claims are more, the sum is disputed and not concluded, nor anything that rests on it. A member with no value of the sum is in neither count, so it hides no dispute. A factor whose equation, or a resistor whose group, holds two values counts in each it names, and each of those sums is one source’s.
• No rule reads the physics. Every rule compares or adds numbers. Whether an equation is true, whether a quantity is plausible and whether a circuit is built of series and parallel groups are not asked.

3.30 physics — queries

Called by name after import physics. Only resistance refuses because sources disagree, and only a disputed group: otherwise a reader answers one value by the rule its row states, and unsettled() names what is in disagreement. The writers and readers of the first two groups are the interface to the facts; the third group computes values from its arguments and writes nothing.

3.31 chemistry — declared fields

The writing scripts of §3.34 write Element, Atom, Bond, Species and Term under the source "chemistry", except element() and elements(), which write Element under the source "CIAAW"; you may write the same fields yourself. A weight is a standard atomic weight, or a sum of them, in g/mol. A valence is the number of bonds an element usually forms in an organic molecule, and 0 for an element that forms none there. A bond order is 1, 2 or 3. An enthalpy of formation is in kJ/mol at 298.15 K, and a reaction’s enthalpy in kJ. Hydrogens are never written: an atom carries the hydrogens its valence leaves over (§3.33).

Element

An Element is named by its symbol. elements() writes these thirteen:

Atom

Bond

A Bond is half a bond. bond() writes both halves, named a-b and b-a, so that each atom reaches the other.

Molecule

A Molecule is named by the molecule its atoms give, and declares no field you write.

Species

Term

A Term is named by term() for its reaction and species, reaction, - and species.

Reaction

A Reaction is named by you, and declares no field you write.

3.32 chemistry — derived fields

hydrogens is what the atom’s valence leaves over after its bonds: an atom with no bond carries its whole valence, as the oxygen of water and the carbon of methane do. It is negative for an atom bonded past its valence, and overbonded marks that atom (§3.33). mass is the atom’s weight with those hydrogens. An atom of an element that has not been written has no valence, no hydrogens and no mass. An atom of an element of valence 0, a metal, takes its own bonds as its valence (§3.33), so it carries no hydrogens and its mass is its weight.

3.33 chemistry — standing rules

Each holds continuously, as in §3.17. A rule over an Atom and a Bond binds them as a or c, o or n, and x or y, in the order the cell names them. A functional group is concluded on the atom that carries it: the carbonyl carbon of an acid, an ester, an amide, an aldehyde and a ketone, the oxygen of an alcohol, and the nitrogen of an amine.

chemistry declares no standing constraint. Six notes that are contract rather than commentary:

• Hydrogens are concluded, not written. The structure is a graph of the heavy atoms and the bonds between them, as a skeletal drawing is. Each atom carries the hydrogens its valence leaves over, and an atom with no bond carries its whole valence. Nothing is concluded until the element is written: before elements() is called, or for a symbol with no Element, an atom has no valence, no hydrogens and no mass, and weight() answers 0.0 for a molecule none of whose atoms has one. An atom of an element of valence 0 takes its own bonds as its valence, so a metal carries no hydrogens and adds its weight to its molecule’s.
• A group takes every reading inside it. Each group rule reads exactly the bonds it names, so an atom that fits two rules carries both groups, and an atom that fits none carries none. A nitrogen is read as an amine only while every bond it has is single, so the nitrogen of a nitrile or an imine carries no group.
• A molecule’s formula and weight are sums over its atoms. Molecule.hydrogens adds the hydrogens of every atom, and an overbonded atom adds a negative number. overbonded and faults() name it.
• A reaction’s enthalpy is the sum over the terms the store holds. A term whose species has no formation adds nothing, and the reaction is incomplete: its enthalpy is the sum of the terms that have one.
• Disagreement is reasoned about, not resolved. When two sources give a field two values, every value is reasoned about, and unsettled() names the fact.
• A sum is not drawn from a member bound to it twice. A sum reads every value of what it sums, so a sulfur atom whose element’s weight holds two values would be weighed at both, and a bond whose order a second source writes, even the same order, counted twice. The _halves, _atoms, terms and _claims fields count the members and their claims over the one binding the sum reads, and while the claims are more, the sum is disputed and not concluded, nor anything that rests on it. An atom whose bonds are disputed has no hydrogens or mass, so it disputes its molecule’s weight and hydrogens rather than leave them. A member with no value of the sum is in neither count, so it hides no dispute. An atom whose molecule, a bond whose a or a term whose reaction holds two values counts in each it names, and each of those sums is one source’s.

3.34 chemistry — queries

Called by name after import chemistry. The first six write facts and answer nothing. The next eight read what the rules concluded; a read refuses only what is disputed, as its cell states, and otherwise answers by the rule its cell states, and unsettled() names what is in disagreement. The last thirteen are value scripts that return a value and write nothing.

3.35 biology — declared fields

The four writing scripts of §3.37 write Compound, Reaction, Family and Person under the sources "medium", "network" and "pedigree", and you may write the same fields yourself. A compound and a reaction are named by you, and so are a family and a person; a reaction’s s1, s2, p1 and p2, a person’s family, mother and father, and a family’s name in Person.family are each the name of another subject. A medium is what a growth medium supplies. A scope is every compound the network can make from it. A mode is how the trait a family is recorded for is inherited: "autosomal dominant", "autosomal recessive" or "X-linked recessive".

Compound

Reaction

Family

Person

Parent and Ancestor declare no field. Each is a relation between two people, Parent.c.p for a child c and a parent p, and Ancestor.x.y for a person x and an ancestor y, concluded by the rules of §3.36 and never written. They are declared so that reading one that does not stand answers empty.

3.36 biology — standing rules

Each holds continuously, as in §3.17. A rule over several subjects binds them as the cell names them: a compound as a, b or c, a reaction as r, a family as y, and a person as c for a child, m for a mother, f for a father, p for a parent and x, y and z along a line of descent.