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 b180a168..bc139eae 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,30 +72,74 @@ 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, ) - 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, - total_unknown_pairs, + structures_with_unknown_properties: { + category: categories_with_unknown_properties, + functor: functors_with_unknown_properties, + }, + unknown_totals: { + category: total_unknown_category_property_pairs, + functor: total_unknown_functor_property_pairs, + }, + undistinguishable_pairs: { + category: undistinguishable_category_pairs, + functor: undistinguishable_functor_pairs, + }, + missing_combinations: { + category: missing_category_combinations, + functor: missing_functor_combinations, + }, categories_with_missing_morphisms, - undistinguishable_category_pairs, - missing_combinations, } } diff --git a/src/routes/missing/+page.svelte b/src/routes/missing/+page.svelte index c4742601..117a5191 100644 --- a/src/routes/missing/+page.svelte +++ b/src/routes/missing/+page.svelte @@ -3,6 +3,8 @@ import MetaData from '$components/MetaData.svelte' import SuggestionForm from '$components/SuggestionForm.svelte' import { get_property_url } from '$lib/commons/property.url' + import { PLURALS, STRUCTURES } from '$lib/commons/structures' + import { capitalize } from '$lib/client/utils' const { data } = $props() @@ -19,17 +21,27 @@ contributing to this project.

-
-

Categories with unknown properties

+{#each STRUCTURES as type} + {@const structures = data.structures_with_unknown_properties[type]} + {@const total = data.unknown_totals[type]} +
+

{capitalize(PLURALS[type])} with unknown properties

-

- 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. -

+

+ There are {structures.length} + {PLURALS[type]} + where at least one property is unknown. + + {#if total > 0} + In total, there are {total} unknown ({type}, property)-pairs. + {:else} + 🎉 + {/if} +

- -
+ +
+{/each}

Categories with unknown special morphisms

@@ -42,58 +54,67 @@
-{#if data.undistinguishable_category_pairs.length > 0} +{#each STRUCTURES as type} + {@const pairs = data.undistinguishable_pairs[type]} + + {#if pairs.length > 0} +
+

Undistinguishable {type} pairs

+ +

+ There are {pairs.length} pairs of {PLURALS[type]} 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} +{/each} + +{#each STRUCTURES as type} + {@const combinations = data.missing_combinations[type]} +
-

Undistinguishable category pairs

+

Missing {type} combinations

- There are {data.undistinguishable_category_pairs.length} pairs of categories 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. + Among the consistent {type} combinations of the form p ∧ ¬q, the following + are not yet witnessed by a {type} in the database or its dual. If some of these + combinations are + inconsistent, this indicates that some + implication is missing.

- +
+ + Show all {combinations.length} combinations + + + +
-{/if} - -
-

Missing 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 - inconsistent, this indicates that some - implication is missing. -

- -
- Show all {data.missing_combinations.length} combinations - - -
-
+{/each}