One function library for RIF-DTB, XPath, XSLT and SPARQL#

Date: 2026-09-07. Branch wt/rif-dtb. Tracking: https://github.com/danbri/factoidal/issues/664

Owner, 2026-09-07, verbatim: "it looks like we should implement all of the latest version of RIF-DTB. Do so in a way that assures us of its integrity using Lean theorems (and F* equiv is possible) and aim for tight integrations with other pieces of Factoidal - from XSLT/XPath/XML to SPARQL."

Specifications:

• RIF-DTB 1.0, 2nd Edition — the built-in names, their signatures, their symbol spaces and their error conditions.
• XQuery 1.0 and XPath 2.0 Functions and Operators — the SEMANTICS. RIF-DTB defines almost every built-in by citing an F&O function; SPARQL 1.1 §17 cites the same ones; XPath 1.0 §4 predates them and defines its own, which agree on some and differ on others.
• XML Schema Part 2: Datatypes — the value spaces every one of these functions computes over.

1. The problem this record answers#

The same F&O function is written more than once in the Lean tree today. Three front ends carry their own copy of the string and numeric semantics:

XSD/Datatypes.lean already carries the value spaces, the lexical mappings, the canonical mappings and the orders (Dec, DTValue, DurValue, parseDateTimeLex, parseDurationLex, timeOnTimeline, dtCompare, durCompare, canonicalDateTime, canonicalDuration). What is missing is a layer ABOVE it: the F&O functions themselves.

Design: L4Factoidal/Fn/ holds the F&O semantics once, over the XSD.Datatypes value spaces. RIF, SPARQL and XPath become signature layers — each keeps its own argument typing, its own coercions and its own error discipline, and none of them reimplements the function.

The XPath 1.0 number grammar (XPath/Number.lean) is NOT consolidated. XPath 1.0 §3.5 defines its own lexical space and its own IEEE 754 double semantics; that is a different specification, not a duplicate of XSD's, and the 2026-09-07 XSD audit §8 already records it as out of scope.

2. The complete RIF-DTB built-in list#

Counted from RIF-DTB 1.0 2nd Edition section 4. "Today" is the state of L4Factoidal/RIF/Builtins.lean at commit 709f3c49c.

The header comment in RIF/Builtins.lean says "RIF-DTB defines 197 built-ins". That figure was never sourced; 236 is the count of the names listed in section 4 of the specification, and it is what this record uses.

2.1 Names the specification and the corpus disagree on#

• DTB 4.5.1 names func:numeric-mod. Every fixture in third_party/testing/rif-core-suite writes func:numeric-integer-mod. Both names are accepted, and the second is noted as the corpus spelling.
• Builtins_Time-premise.rifps writes External( func:add-dayTimeDuration-to-dateTime(...) ) = "2000-11-02T12:27:00"^^xs:dayTime. There is no xs:dayTime datatype. It is a typo for xs:dateTime in the Approved fixture. The F* tree skips the whole test rather than decide it. This work decides the test and records the accommodation at its single site (RIF/Builtins.lean, xsdFamily), naming the fixture line.

3. The inventory, function by function#

Column (a) is the F&O function RIF-DTB cites; (b) is where the same semantics already existed in the Lean tree before this work; (c) is the XSD value space it computes over.

4.1 / 4.2 / 4.3 — literal comparison and the guards#

The two guards missing before this work are pred:is-literal-time / -not-time reaching a time lexical space that CSVW.parseCanonicalDate does not model, and dateTimeStamp (a dateTime with the timezone REQUIRED). Both are decided by XSD.parseDateTimeLex.

4.4 — casting#

4.5 — numeric#

4.6 — boolean#

4.7 — strings#

4.8 — dates, times and durations#

Before this work: func:subtract-dateTimes and func:days-from-duration only, written against a private dateTimeSecsOfLex that reads a four-digit year and treats an absent timezone as UTC. The other 70 names were absent and Builtins_Time was undecided in both trees.

All 72 are cited by RIF-DTB from F&O 10.5 (accessors), 10.6 (duration arithmetic), 10.7 (date/time arithmetic), 10.8 (date/time subtraction) and 10.4 (comparison). They compute over XSD.DTValue (§3.3.7's seven-property model) and XSD.DurValue (§3.3.6's two-property model), and their results are written back through XSD.canonicalDateTime and XSD.canonicalDuration.

4.9 / 4.10 — XMLLiteral and PlainLiteral#

4.11 — lists#

All 16 were already present (listIndex, dedup and the evalFunc cases). They are RIF-specific: F&O's sequence functions are the model, but a RIF list is a term, not a sequence, so the correspondence is by analogy only. They move to Fn/List.lean as polymorphic functions over List α with BEq α, which is what makes them reusable by a SPARQL or XPath sequence layer later.

4. Where the three specifications genuinely disagree#

These are not defects to reconcile. Each is a stated difference between two W3C Recommendations, and each gets a named theorem with the input that witnesses it.

