From 1e52414e8e794b0bcf06134c7d1d783293c96c2c Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 8 Jun 2026 12:00:10 +0200 Subject: [PATCH 1/4] missing page: display functors with missing data + undistinguishable functors pairs --- src/routes/missing/+page.server.ts | 49 +++++++++++++++++++++++-- src/routes/missing/+page.svelte | 58 ++++++++++++++++++++++++++++-- 2 files changed, 101 insertions(+), 6 deletions(-) diff --git a/src/routes/missing/+page.server.ts b/src/routes/missing/+page.server.ts index b180a168..30e10f65 100644 --- a/src/routes/missing/+page.server.ts +++ b/src/routes/missing/+page.server.ts @@ -11,6 +11,8 @@ export const load = async () => { [ StructureShort & { count: number }, StructureShort & { count: number }, + StructureShort & { count: number }, + StructurePair, StructurePair, ] >([ @@ -26,7 +28,19 @@ export const load = async () => { GROUP BY c.id ORDER BY lower(c.name); `, - // missing special morphisms + // functors with unknown properties + sql` + SELECT f.id, f.name, COUNT(*) AS count + FROM functors f + INNER JOIN functor_properties p + LEFT JOIN functor_property_assignments fp + ON fp.functor_id = f.id + AND fp.property_id = p.id + WHERE fp.property_id IS NULL + GROUP BY f.id + ORDER BY lower(f.name); + `, + // categories with missing special morphisms sql` SELECT c.id, c.name, COUNT(*) AS count FROM categories c @@ -58,17 +72,43 @@ export const load = async () => { END ) = 0; `, + // undistinguishable functor pairs + sql` + SELECT + f1.id AS id1, f1.name AS name1, + f2.id AS id2, f2.name AS name2 + FROM functors f1 + JOIN functors f2 + ON f1.id < f2.id + JOIN functor_properties p + LEFT JOIN functor_property_assignments a1 + ON a1.functor_id = f1.id AND a1.property_id = p.id + LEFT JOIN functor_property_assignments a2 + ON a2.functor_id = f2.id AND a2.property_id = p.id + GROUP BY f1.id, f1.name, f2.id, f2.name + HAVING SUM( + CASE + WHEN a1.is_satisfied IS a2.is_satisfied THEN 0 + ELSE 1 + END + ) = 0; + `, ]) if (err) error(500, 'Failed to load data') const [ categories_with_unknown_properties, + functors_with_unknown_properties, categories_with_missing_morphisms, undistinguishable_category_pairs, + undistinguishable_functor_pairs, ] = results - const total_unknown_pairs = categories_with_unknown_properties.reduce( + const total_unknown_category_property_pairs = + categories_with_unknown_properties.reduce((total, item) => item.count + total, 0) + + const total_unknown_functor_property_pairs = functors_with_unknown_properties.reduce( (total, item) => item.count + total, 0, ) @@ -79,9 +119,12 @@ export const load = async () => { return { categories_with_unknown_properties, - total_unknown_pairs, + total_unknown_category_property_pairs, + functors_with_unknown_properties, + total_unknown_functor_property_pairs, categories_with_missing_morphisms, undistinguishable_category_pairs, + undistinguishable_functor_pairs, missing_combinations, } } diff --git a/src/routes/missing/+page.svelte b/src/routes/missing/+page.svelte index c4742601..6f7512a8 100644 --- a/src/routes/missing/+page.svelte +++ b/src/routes/missing/+page.svelte @@ -24,13 +24,39 @@

There are {data.categories_with_unknown_properties.length} categories where at least - one property is unknown. In total, there are {data.total_unknown_pairs} unknown (category, - property)-pairs. + one property is unknown. + + {#if data.total_unknown_category_property_pairs > 0} + In total, there are + {data.total_unknown_category_property_pairs} + unknown (category, property)-pairs. + {:else} + 🎉 + {/if}

+
+

Functors with unknown properties

+ +

+ There are {data.functors_with_unknown_properties.length} functors where at least one + property is unknown. + + {#if data.functors_with_unknown_properties.length > 0} + In total, there are + {data.total_unknown_functor_property_pairs} + unknown (functor, property)-pairs. + {:else} + 🎉 + {/if} +

+ + +
+

Categories with unknown special morphisms

@@ -69,8 +95,34 @@
{/if} +{#if data.undistinguishable_functor_pairs.length > 0} +
+

Undistinguishable functor pairs

+ +

+ There are {data.undistinguishable_functor_pairs.length} pairs of functors that cannot + be distinguished by the properties currently recorded in the database. This indicates + that the data may be incomplete or that a distinguishing property may be missing. +

+ + +
+{/if} +
-

Missing combinations

+

Missing category combinations

Among the consistent combinations of the form p ∧ ¬q, the following are From de06ace1ded2bf7a9ea5394b4f4a8455c3f52d82 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 8 Jun 2026 12:10:46 +0200 Subject: [PATCH 2/4] load and display missing functor combinations --- src/lib/server/consistency.ts | 27 ++++++++++++-------- src/routes/missing/+page.server.ts | 13 +++++++--- src/routes/missing/+page.svelte | 40 ++++++++++++++++++++++++++---- 3 files changed, 61 insertions(+), 19 deletions(-) diff --git a/src/lib/server/consistency.ts b/src/lib/server/consistency.ts index fbf94cdf..23732d27 100644 --- a/src/lib/server/consistency.ts +++ b/src/lib/server/consistency.ts @@ -1,4 +1,3 @@ -import sql from 'sql-template-tag' import { query } from '$lib/server/db.catdat' import { is_subset } from './utils' import type { SqliteError } from 'better-sqlite3' @@ -110,28 +109,34 @@ function build_shortest_proof( return proof } -export function get_missing_combinations() { - const { implications, err: err_imp } = get_normalized_implications('category') +export function get_missing_combinations(type: StructureType) { + const { implications, err: err_imp } = get_normalized_implications(type) if (err_imp) return { err: err_imp, missing_combinations: [] } const { rows: properties, err } = query<{ id: string dual_property_id: string | null - }>(sql`SELECT id, dual_property_id FROM category_properties ORDER BY lower(id)`) + }>({ + sql: `SELECT id, dual_property_id FROM ${type}_properties ORDER BY lower(id)`, + values: [], + }) if (err) return { err, missing_combinations: [] } const { rows: existing, err: err_existing } = query<{ p: string q: string - }>(sql` - SELECT DISTINCT cp.property_id AS p, cnp.property_id AS q - FROM category_property_assignments cp - INNER JOIN category_property_assignments cnp - ON cp.category_id = cnp.category_id - WHERE cp.is_satisfied = TRUE AND cnp.is_satisfied = FALSE - `) + }>({ + sql: ` + SELECT DISTINCT a.property_id AS p, an.property_id AS q + FROM ${type}_property_assignments a + INNER JOIN ${type}_property_assignments an + ON a.${type}_id = an.${type}_id + WHERE a.is_satisfied = TRUE AND an.is_satisfied = FALSE + `, + values: [], + }) if (err_existing) return { err: err_existing, missing_combinations: [] } diff --git a/src/routes/missing/+page.server.ts b/src/routes/missing/+page.server.ts index 30e10f65..6467115a 100644 --- a/src/routes/missing/+page.server.ts +++ b/src/routes/missing/+page.server.ts @@ -113,9 +113,15 @@ export const load = async () => { 0, ) - const { missing_combinations, err: err_missing } = get_missing_combinations() + const { missing_combinations: missing_category_combinations, err: err_cat_missing } = + get_missing_combinations('category') - if (err_missing) error(500, 'Failed to load missing combinations') + if (err_cat_missing) error(500, 'Failed to load missing category combinations') + + const { missing_combinations: missing_functor_combinations, err: err_fun_missing } = + get_missing_combinations('functor') + + if (err_fun_missing) error(500, 'Failed to load missing functor combinations') return { categories_with_unknown_properties, @@ -125,6 +131,7 @@ export const load = async () => { categories_with_missing_morphisms, undistinguishable_category_pairs, undistinguishable_functor_pairs, - missing_combinations, + missing_category_combinations, + missing_functor_combinations, } } diff --git a/src/routes/missing/+page.svelte b/src/routes/missing/+page.svelte index 6f7512a8..fabf5893 100644 --- a/src/routes/missing/+page.svelte +++ b/src/routes/missing/+page.svelte @@ -125,18 +125,20 @@

Missing category combinations

- Among the consistent combinations of the form p ∧ ¬q, the following are - not yet witnessed by a category in the database or its dual category. If some of - these combinations are + Among the consistent category combinations of the form p ∧ ¬q, the + following are not yet witnessed by a category in the database or its dual + category. If some of these combinations are inconsistent, this indicates that some implication is missing.

- Show all {data.missing_combinations.length} combinations + + Show all {data.missing_category_combinations.length} combinations +
    - {#each data.missing_combinations as [p, q]} + {#each data.missing_category_combinations as [p, q]}
  • {p} ∧ ¬{q}
+
+

Missing functor combinations

+ +

+ Among the consistent functor combinations of the form p ∧ ¬q, the + following are not yet witnessed by a functor in the database or its dual functor. + If some of these combinations are + inconsistent, this indicates that some + implication is missing. +

+ +
+ + Show all {data.missing_functor_combinations.length} combinations + + +
    + {#each data.missing_functor_combinations as [p, q]} +
  • + {p} ∧ ¬{q} +
    • + {/each} +
+
+
+