1. substring, three ways. F&O fn:substring is 1-based and keeps every position p with start <= p < start + length, with start and length rounded as xs:double. SPARQL SUBSTR (§17.4.3.3) cites fn:substring but takes xs:integer arguments. XPath 1.0 §4.2 substring() rounds its double arguments with round() and has the same window rule. The RIF Core Approved Builtins_String fixture additionally asserts substring("foobar" 3) = "bar", which is 0-BASED — the 2-argument and 3-argument forms in that fixture disagree with each other on the base, and the fixture is the authority for the RIF front end.
2. Language-range matching. pred:matches-language-range is RFC 4647 §3.3.2 EXTENDED filtering (wildcards inside the range). SPARQL langMatches is §3.3.1 BASIC filtering. Witness: tag de-Latn-DE, range de-*-DE — extended matches, basic does not.
3. Error versus empty. F&O raises a dynamic error; SPARQL §17.2 makes the expression an error that a FILTER reads as false; XPath 1.0 has no error value at all and returns the empty string or NaN; RIF-DTB leaves the built-in with no value, which RIF/Builtins.lean reports as unknown so the rule does not fire. The library returns Option; each front end maps none to its own discipline.
4. concat arity. fn:concat and SPARQL CONCAT are variadic over the whole argument list; XPath 1.0 concat() requires at least two arguments.
5. Timezone defaulting. F&O 10.7 uses an implicit timezone from the evaluation context. RIF-DTB 4.8 has no context, so an absent timezone is read as UTC. The library takes the implicit offset as a parameter and the RIF front end passes zero.

5. Module layout#

6. What was found while writing the library#

Two defects, both from the same wrong assumption: that Lean 4's Int / truncates toward zero. It is EUCLIDEAN — (-7) / 2 is -4 and (-7) % 2 is 1.

1. XSD.daysFromCivil was one day short for every year in [-399, -1]. Hinnant's days_from_civil takes the era with a TRUNCATING division and writes y' - 399 to emulate a floor. Written with Lean's /, the adjustment fires a second time. Found by the round-trip #guard between Fn.DateTime.civilFromDays and XSD.daysFromCivil on -44-03-15; fixed with Int.tdiv. Every date/time comparison and every timeOnTimeline for a BCE date read the wrong instant before this. No vendored fixture has a negative year, which is why 18,951 of 18,956 datatype tests passed over it.
2. func:numeric-divide floored where F&O §6.2.4 truncates. The comment above divDec in RIF/Builtins.lean asserted the opposite of what the code did. divDec "-1" "3" gave -0.333333333333333334. Fixed with Int.tdiv, with a #guard on both signs.

Both are the shape anti-pattern #28 names: a comment stating a property of a primitive is evidence about the comment, not about the primitive. Fn/Numeric.lean now pins all four division directions as examples, so the next reader does not have to take anyone's word for it.

7. Status (measured 2026-09-07 in /Users/danbri/working/factoidal-wt-dtb)#

Every number below was produced by running the probe in this worktree, before and after, not quoted from a dashboard.

The l4xsd-datatypes score not moving is the expected result of the daysFromCivil repair, not evidence against it: no vendored instance file in that suite carries a negative proleptic year, so the suite cannot see the defect in either direction. The #guard in Fn/DateTime.lean is what sees it.

Not a gate here, and reported without a claim: the superseded SPARQL 1.0 evaluation manifest gives 208 pass, 74 fail (out of 282). No baseline for it is recorded anywhere in the repository, so this run establishes one rather than measuring a change.

Hygiene: #print axioms over all 27 theorems of L4Factoidal.Fn gives propext, Classical.choice, Quot.sound or fewer. No sorry, no user axiom, no native_decide, no unsafe. partial def count across L4Factoidal is 170, down from the 172 baseline.

Builtins_Time was undecided in BOTH trees for lack of DTB §4.8. It is now decided and passes. The 2 remaining undecided cases are Modeling_Brain_Anatomy and Non-Annotation_Entailment, both blocked on an OWL entailment regime rather than on a built-in (#665).

The QT3 Functions-and-Operators suite is NOT vendored#

The task brief allowed vendoring w3c/qt3tests shallow if it is under 300 MB. It was not vendored, and the reason is the disk rather than the licence: this machine ran to 162 MB free during the session with five worktrees live, and a new submodule plus its build products is exactly the thing that filled it. No QT3 number is reported, and none is estimated. The executable evidence for the shared functions is the #guard set in each Fn module (the F&O examples and the RIF corpus's own equations) plus the five suites above.

Still open#

• The numeric lexical spaces still route through CSVW.isXsdNumericLexical at the RIF call site rather than through XSD.lexicalMap. That move changes ACCEPTANCE and its gate is the SPARQL suites, so it is commit 7 of docs/designissues/2026-09-07-xsd-datatypes-audit.md §8 and not this work.
• civilFromDays and daysFromCivil are shown mutually inverse by #guard on eight dates, not by a theorem for every year.
• LWS/Operations.lean keeps a third civilFromDays for HTTP-date formatting. It is a different specification's formatter and moving it is a separate commit with its own gate.
• SPARQL's valueCompare still orders same-datatype xs:dateTime literals by LEXICAL string rather than by XSD.dtCompare. Fn.DateTime.compare is now available to it; the repair is commit 8 of the XSD audit plan.