diff --git a/databases/catdat/scripts/deduce-category-implications.ts b/databases/catdat/scripts/deduce-category-implications.ts index 5dcca040e..1d57f74df 100644 --- a/databases/catdat/scripts/deduce-category-implications.ts +++ b/databases/catdat/scripts/deduce-category-implications.ts @@ -1,104 +1,82 @@ -import { are_equal_sets, get_client } from './utils/helpers' +import { get_client } from './utils/helpers' +import { clear_deduced_implications, is_dualizable } from './utils/implications' const db = get_client() /** - * Deduces implications from given ones. + * Deduces category implications from given ones. */ export function deduce_category_implications() { console.info('\n--- Deduce category implications ---') - clear_deduced_category_implications() + clear_deduced_implications(db, 'category') create_dualized_category_implications() create_self_dual_category_implications() } /** - * Clears all deduced implications. This is done as a first step. - */ -function clear_deduced_category_implications() { - db.prepare(`DELETE FROM category_implications WHERE is_deduced = TRUE`).run() -} - -/** - * Dualizes all implications by dualizing the involved properties + * Dualizes all implications of categories by dualizing the involved properties * (in case they have a dual). For example, if P ===> Q holds, * then P^op ===> Q^op holds as well. */ function create_dualized_category_implications() { - type FullImplication = { + const implications_query = db.prepare( + `SELECT + v.id, + v.assumptions, + v.conclusions, + v.is_equivalence, + ( + SELECT json_group_array(p.dual_property_id) + FROM json_each(v.assumptions) a + JOIN category_properties p ON p.id = a.value + ) AS dual_assumptions, + ( + SELECT json_group_array(p.dual_property_id) + FROM json_each(v.conclusions) c + JOIN category_properties p ON p.id = c.value + ) AS dual_conclusions + FROM category_implications_view v + WHERE v.is_deduced = FALSE`, + ) + + const implications = implications_query.all() as { id: string assumptions: string conclusions: string dual_assumptions: string dual_conclusions: string - is_equivalence: number - reason: string - } + is_equivalence: 0 | 1 + }[] - const implications = db - .prepare( - `SELECT - v.id, - v.assumptions, - v.conclusions, - v.is_equivalence, - v.reason, - ( - SELECT json_group_array(p.dual_property_id) - FROM json_each(v.assumptions) a - JOIN category_properties p ON p.id = a.value - ) AS dual_assumptions, - ( - SELECT json_group_array(p.dual_property_id) - FROM json_each(v.conclusions) c - JOIN category_properties p ON p.id = c.value - ) AS dual_conclusions - FROM category_implications_view v - WHERE v.is_deduced = FALSE`, - ) - .all() as FullImplication[] - - const dualizable_implications = implications.filter((impl) => { - const has_null = - JSON.parse(impl.dual_assumptions).includes(null) || - JSON.parse(impl.dual_conclusions).includes(null) - if (has_null) return false + const dualizable_implications = implications.filter(is_dualizable) - const assumptions = new Set(JSON.parse(impl.assumptions)) - const conclusions = new Set(JSON.parse(impl.conclusions)) - const dual_assumptions = new Set(JSON.parse(impl.dual_assumptions)) - const dual_conclusions = new Set(JSON.parse(impl.dual_conclusions)) - - return ( - !are_equal_sets(assumptions, dual_assumptions) || - !are_equal_sets(conclusions, dual_conclusions) - ) - }) + const insert_query = db.prepare( + `INSERT INTO category_implications_view ( + id, + assumptions, + conclusions, + is_equivalence, + is_deduced, + dualized_from, + reason + ) VALUES (?, ?, ?, ?, TRUE, ?, ?)`, + ) const insert_duals = db.transaction(() => { for (const impl of dualizable_implications) { - db.prepare( - `INSERT INTO category_implications_view ( - id, - assumptions, - conclusions, - is_equivalence, - reason, - is_deduced, - dualized_from - ) VALUES (?, ?, ?, ?, ?, TRUE, ?)`, - ).run( + insert_query.run( `dual_${impl.id}`, impl.dual_assumptions, impl.dual_conclusions, impl.is_equivalence, - 'This follows from the dual implication.', impl.id, + 'This follows from the dual implication.', ) } }) insert_duals() + console.info(`Deduced ${dualizable_implications.length} implications by duality`) } diff --git a/databases/catdat/scripts/deduce-category-properties.ts b/databases/catdat/scripts/deduce-category-properties.ts deleted file mode 100644 index 40b7b3fe2..000000000 --- a/databases/catdat/scripts/deduce-category-properties.ts +++ /dev/null @@ -1,285 +0,0 @@ -import { SqliteError } from 'better-sqlite3' -import { - type CategoryMeta, - type CategoryPropertyMeta, - type NormalizedCategoryImplication, - get_property_assignments, - get_categories, - get_normalized_category_implications, - get_properties_dict, -} from './utils/categories' -import { - get_deduced_satisfied_properties, - get_deduced_unsatisfied_properties, -} from './utils/deduction' -import { get_client } from './utils/helpers' - -const db = get_client() - -/** - * Deduce properties of categories from given ones - * by using the list of implications. - */ -export function deduce_category_properties() { - console.info('\n--- Deduce category properties ---') - - const implications = get_normalized_category_implications(db) - const categories = get_categories(db) - const properties_dict = get_properties_dict(db) - - const deduction = db.transaction(() => { - delete_deduced_category_properties() - - const all_decided_properties = get_property_assignments(db, categories) - - for (const category of categories) { - const decided = all_decided_properties[category.id] - - deduce_satisfied_category_properties( - category.id, - implications, - decided.satisfied, - properties_dict, - ) - - deduce_unsatisfied_category_properties( - category.id, - implications, - decided.satisfied, - decided.unsatisfied, - properties_dict, - ) - } - - for (const category of categories) { - if (!is_dual_category(category)) continue - - const decided = all_decided_properties[category.id] - const dual_decided = all_decided_properties[category.dual_category_id] - - deduce_dual_category_properties( - category, - decided.satisfied, - decided.unsatisfied, - dual_decided.satisfied, - dual_decided.unsatisfied, - properties_dict, - ) - - deduce_satisfied_category_properties( - category.id, - implications, - decided.satisfied, - properties_dict, - ) - - deduce_unsatisfied_category_properties( - category.id, - implications, - decided.satisfied, - decided.unsatisfied, - properties_dict, - ) - } - }) - - deduction() -} - -/** - * Clears all the deduced properties. - * This runs before the deduction starts. - */ -function delete_deduced_category_properties() { - db.prepare(`DELETE FROM category_property_assignments WHERE is_deduced = TRUE`).run() -} - -/** - * Deduce satisfied properties for a given category from given ones - * by using the list of normalized implications. - * Warning: This function mutates the set of satisfied properties. - */ -function deduce_satisfied_category_properties( - category_id: string, - implications: NormalizedCategoryImplication[], - satisfied_properties: Set, - properties_dict: Record, -) { - const { found, reasons } = get_deduced_satisfied_properties( - satisfied_properties, - implications, - { properties_dict }, - ) - - for (const p of found) satisfied_properties.add(p) - - save_satisfied_properties(category_id, found, reasons) - - console.info(`Deduced ${found.size} satisfied properties for ${category_id}`) -} - -/** - * Saves the deduced satisfied properties to the database - */ -function save_satisfied_properties( - category_id: string, - found: Set, - reasons: Record, -) { - if (found.size === 0) return - - const err_msg = `❌ Failed to complete deduction of satisfied properties for ${category_id} because of a conflict. The likely cause is a contradiction between its assigned properties.` - - const property_insert = db.prepare(` - INSERT INTO category_property_assignments - (category_id, property_id, is_satisfied, reason, is_deduced) - VALUES (?, ?, TRUE, ?, TRUE) - `) - - try { - for (const p of found) { - property_insert.run(category_id, p, reasons[p]) - } - } catch (err) { - if (err instanceof SqliteError) { - if (err.code.startsWith('SQLITE_CONSTRAINT')) { - console.error(err_msg) - } - console.error(err.message) - } else { - console.error(err) - } - process.exit(1) - } -} - -/** - * Deduce unsatisfied properties for a given category from given ones - * by using the satisfied properties and the list of normalized implications. - * Warning: This function mutates the set of unsatisfied properties. - */ -function deduce_unsatisfied_category_properties( - category_id: string, - implications: NormalizedCategoryImplication[], - satisfied_properties: Set, - unsatisfied_properties: Set, - properties_dict: Record, -) { - const { found, reasons } = get_deduced_unsatisfied_properties( - satisfied_properties, - unsatisfied_properties, - implications, - { properties_dict }, - ) - - for (const p of found) unsatisfied_properties.add(p) - - save_unsatisfied_properties(category_id, found, reasons) - - console.info(`Deduced ${found.size} unsatisfied properties for ${category_id}`) -} - -/** - * Saves the deduced unsatisfied properties to the database - */ -function save_unsatisfied_properties( - category_id: string, - found: Set, - reasons: Record, -) { - if (found.size === 0) return - - const err_msg = `❌ Failed to complete deduction of unsatisfied properties for ${category_id} because of a conflict. The likely cause is a contradiction between its assigned properties.` - - const property_insert = db.prepare(` - INSERT INTO category_property_assignments - (category_id, property_id, is_satisfied, reason, is_deduced) - VALUES (?, ?, FALSE, ?, TRUE) - `) - - try { - for (const p of found) { - property_insert.run(category_id, p, reasons[p]) - } - } catch (err) { - if (err instanceof SqliteError) { - if (err.code.startsWith('SQLITE_CONSTRAINT')) { - console.error(err_msg) - } - console.error(err.message) - } else { - console.error(err) - } - process.exit(1) - } -} - -/** - * Checks if a category is a dual category, but not the - * original category to prevent circular reasoning. - */ -function is_dual_category( - category: CategoryMeta, -): category is CategoryMeta & { dual_category_id: string } { - return ( - category.dual_category_id !== null && - category.name.toLowerCase().startsWith('dual') - ) -} - -/** - * Assign dual properties to dual categories: - * If C has property P, then C^op has property P^op (if defined). - * Warning: This mutates the sets of satisfied and unsatisfied properties. - */ -function deduce_dual_category_properties( - category: CategoryMeta, - satisfied: Set, - unsatisfied: Set, - dual_satisfied: Set, - dual_unsatisfied: Set, - properties_dict: Record, -) { - const new_satisfied = new Set() - - for (const p of dual_satisfied) { - const p_dual = properties_dict[p].dual_property_id - if (!p_dual || satisfied.has(p_dual)) continue - new_satisfied.add(p_dual) - satisfied.add(p_dual) - } - - const new_unsatisfied = new Set() - - for (const p of dual_unsatisfied) { - const p_dual = properties_dict[p].dual_property_id - if (!p_dual || unsatisfied.has(p_dual)) continue - new_unsatisfied.add(p_dual) - unsatisfied.add(p_dual) - } - - const property_insert = db.prepare(` - INSERT INTO category_property_assignments - (category_id, property_id, is_satisfied, reason, is_deduced) - VALUES (?, ?, ?, ?, TRUE) - `) - - const reason_satisfied = 'Its dual category satisfies the dual property.' - const reason_unsatisfied = 'Its dual category does not satisfy the dual property.' - - for (const p of new_satisfied) { - property_insert.run(category.id, p, 1, reason_satisfied) - } - - console.info( - `Deduced ${new_satisfied.size} satisfied properties by duality for ${category.id}`, - ) - - for (const q of new_unsatisfied) { - property_insert.run(category.id, q, 0, reason_unsatisfied) - } - - console.info( - `Deduced ${new_unsatisfied.size} unsatisfied properties by duality for ${category.id}`, - ) -} diff --git a/databases/catdat/scripts/deduce-entity-properties.ts b/databases/catdat/scripts/deduce-entity-properties.ts new file mode 100644 index 000000000..9e8d6c074 --- /dev/null +++ b/databases/catdat/scripts/deduce-entity-properties.ts @@ -0,0 +1,452 @@ +/** + * This file contains all functions that are used to deduce properties + * for categories and functors. + */ + +import { type Database, SqliteError } from 'better-sqlite3' +import { get_client, is_subset } from './utils/helpers' +import { + get_entities, + get_normalized_implications, + get_properties_dict, + get_property_assignments, + is_dual_entity, + type EntityMeta, + type NormalizedImplication, + type PropertyMeta, +} from './utils/deduction' +import { get_contradiction_string, get_reason_string } from './utils/implications' + +/** + * Returns the set of satisfied properties that can be deduced from a set + * of satisfied properties, based on a list of normalized implications. If a + * property dictionary is provided, human-readable reasons are generated as well. + */ +export function get_deduced_satisfied_properties( + satisfied_properties: Set, + implications: NormalizedImplication[], + options: { + properties_dict?: Record + stop_when_found?: string + }, + type: 'category' | 'functor', + // used for source and target properties of a functor + associated_satisfied_properties?: Record>, +) { + const found = new Set() + const reasons: Record = {} + const deduced_satisfied_properties = new Set(satisfied_properties) + + while (true) { + const newly_found = new Set() + + for (const implication of implications) { + const is_valid = + is_subset(implication.assumptions, deduced_satisfied_properties) && + !deduced_satisfied_properties.has(implication.conclusion) && + !newly_found.has(implication.conclusion) + + if (!is_valid) continue + + if (implication.associated_assumptions) { + const is_applicable = Object.keys( + implication.associated_assumptions, + ).every((key) => { + return is_subset( + implication.associated_assumptions?.[key] ?? new Set(), + associated_satisfied_properties?.[key] ?? new Set(), + ) + }) + if (!is_applicable) continue + } + + newly_found.add(implication.conclusion) + found.add(implication.conclusion) + + if (options?.stop_when_found === implication.conclusion) { + deduced_satisfied_properties.add(implication.conclusion) + return { deduced_satisfied_properties, found, reasons } + } + + if (options.properties_dict) { + reasons[implication.conclusion] = get_reason_string( + implication, + options.properties_dict, + type, + ) + } + } + + for (const p of newly_found) deduced_satisfied_properties.add(p) + + if (!newly_found.size) break + } + + return { deduced_satisfied_properties, found, reasons } +} + +/** + * Returns the set of unsatisfied properties that can be deduced from + * a set of satisfied properties and a set of unsatisfied properties, + * based on a list of normalized implications. If a property dictionary + * is provided, human-readable reasons are generated as well. + */ +export function get_deduced_unsatisfied_properties( + satisfied_properties: Set, + unsatisfied_properties: Set, + implications: NormalizedImplication[], + options: { + properties_dict?: Record + stop_when_found?: string + }, + type: 'category' | 'functor', + // used for source and target properties of a functor + associated_satisfied_properties?: Record>, +) { + const found = new Set() + const reasons: Record = {} + const deduced_unsatisfied_properties = new Set(unsatisfied_properties) + + while (true) { + const newly_found = new Set() + + for (const implication of implications) { + if (!deduced_unsatisfied_properties.has(implication.conclusion)) continue + for (const p of implication.assumptions) { + const is_valid = + !deduced_unsatisfied_properties.has(p) && + !newly_found.has(p) && + is_subset(implication.assumptions, satisfied_properties, { + exception: p, + }) + if (!is_valid) continue + + if (implication.associated_assumptions) { + const is_applicable = Object.keys( + implication.associated_assumptions, + ).every((key) => { + return is_subset( + implication.associated_assumptions?.[key] ?? new Set(), + associated_satisfied_properties?.[key] ?? new Set(), + ) + }) + if (!is_applicable) continue + } + + if (satisfied_properties.has(p)) { + throw new Error(`Contradiction has been found for: ${p}`) + } + + if (options?.stop_when_found === p) { + deduced_unsatisfied_properties.add(p) + return { deduced_unsatisfied_properties, found, reasons } + } + + newly_found.add(p) + found.add(p) + + if (options.properties_dict) { + reasons[p] = get_contradiction_string( + implication, + options.properties_dict, + p, + type, + ) + } + } + } + + for (const p of newly_found) deduced_unsatisfied_properties.add(p) + + if (!newly_found.size) break + } + + return { deduced_unsatisfied_properties, found, reasons } +} + +/** + * Saves the deduced satisfied properties to the database + */ +function save_satisfied_properties( + db: Database, + entity_id: string, + found: Set, + reasons: Record, + type: 'category' | 'functor', +) { + if (found.size === 0) return + + const err_msg = `❌ Failed to complete deduction of satisfied properties for ${entity_id} because of a conflict. The likely cause is a contradiction between its assigned properties.` + + const property_insert = db.prepare(` + INSERT INTO ${type}_property_assignments + (${type}_id, property_id, is_satisfied, reason, is_deduced) + VALUES (?, ?, TRUE, ?, TRUE) + `) + + try { + for (const p of found) { + property_insert.run(entity_id, p, reasons[p]) + } + } catch (err) { + if (err instanceof SqliteError) { + if (err.code.startsWith('SQLITE_CONSTRAINT')) { + console.error(err_msg) + } + console.error(err.message) + } else { + console.error(err) + } + process.exit(1) + } +} + +/** + * Saves the deduced unsatisfied properties to the database + */ +function save_unsatisfied_properties( + db: Database, + entity_id: string, + found: Set, + reasons: Record, + type: 'category' | 'functor', +) { + if (found.size === 0) return + + const err_msg = `❌ Failed to complete deduction of unsatisfied properties for ${entity_id} because of a conflict. The likely cause is a contradiction between its assigned properties.` + + const property_insert = db.prepare(` + INSERT INTO ${type}_property_assignments + (${type}_id, property_id, is_satisfied, reason, is_deduced) + VALUES (?, ?, FALSE, ?, TRUE) + `) + + try { + for (const p of found) { + property_insert.run(entity_id, p, reasons[p]) + } + } catch (err) { + if (err instanceof SqliteError) { + if (err.code.startsWith('SQLITE_CONSTRAINT')) { + console.error(err_msg) + } + console.error(err.message) + } else { + console.error(err) + } + process.exit(1) + } +} + +/** + * Deduce satisfied properties for a given entity from given ones + * by using the list of normalized implications. + * Warning: This mutates the set of satisfied properties. + */ +function deduce_satisfied_properties( + db: Database, + entity: EntityMeta, + implications: NormalizedImplication[], + satisfied_properties: Set, + properties_dict: Record, + type: 'category' | 'functor', +) { + const { found, reasons } = get_deduced_satisfied_properties( + satisfied_properties, + implications, + { properties_dict }, + type, + entity.associated_satisfied_properties, + ) + + for (const p of found) satisfied_properties.add(p) + + save_satisfied_properties(db, entity.id, found, reasons, type) + + console.info(`Deduced ${found.size} satisfied properties for ${entity.id}`) +} + +/** + * Deduce unsatisfied properties for a given entity from given ones + * by using the satisfied properties and the list of normalized implications. + * Warning: This mutates the set of unsatisfied properties. + */ +function deduce_unsatisfied_properties( + db: Database, + entity: EntityMeta, + implications: NormalizedImplication[], + satisfied_properties: Set, + unsatisfied_properties: Set, + properties_dict: Record, + type: 'category' | 'functor', +) { + const { found, reasons } = get_deduced_unsatisfied_properties( + satisfied_properties, + unsatisfied_properties, + implications, + { properties_dict }, + type, + entity.associated_satisfied_properties, + ) + + for (const p of found) unsatisfied_properties.add(p) + + save_unsatisfied_properties(db, entity.id, found, reasons, type) + + console.info(`Deduced ${found.size} unsatisfied properties for ${entity.id}`) +} + +/** + * Assign dual properties to dual entities: + * If C has property P, then C^op has property P^op (if defined). + * Warning: This mutates the sets of satisfied and unsatisfied properties. + */ +function deduce_dual_properties( + db: Database, + entity: EntityMeta & { dual: string }, + satisfied: Set, + unsatisfied: Set, + dual_satisfied: Set, + dual_unsatisfied: Set, + properties_dict: Record, + type: 'category', +) { + const new_satisfied = new Set() + + for (const p of dual_satisfied) { + const p_dual = properties_dict[p].dual + if (!p_dual || satisfied.has(p_dual)) continue + new_satisfied.add(p_dual) + satisfied.add(p_dual) + } + + const new_unsatisfied = new Set() + + for (const p of dual_unsatisfied) { + const p_dual = properties_dict[p].dual + if (!p_dual || unsatisfied.has(p_dual)) continue + new_unsatisfied.add(p_dual) + unsatisfied.add(p_dual) + } + + const property_insert = db.prepare(` + INSERT INTO ${type}_property_assignments + (${type}_id, property_id, is_satisfied, reason, is_deduced) + VALUES (?, ?, ?, ?, TRUE) + `) + + const reason_satisfied = 'Its dual ${type} satisfies the dual property.' + const reason_unsatisfied = 'Its dual ${type} does not satisfy the dual property.' + + for (const p of new_satisfied) { + property_insert.run(entity.id, p, 1, reason_satisfied) + } + + console.info( + `Deduced ${new_satisfied.size} satisfied properties by duality for ${entity.id}`, + ) + + for (const q of new_unsatisfied) { + property_insert.run(entity.id, q, 0, reason_unsatisfied) + } + + console.info( + `Deduced ${new_unsatisfied.size} unsatisfied properties by duality for ${entity.id}`, + ) +} + +/** + * Clears all the deduced properties. This runs before the deduction starts. + */ +function delete_deduced_properties(db: Database, type: 'category' | 'functor') { + db.prepare(`DELETE FROM ${type}_property_assignments WHERE is_deduced = TRUE`).run() +} + +/** + * --- MAIN FUNCTION --- + * Deduce properties of entities from given ones + * by using the list of implications. + */ +export function deduce_properties_for_entities(type: 'category' | 'functor') { + console.info(`\n--- Deduce ${type} properties ---`) + + const db = get_client() + + const implications = get_normalized_implications(db, type) + const entities = get_entities(db, type) + const properties_dict = get_properties_dict(db, type) + const all_decided_properties = get_property_assignments(db, entities, type) + + const deduction = db.transaction(() => { + delete_deduced_properties(db, type) + + for (const entity of entities) { + const decided = all_decided_properties[entity.id] + + deduce_satisfied_properties( + db, + entity, + implications, + decided.satisfied, + properties_dict, + type, + ) + + deduce_unsatisfied_properties( + db, + entity, + implications, + decided.satisfied, + decided.unsatisfied, + properties_dict, + type, + ) + } + }) + + deduction() + + // currently, only categories have duals + if (type !== 'category') return + + const dual_deduction = db.transaction(() => { + for (const entity of entities) { + if (!is_dual_entity(entity)) continue + + const decided = all_decided_properties[entity.id] + const dual_decided = all_decided_properties[entity.dual] + + deduce_dual_properties( + db, + entity, + decided.satisfied, + decided.unsatisfied, + dual_decided.satisfied, + dual_decided.unsatisfied, + properties_dict, + type, + ) + + deduce_satisfied_properties( + db, + entity, + implications, + decided.satisfied, + properties_dict, + type, + ) + + deduce_unsatisfied_properties( + db, + entity, + implications, + decided.satisfied, + decided.unsatisfied, + properties_dict, + type, + ) + } + }) + + dual_deduction() +} diff --git a/databases/catdat/scripts/deduce-functor-implications.ts b/databases/catdat/scripts/deduce-functor-implications.ts index f231a759d..1e551854d 100644 --- a/databases/catdat/scripts/deduce-functor-implications.ts +++ b/databases/catdat/scripts/deduce-functor-implications.ts @@ -1,6 +1,5 @@ -import { are_equal_sets, get_client } from './utils/helpers' - -// TODO: remove code duplication with category implication deduction script +import { get_client } from './utils/helpers' +import { clear_deduced_implications, is_dualizable } from './utils/implications' const db = get_client() @@ -9,25 +8,48 @@ const db = get_client() */ export function deduce_functor_implications() { console.info('\n--- Deduce functor implications ---') - clear_deduced_functor_implications() + clear_deduced_implications(db, 'functor') create_dualized_functor_implications() } /** - * Clears all deduced functor implications. This is done as a first step. - */ -function clear_deduced_functor_implications() { - db.prepare(`DELETE FROM functor_implications WHERE is_deduced = TRUE`).run() -} - -/** - * Dualizes all functor implications by dualizing the involved properties + * Dualizes all implications of functors by dualizing the involved properties * (in case they have a dual). For example, if P ===> Q holds, * then P^op ===> Q^op holds as well. The assumptions of source and target * categories (if any) need to be dualized as well. */ function create_dualized_functor_implications() { - type FullImplication = { + const implications_query = db.prepare( + `SELECT + v.id, + v.assumptions, + v.conclusions, + v.is_equivalence, + ( + SELECT json_group_array(p.dual_property_id) + FROM json_each(v.assumptions) a + JOIN functor_properties p ON p.id = a.value + ) AS dual_assumptions, + ( + SELECT json_group_array(p.dual_property_id) + FROM json_each(v.source_assumptions) sa + JOIN category_properties p ON p.id = sa.value + ) AS dual_source_assumptions, + ( + SELECT json_group_array(p.dual_property_id) + FROM json_each(v.target_assumptions) ta + JOIN category_properties p ON p.id = ta.value + ) AS dual_target_assumptions, + ( + SELECT json_group_array(p.dual_property_id) + FROM json_each(v.conclusions) c + JOIN functor_properties p ON p.id = c.value + ) AS dual_conclusions + FROM functor_implications_view v + WHERE v.is_deduced = FALSE`, + ) + + const implications = implications_query.all() as { id: string assumptions: string conclusions: string @@ -35,90 +57,41 @@ function create_dualized_functor_implications() { dual_source_assumptions: string dual_target_assumptions: string dual_conclusions: string - is_equivalence: number - reason: string - } - - const implications = db - .prepare( - `SELECT - v.id, - v.assumptions, - v.conclusions, - v.is_equivalence, - v.reason, - ( - SELECT json_group_array(p.dual_property_id) - FROM json_each(v.assumptions) a - JOIN functor_properties p ON p.id = a.value - ) AS dual_assumptions, - ( - SELECT json_group_array(p.dual_property_id) - FROM json_each(v.source_assumptions) sa - JOIN category_properties p ON p.id = sa.value - ) AS dual_source_assumptions, - ( - SELECT json_group_array(p.dual_property_id) - FROM json_each(v.target_assumptions) ta - JOIN category_properties p ON p.id = ta.value - ) AS dual_target_assumptions, - ( - SELECT json_group_array(p.dual_property_id) - FROM json_each(v.conclusions) c - JOIN functor_properties p ON p.id = c.value - ) AS dual_conclusions - FROM functor_implications_view v - WHERE v.is_deduced = FALSE`, - ) - .all() as FullImplication[] + is_equivalence: 0 | 1 + }[] - const dualizable_implications = implications.filter((impl) => { - const has_null = - JSON.parse(impl.dual_assumptions).includes(null) || - JSON.parse(impl.dual_conclusions).includes(null) || - JSON.parse(impl.dual_source_assumptions).includes(null) || - JSON.parse(impl.dual_target_assumptions).includes(null) + const dualizable_implications = implications.filter(is_dualizable) - if (has_null) return false - - const assumptions = new Set(JSON.parse(impl.assumptions)) - const conclusions = new Set(JSON.parse(impl.conclusions)) - const dual_assumptions = new Set(JSON.parse(impl.dual_assumptions)) - const dual_conclusions = new Set(JSON.parse(impl.dual_conclusions)) - - return ( - !are_equal_sets(assumptions, dual_assumptions) || - !are_equal_sets(conclusions, dual_conclusions) - ) - }) + const insert_query = db.prepare( + `INSERT INTO functor_implications_view ( + id, + assumptions, + source_assumptions, + target_assumptions, + conclusions, + is_equivalence, + is_deduced, + dualized_from, + reason + ) VALUES (?, ?, ?, ?, ?, ?, TRUE, ?, ?)`, + ) const insert_duals = db.transaction(() => { for (const impl of dualizable_implications) { - db.prepare( - `INSERT INTO functor_implications_view ( - id, - assumptions, - source_assumptions, - target_assumptions, - conclusions, - is_equivalence, - reason, - dualized_from, - is_deduced - ) VALUES (?, ?, ?, ?, ?, ?, ?, ?, TRUE)`, - ).run( + insert_query.run( `dual_${impl.id}`, impl.dual_assumptions, impl.dual_source_assumptions, impl.dual_target_assumptions, impl.dual_conclusions, impl.is_equivalence, - 'This follows from the dual implication.', impl.id, + 'This follows from the dual implication.', ) } }) insert_duals() + console.info(`Deduced ${dualizable_implications.length} implications by duality`) } diff --git a/databases/catdat/scripts/deduce-functor-properties.ts b/databases/catdat/scripts/deduce-functor-properties.ts deleted file mode 100644 index 954b28505..000000000 --- a/databases/catdat/scripts/deduce-functor-properties.ts +++ /dev/null @@ -1,369 +0,0 @@ -import { get_client, is_subset } from './utils/helpers' -import { get_assumption_string, get_conclusion_string } from './utils/deduction' - -const db = get_client() - -type FunctorMeta = { - id: string - name: string - source: string - source_props: Set - target: string - target_props: Set -} - -type NormalizedFunctorImplication = { - id: string - assumptions: Set - conclusion: string - source_assumptions: Set - target_assumptions: Set -} - -type FunctorPropertyMeta = { - id: string - dual_property_id: string | null - relation: string - negation: string - conditional: string -} - -// TODO: remove code duplication with category deduction script -// (not quite the same because we need source and target assumptions) - -// TODO: apply the same refactoring here that has been done for categories - -/** - * Deduce properties of functors from given ones - * by using the list of functor implications. - */ -export function deduce_functor_properties() { - console.info('\n--- Deduce functor properties ---') - - const implications = get_normalized_functor_implications() - const functors = get_functors() - const properties_dict = get_functor_properties_dict() - - const deduction = db.transaction(() => { - delete_deduced_functor_properties() - - for (const functor of functors) { - deduce_satisfied_functor_properties(functor, implications, properties_dict) - deduce_unsatisfied_functor_properties(functor, implications, properties_dict) - } - }) - - deduction() -} - -/** - * Implications have the form: - * - * P_1 + ... + P_n ----> Q_1 + ... + Q_m - * - * or - * - * P_1 + ... + P_n <---> Q_1 + ... + Q_m - * - * This function decomposes them into normalized implications, - * which have the form: - * - * P_1 + ... + P_n ----> Q - */ -function get_normalized_functor_implications(): NormalizedFunctorImplication[] { - const all_implications_db = db - .prepare( - `SELECT - v.id, - v.assumptions, - v.source_assumptions, - v.target_assumptions, - v.conclusions, - v.is_equivalence - FROM functor_implications_view v`, - ) - .all() as { - id: string - assumptions: string - source_assumptions: string - target_assumptions: string - conclusions: string - is_equivalence: number - }[] - - const implications: NormalizedFunctorImplication[] = [] - - for (const impl of all_implications_db) { - const assumptions: string[] = JSON.parse(impl.assumptions) - const conclusions: string[] = JSON.parse(impl.conclusions) - const source_assumptions: string[] = JSON.parse(impl.source_assumptions) - const target_assumptions: string[] = JSON.parse(impl.target_assumptions) - - for (const conclusion of conclusions) { - implications.push({ - id: impl.id, - assumptions: new Set(assumptions), - source_assumptions: new Set(source_assumptions), - target_assumptions: new Set(target_assumptions), - conclusion, - }) - } - - if (impl.is_equivalence) { - for (const assumption of assumptions) { - implications.push({ - id: impl.id, - assumptions: new Set(conclusions), - source_assumptions: new Set(source_assumptions), - target_assumptions: new Set(target_assumptions), - conclusion: assumption, - }) - } - } - } - - return implications -} - -/** - * Returns the list of functors saved in the database along with - * the satisfied properties of their source and target category. - */ -function get_functors() { - const rows = db - .prepare( - `SELECT - id, name, source, target, - ( - SELECT json_group_array(property_id) FROM ( - SELECT property_id - FROM category_property_assignments - WHERE category_id = source AND is_satisfied = TRUE - ) - ) as source_props, - ( - SELECT json_group_array(property_id) FROM ( - SELECT property_id - FROM category_property_assignments - WHERE category_id = target AND is_satisfied = TRUE - ) - ) as target_props - FROM functors - ORDER BY lower(name)`, - ) - .all() as { - id: string - name: string - source: string - target: string - source_props: string - target_props: string - }[] - - return rows.map((row) => ({ - id: row.id, - name: row.name, - source: row.source, - target: row.target, - source_props: new Set(JSON.parse(row.source_props as string)), - target_props: new Set(JSON.parse(row.target_props as string)), - })) as FunctorMeta[] -} - -/** - * Returns a dictionary of functor properties saved in the database. - */ -function get_functor_properties_dict() { - const properties = db - .prepare( - `SELECT - p.id, p.dual_property_id, p.relation, - r.negation, r.conditional - FROM functor_properties p - INNER JOIN relations r ON r.relation = p.relation - ORDER BY lower(p.id)`, - ) - .all() as FunctorPropertyMeta[] - - const dict: Record = {} - - for (const p of properties) dict[p.id] = p - - return dict -} - -/** - * Clears all the deduced functor properties. - * This runs before the deduction starts. - */ -function delete_deduced_functor_properties() { - db.prepare('DELETE FROM functor_property_assignments WHERE is_deduced = TRUE').run() -} - -/** - * Returns the list of properties that are satisfied or unsatisfied - * for a given functor. - */ -function get_decided_functor_properties(functor_id: string, value: boolean) { - const rows = db - .prepare( - `SELECT property_id - FROM functor_property_assignments - WHERE functor_id = ? AND is_satisfied = ?`, - ) - .all(functor_id, value ? 1 : 0) as { property_id: string }[] - - return new Set(rows.map((row) => row.property_id) as string[]) -} - -/** - * Deduce satisfied properties for a given functor from given ones - * by using the list of normalized implications. - */ -function deduce_satisfied_functor_properties( - functor: FunctorMeta, - implications: NormalizedFunctorImplication[], - properties_dict: Record, -) { - const satisfied_props = get_decided_functor_properties(functor.id, true) - - const deduced_satisfied_props: string[] = [] - const reasons: Record = {} - - while (true) { - const implication = implications.find( - ({ assumptions, conclusion, source_assumptions, target_assumptions }) => - is_subset(assumptions, satisfied_props) && - !satisfied_props.has(conclusion) && - is_subset(source_assumptions, functor.source_props) && - is_subset(target_assumptions, functor.target_props), - ) - if (!implication) break - - const { id: implication_id, conclusion } = implication - - satisfied_props.add(conclusion) - deduced_satisfied_props.push(conclusion) - - const assumption_string = get_assumption_string(implication, properties_dict) - const conclusion_string = get_conclusion_string(implication, properties_dict) - - const ref = `by this result` - const reason = `Since it ${assumption_string}, it ${conclusion_string} (${ref}).` - - reasons[conclusion] = reason - } - - if (deduced_satisfied_props.length > 0) { - const value_fragments: string[] = [] - const values: (string | number)[] = [] - - for (const id of deduced_satisfied_props) { - value_fragments.push(`(?, ?, TRUE, ?, TRUE)`) - values.push(functor.id, id, reasons[id]) - } - - const insert_sql = ` - INSERT INTO functor_property_assignments ( - functor_id, property_id, is_satisfied, reason, is_deduced - ) - VALUES - ${value_fragments.join(',\n')} - ` - - db.prepare(insert_sql).run(values) - } - - console.info( - `Deduced ${deduced_satisfied_props.length} satisfied properties for ${functor.id}`, - ) -} - -/** - * Deduce unsatisfied properties for a given functor from given ones - * by using the satisfied properties and the list of normalized implications. - */ -function deduce_unsatisfied_functor_properties( - functor: FunctorMeta, - implications: NormalizedFunctorImplication[], - properties_dict: Record, -) { - const satisfied_props = get_decided_functor_properties(functor.id, true) - const unsatisfied_props = get_decided_functor_properties(functor.id, false) - - const deduced_unsatisfied_props: string[] = [] - const reasons: Record = {} - - function get_next_implication() { - for (const implication of implications) { - if (!unsatisfied_props.has(implication.conclusion)) continue - for (const p of implication.assumptions) { - const is_valid = - !unsatisfied_props.has(p) && - is_subset(implication.assumptions, satisfied_props, { - exception: p, - }) && - is_subset(implication.source_assumptions, functor.source_props) && - is_subset(implication.target_assumptions, functor.target_props) - - if (is_valid) return { implication, property: p } - } - } - - return null - } - - while (true) { - const next = get_next_implication() - if (!next) break - - const { implication, property } = next - const { id: implication_id } = implication - - if (satisfied_props.has(property)) { - throw new Error(`Contradiction has been found for: ${property}`) - } - - unsatisfied_props.add(property) - deduced_unsatisfied_props.push(property) - - const assumption_string = get_assumption_string(implication, properties_dict) - const conclusion_string = get_conclusion_string(implication, properties_dict) - - const has_multiple_assumptions = implication.assumptions.size > 1 - - const ref = `by this result` - - const contra = `Assume for contradiction that it ${properties_dict[property].relation} ${property}` - - const reason = has_multiple_assumptions - ? `${contra}. Then it ${assumption_string}, so it ${conclusion_string} (${ref}) – contradiction.` - : `${contra}. Then it ${conclusion_string} (${ref}) – contradiction.` - - reasons[property] = reason - } - - if (deduced_unsatisfied_props.length > 0) { - const value_fragments: string[] = [] - const values: (string | number)[] = [] - - for (let i = 0; i < deduced_unsatisfied_props.length; i++) { - const id = deduced_unsatisfied_props[i] - value_fragments.push('(?, ?, FALSE, ?, TRUE)') - values.push(functor.id, id, reasons[id]) - } - - const insert_query = ` - INSERT INTO functor_property_assignments ( - functor_id, property_id, is_satisfied, reason, is_deduced - ) - VALUES - ${value_fragments.join(',\n')}` - - db.prepare(insert_query).run(values) - } - - console.info( - `Deduced ${deduced_unsatisfied_props.length} unsatisfied properties for ${functor.id}`, - ) -} diff --git a/databases/catdat/scripts/deduce.ts b/databases/catdat/scripts/deduce.ts index 91163ca15..e35562298 100644 --- a/databases/catdat/scripts/deduce.ts +++ b/databases/catdat/scripts/deduce.ts @@ -1,9 +1,8 @@ import { deduce_category_implications } from './deduce-category-implications' -import { deduce_category_properties } from './deduce-category-properties' import { deduce_functor_implications } from './deduce-functor-implications' -import { deduce_functor_properties } from './deduce-functor-properties' import { deduce_special_objects } from './deduce-special-objects' import { deduce_special_morphisms } from './deduce-special-morphisms' +import { deduce_properties_for_entities } from './deduce-entity-properties' deduce() @@ -12,11 +11,11 @@ deduce() */ function deduce() { deduce_category_implications() - deduce_category_properties() + deduce_properties_for_entities('category') deduce_special_objects() deduce_special_morphisms() deduce_functor_implications() - deduce_functor_properties() + deduce_properties_for_entities('functor') } diff --git a/databases/catdat/scripts/expected-data/_INFO.md b/databases/catdat/scripts/expected-data/_INFO.md index 58b0b8178..0cd8f038b 100644 --- a/databases/catdat/scripts/expected-data/_INFO.md +++ b/databases/catdat/scripts/expected-data/_INFO.md @@ -1,2 +1,3 @@ - The JSON file `decided-categories.json` lists various categories whose properties need to be decided. If a new property is added to the database, make sure to decide it _at least_ for these categories. -- The other JSON files specify precisely which properties are satisfied by a small selection of categories. If a new property is added to the database, make sure to add the value here. +- Similar remarks apply to `decided-functors.json`. +- The other JSON files specify precisely which properties are satisfied by a small selection of categories or functors. If a new property is added to the database, make sure to add the value here. diff --git a/databases/catdat/scripts/expected-data/decided-categories.json b/databases/catdat/scripts/expected-data/decided-categories.json index 78b56b49c..cad3c44e8 100644 --- a/databases/catdat/scripts/expected-data/decided-categories.json +++ b/databases/catdat/scripts/expected-data/decided-categories.json @@ -9,6 +9,7 @@ "CRing", "Ring", "Set", + "Set_op", "Set*", "Top", "Top*", diff --git a/databases/catdat/scripts/expected-data/decided-functors.json b/databases/catdat/scripts/expected-data/decided-functors.json new file mode 100644 index 000000000..4c5bfed96 --- /dev/null +++ b/databases/catdat/scripts/expected-data/decided-functors.json @@ -0,0 +1 @@ +["id_Set", "forget_vector"] diff --git a/databases/catdat/scripts/expected-data/forget_vector.json b/databases/catdat/scripts/expected-data/forget_vector.json new file mode 100644 index 000000000..f469d9783 --- /dev/null +++ b/databases/catdat/scripts/expected-data/forget_vector.json @@ -0,0 +1,29 @@ +{ + "cocontinuous": false, + "coequalizer-preserving": false, + "comonadic": false, + "coproduct-preserving": false, + "equivalence": false, + "essentially surjective": false, + "exact": false, + "finite-coproduct-preserving": false, + "full": false, + "initial-object-preserving": false, + "left adjoint": false, + "right exact": false, + "cofinitary": true, + "conservative": true, + "continuous": true, + "epimorphism-preserving": true, + "equalizer-preserving": true, + "faithful": true, + "finitary": true, + "finite-product-preserving": true, + "left exact": true, + "monadic": true, + "monomorphism-preserving": true, + "product-preserving": true, + "representable": true, + "right adjoint": true, + "terminal-object-preserving": true +} diff --git a/databases/catdat/scripts/expected-data/id_Set.json b/databases/catdat/scripts/expected-data/id_Set.json new file mode 100644 index 000000000..ac2a0a693 --- /dev/null +++ b/databases/catdat/scripts/expected-data/id_Set.json @@ -0,0 +1,29 @@ +{ + "cocontinuous": true, + "coequalizer-preserving": true, + "cofinitary": true, + "comonadic": true, + "conservative": true, + "continuous": true, + "coproduct-preserving": true, + "epimorphism-preserving": true, + "equalizer-preserving": true, + "equivalence": true, + "essentially surjective": true, + "exact": true, + "faithful": true, + "finitary": true, + "finite-coproduct-preserving": true, + "finite-product-preserving": true, + "full": true, + "initial-object-preserving": true, + "left adjoint": true, + "left exact": true, + "monadic": true, + "monomorphism-preserving": true, + "product-preserving": true, + "representable": true, + "right adjoint": true, + "right exact": true, + "terminal-object-preserving": true +} diff --git a/databases/catdat/scripts/redundancies.ts b/databases/catdat/scripts/redundancies.ts index 17fedf682..fc3cd3d4a 100644 --- a/databases/catdat/scripts/redundancies.ts +++ b/databases/catdat/scripts/redundancies.ts @@ -3,13 +3,13 @@ import { get_categories, get_ignored_redundant_properties, get_normalized_category_implications, - get_property_assignments_by_deduction, type NormalizedCategoryImplication, } from './utils/categories' import { get_deduced_satisfied_properties, get_deduced_unsatisfied_properties, -} from './utils/deduction' +} from './deduce-entity-properties' +import { get_property_assignments_by_deduction } from './utils/deduction' const db = get_client() @@ -32,7 +32,7 @@ function check_redundant_category_property_assignments() { const implications = get_normalized_category_implications(db) const categories = get_categories(db) - const assignments = get_property_assignments_by_deduction(db, categories) + const assignments = get_property_assignments_by_deduction(db, categories, 'category') const ignore_dict = get_ignored_redundant_properties(db) const ignore_count = Object.keys(ignore_dict).reduce( @@ -107,6 +107,7 @@ function get_redundant_satisfied_property( satisfied_properties, implications, { stop_when_found: p }, + 'category', ) if (deduced_satisfied_properties.has(p)) return p satisfied_properties.add(p) @@ -134,6 +135,7 @@ function get_redundant_unsatisfied_property( unsatisfied_properties, implications, { stop_when_found: p }, + 'category', ) if (deduced_unsatisfied_properties.has(p)) return p unsatisfied_properties.add(p) diff --git a/databases/catdat/scripts/test.ts b/databases/catdat/scripts/test.ts index ecf2a7c15..8e8434794 100644 --- a/databases/catdat/scripts/test.ts +++ b/databases/catdat/scripts/test.ts @@ -7,8 +7,11 @@ import Set_expected from './expected-data/Set.json' import Ab_expected from './expected-data/Ab.json' import Top_expected from './expected-data/Top.json' +import forget_vector_expected from './expected-data/forget_vector.json' +import id_Set_expected from './expected-data/id_Set.json' import decided_categories from './expected-data/decided-categories.json' -import { get_client } from './utils/helpers' +import decided_functors from './expected-data/decided-functors.json' +import { capitalize, get_client } from './utils/helpers' const db = get_client() @@ -18,13 +21,24 @@ execute_tests() * The main test function verifying that the data behaves as expected. */ function execute_tests() { - console.info('\n--- Test database ---') try { + console.info('\n--- Test categories ---') test_mutual_category_duals() - test_mutual_property_duals() - test_decided_categories() test_properties_of_trivial_category() - test_properties_of_selected_categories() + test_mutual_property_duals('category') + test_decided_entities(decided_categories, 'category') + test_properties_of_selected_entities( + { Set: Set_expected, Ab: Ab_expected, Top: Top_expected }, + 'category', + ) + + console.info('\n--- Test functors ---') + test_mutual_property_duals('functor') + test_decided_entities(decided_functors, 'functor') + test_properties_of_selected_entities( + { forget_vector: forget_vector_expected, id_Set: id_Set_expected }, + 'functor', + ) } catch (err) { if (err instanceof Error) { console.error(err.message) @@ -35,30 +49,6 @@ function execute_tests() { } } -/** - * Tests for all category properties p,q that if p is dual to q, then q is dual to p. - */ -function test_mutual_property_duals() { - const dict: Record = {} - - const properties = db - .prepare('SELECT id, dual_property_id FROM category_properties') - .all() as { id: string; dual_property_id: string | null }[] - - for (const { id, dual_property_id } of properties) { - dict[id] = dual_property_id - } - - for (const id in dict) { - const dual = dict[id] - if (dual && dict[dual] !== id) { - throw new Error(`❌ Found non-mutual property duality: ${id}, ${dual}`) - } - } - - console.info(`✅ Properties are mutually dual`) -} - /** * Tests for all categories C,D that if C is dual to D, then D is dual to C. */ @@ -83,42 +73,6 @@ function test_mutual_category_duals() { console.info(`✅ Categories are mutually dual`) } -/** - * Tests if for a specified list of categories all properties have been decided. - * If this test fails, property assignments or implications are missing. - */ -function test_decided_categories() { - for (const category_id of decided_categories) { - test_decided_category(category_id) - } -} - -/** - * Tests for a given category if all properties have been decided, - * i.e. are either satisfied or unsatisfied. - */ -function test_decided_category(category_id: string) { - const res = db - .prepare( - `SELECT p.id FROM category_properties p WHERE NOT EXISTS - ( - SELECT 1 FROM category_property_assignments - WHERE category_id = ? AND property_id = p.id - )`, - ) - .all(category_id) as { id: string }[] - - const unknown_properties = res.map((row) => row.id) - - if (unknown_properties.length > 0) { - throw new Error( - `❌ Found unknown properties of ${category_id}:\n${unknown_properties.join(', ')}.\nEvery property needs to be decided for this category.`, - ) - } - - console.info(`✅ All properties have been decided for ${category_id}`) -} - /** * Tests that the trivial category has no unsatisfied property. * This enforces that all properties in the database are "positive". @@ -141,40 +95,83 @@ function test_properties_of_trivial_category() { } /** - * Tests if selected categories behave as expected: - * All of their properties in the database have to match those in the - * respective JSON files in the subfolder "expected-data". + * Tests for all properties p,q of categories or functors that + * if p is dual to q, then q is dual to p. */ -function test_properties_of_selected_categories() { - const expected = { - Set: Set_expected, - Ab: Ab_expected, - Top: Top_expected, - } as Record> - - for (const cat in expected) { - test_selected_category(cat, expected[cat]) +function test_mutual_property_duals(type: 'category' | 'functor') { + const dict: Record = {} + + const properties = db + .prepare(`SELECT id, dual_property_id FROM ${type}_properties`) + .all() as { id: string; dual_property_id: string | null }[] + + for (const { id, dual_property_id } of properties) { + dict[id] = dual_property_id } + + for (const id in dict) { + const dual = dict[id] + if (dual && dict[dual] !== id) { + throw new Error(`❌ Found non-mutual property duality: ${id}, ${dual}`) + } + } + + console.info(`✅ ${capitalize(type)} properties are mutually dual`) } /** - * Tests if a selected category has the expected properties. + * Tests that for a specified list of categories or functors all properties have + * been decided. If this test fails, property assignments or implications are missing. */ -function test_selected_category(category_id: string, expected: Record) { - const properties = db - .prepare( - `SELECT property_id AS id, is_satisfied - FROM category_property_assignments - WHERE category_id = ?`, - ) - .all(category_id) as { id: string; is_satisfied: number }[] - - for (const { id, is_satisfied } of properties) { - const ok = Boolean(is_satisfied) === expected[id] - if (!ok) { - throw new Error(`❌ Incorrect property of ${category_id}: ${id}`) +function test_decided_entities(entities: string[], type: 'category' | 'functor') { + const unknown_query = db.prepare( + `SELECT p.id FROM ${type}_properties p WHERE NOT EXISTS + (SELECT 1 FROM ${type}_property_assignments + WHERE ${type}_id = ? AND property_id = p.id + ) + `, + ) + + for (const entity_id of entities) { + const res = unknown_query.all(entity_id) as { id: string }[] + const unknown_properties = res.map((row) => row.id) + + if (unknown_properties.length > 0) { + throw new Error( + `❌ Found unknown properties of ${entity_id}:\n${unknown_properties.join(', ')}.\nEvery property needs to be decided for this ${type}.`, + ) } + + console.info(`✅ All properties have been decided for ${entity_id}`) } +} + +/** + * Tests if selected categories or functors behave as expected: + * All of their properties in the database have to match those in the + * respective JSON files in the subfolder "expected-data". + */ +function test_properties_of_selected_entities( + expected: Record>, + type: 'category' | 'functor', +) { + const property_query = db.prepare( + `SELECT property_id, is_satisfied FROM ${type}_property_assignments + WHERE ${type}_id = ?`, + ) + + for (const entity_id in expected) { + const properties = property_query.all(entity_id) as { + property_id: string + is_satisfied: 0 | 1 + }[] + + for (const { property_id, is_satisfied } of properties) { + const ok = Boolean(is_satisfied) === expected[entity_id][property_id] + if (ok) continue + throw new Error(`❌ Incorrect property of ${entity_id}: ${property_id}`) + } - console.info(`✅ Properties of ${category_id} are correct`) + console.info(`✅ Properties of ${entity_id} are correct`) + } } diff --git a/databases/catdat/scripts/utils/categories.ts b/databases/catdat/scripts/utils/categories.ts index e0aa3e209..e0dfd5a5d 100644 --- a/databases/catdat/scripts/utils/categories.ts +++ b/databases/catdat/scripts/utils/categories.ts @@ -1,9 +1,10 @@ import { type Database } from 'better-sqlite3' +import { parse_json_set } from './helpers' -export type CategoryMeta = { +type CategoryMeta = { id: string name: string - dual_category_id: string | null + dual: string | null } export type NormalizedCategoryImplication = { @@ -12,21 +13,13 @@ export type NormalizedCategoryImplication = { conclusion: string } -export type CategoryPropertyMeta = { - id: string - dual_property_id: string | null - relation: string - negation: string - conditional: string -} - /** * Returns the list of categories saved in the database. */ export function get_categories(db: Database) { return db .prepare( - `SELECT id, name, dual_category_id + `SELECT id, name, dual_category_id as dual FROM categories ORDER BY lower(name)`, ) .all() as CategoryMeta[] @@ -44,39 +37,33 @@ export function get_categories(db: Database) { export function get_normalized_category_implications( db: Database, ): NormalizedCategoryImplication[] { - type ImplicationDB = { - id: string - assumptions: string - conclusions: string - is_equivalence: number - } - const all_implications_db = db .prepare( `SELECT id, assumptions, conclusions, is_equivalence FROM category_implications_view`, ) - .all() as ImplicationDB[] + .all() as { + id: string + assumptions: string + conclusions: string + is_equivalence: 0 | 1 + }[] const implications: NormalizedCategoryImplication[] = [] for (const impl of all_implications_db) { - const assumptions: string[] = JSON.parse(impl.assumptions) - const conclusions: string[] = JSON.parse(impl.conclusions) + const assumptions = parse_json_set(impl.assumptions) + const conclusions = parse_json_set(impl.conclusions) for (const conclusion of conclusions) { - implications.push({ - id: impl.id, - assumptions: new Set(assumptions), - conclusion, - }) + implications.push({ id: impl.id, assumptions, conclusion }) } if (impl.is_equivalence) { for (const assumption of assumptions) { implications.push({ id: impl.id, - assumptions: new Set(conclusions), + assumptions: conclusions, conclusion: assumption, }) } @@ -86,106 +73,6 @@ export function get_normalized_category_implications( return implications } -/** - * Returns a dictionary of properties saved in the database. - */ -export function get_properties_dict(db: Database) { - const properties = db - .prepare( - `SELECT - p.id, p.dual_property_id, p.relation, - r.negation, r.conditional - FROM category_properties p - INNER JOIN relations r ON r.relation = p.relation - ORDER BY lower(p.id)`, - ) - .all() as CategoryPropertyMeta[] - - const dict: Record = {} - - for (const p of properties) dict[p.id] = p - - return dict -} - -/** - * Returns a dictionary with all assigned properties of categories, - * grouped by category and value (satisfied / unsatisfied). - */ -export function get_property_assignments(db: Database, categories: { id: string }[]) { - const rows = db - .prepare( - `SELECT property_id, category_id, is_satisfied - FROM category_property_assignments`, - ) - .all() as { property_id: string; category_id: string; is_satisfied: number }[] - - const grouped: Record; unsatisfied: Set }> = - {} - - for (const category of categories) { - grouped[category.id] = { satisfied: new Set(), unsatisfied: new Set() } - } - - for (const row of rows) { - const { property_id, category_id, is_satisfied } = row - grouped[category_id][is_satisfied ? 'satisfied' : 'unsatisfied'].add(property_id) - } - - return grouped -} - -/** - * Returns a dictionary with all assigned properties of categories, - * grouped by category, value (satisfied / unsatisfied), and deduced status. - */ -export function get_property_assignments_by_deduction( - db: Database, - categories: { id: string }[], -) { - const rows = db - .prepare( - `SELECT property_id, category_id, is_satisfied, is_deduced - FROM category_property_assignments`, - ) - .all() as { - property_id: string - category_id: string - is_satisfied: number - is_deduced: number - }[] - - const grouped: Record< - string, - { - satisfied: { - non_deduced: Set - deduced: Set - } - unsatisfied: { - non_deduced: Set - deduced: Set - } - } - > = {} - - for (const category of categories) { - grouped[category.id] = { - satisfied: { non_deduced: new Set(), deduced: new Set() }, - unsatisfied: { non_deduced: new Set(), deduced: new Set() }, - } - } - - for (const row of rows) { - const { property_id, category_id, is_satisfied, is_deduced } = row - grouped[category_id][is_satisfied ? 'satisfied' : 'unsatisfied'][ - is_deduced ? 'deduced' : 'non_deduced' - ].add(property_id) - } - - return grouped -} - /** * Returns a dictionary mapping a category to the set of its assigned * properties (satisfied or unsatisfied) that should not be checked diff --git a/databases/catdat/scripts/utils/deduction.ts b/databases/catdat/scripts/utils/deduction.ts index a48dac564..01d670a71 100644 --- a/databases/catdat/scripts/utils/deduction.ts +++ b/databases/catdat/scripts/utils/deduction.ts @@ -1,185 +1,160 @@ -import { is_subset } from './helpers' +import { type Database } from 'better-sqlite3' +import { get_categories, get_normalized_category_implications } from './categories' +import { get_functors, get_normalized_functor_implications } from './functors' -type NormalizedImplication = { +/** + * An entity is a category or a functor. + */ +export type EntityMeta = { + id: string + name: string + dual?: string | null + // used for source and target properties of a functor + associated_satisfied_properties?: Record> +} + +export type NormalizedImplication = { id: string assumptions: Set conclusion: string + // used for source and target assumptions of a functor in an implication + associated_assumptions?: Record> } -type PropertyMeta = { +export type PropertyMeta = { id: string - dual_property_id: string | null + dual: string | null relation: string negation: string conditional: string } -export function get_assumption_string( - implication: NormalizedImplication, - properties_dict: Record, - conditional = false, -): string { - const { assumptions } = implication - - return Array.from(assumptions) - .map( - (assumption) => - `${properties_dict[assumption][conditional ? 'conditional' : 'relation']} ${assumption}`, - ) - .join(' and ') -} - -export function get_conclusion_string( - implication: NormalizedImplication, - properties_dict: Record, - conditional = false, -): string { - const { conclusion } = implication - - return `${properties_dict[conclusion][conditional ? 'conditional' : 'relation']} ${conclusion}` +/** + * Returns the list of entities saved in the database of a given type. + */ +export function get_entities(db: Database, type: 'category' | 'functor'): EntityMeta[] { + if (type === 'category') return get_categories(db) + if (type === 'functor') return get_functors(db) + throw new Error('Unsupported type') } -function get_reason_string( - implication: NormalizedImplication, - properties_dict: Record, -) { - const assumption_string = get_assumption_string(implication, properties_dict) - const conclusion_string = get_conclusion_string(implication, properties_dict) - - const ref = `by this result` - return `Since it ${assumption_string}, it ${conclusion_string} (${ref}).` +/** + * Returns the list of normalized implications saved in the database of a given type. + */ +export function get_normalized_implications( + db: Database, + type: 'category' | 'functor', +): NormalizedImplication[] { + if (type === 'category') return get_normalized_category_implications(db) + if (type === 'functor') return get_normalized_functor_implications(db) + throw new Error('Unsupported type') } -function get_contradiction_string( - implication: NormalizedImplication, - properties_dict: Record, - property: string, -) { - const assumption_string = get_assumption_string(implication, properties_dict, true) - const conclusion_string = get_conclusion_string(implication, properties_dict, true) - - const has_multiple_assumptions = implication.assumptions.size > 1 +/** + * Returns a dictionary of properties saved in the database. + */ +export function get_properties_dict(db: Database, type: 'category' | 'functor') { + const properties = db + .prepare( + `SELECT + p.id, p.dual_property_id as dual, p.relation, + r.negation, r.conditional + FROM ${type}_properties p + INNER JOIN relations r ON r.relation = p.relation + ORDER BY lower(p.id)`, + ) + .all() as PropertyMeta[] - const ref = `by this result` + const dict: Record = {} - const contra = `Assume for contradiction that it ${properties_dict[property].relation} ${property}` + for (const p of properties) dict[p.id] = p - return has_multiple_assumptions - ? `${contra}. Then it ${assumption_string}, so it ${conclusion_string} (${ref}) – contradiction.` - : `${contra}. Then it ${conclusion_string} (${ref}) – contradiction.` + return dict } /** - * Returns the set of satisfied properties that can be deduced from a set - * of satisfied properties, based on a list of normalized implications. If a - * property dictionary is provided, human-readable reasons are generated as well. + * Returns a dictionary with all assigned properties of a list of entities + * (categories or functors), grouped by id and value (satisfied / unsatisfied). */ -export function get_deduced_satisfied_properties( - satisfied_properties: Set, - implications: NormalizedImplication[], - options: { - properties_dict?: Record - stop_when_found?: string - }, +export function get_property_assignments( + db: Database, + entities: { id: string }[], + type: 'category' | 'functor', ) { - const found = new Set() - const reasons: Record = {} - const deduced_satisfied_properties = new Set(satisfied_properties) - - while (true) { - const newly_found = new Set() - - for (const implication of implications) { - const is_valid = - is_subset(implication.assumptions, deduced_satisfied_properties) && - !deduced_satisfied_properties.has(implication.conclusion) && - !newly_found.has(implication.conclusion) - - if (!is_valid) continue - - newly_found.add(implication.conclusion) - found.add(implication.conclusion) - - if (options?.stop_when_found === implication.conclusion) { - deduced_satisfied_properties.add(implication.conclusion) - return { deduced_satisfied_properties, found, reasons } - } - - if (options.properties_dict) { - reasons[implication.conclusion] = get_reason_string( - implication, - options.properties_dict, - ) - } - } + const rows = db + .prepare( + `SELECT property_id, ${type}_id as entity_id, is_satisfied + FROM ${type}_property_assignments`, + ) + .all() as { property_id: string; entity_id: string; is_satisfied: 0 | 1 }[] - for (const p of newly_found) deduced_satisfied_properties.add(p) + const grouped: Record; unsatisfied: Set }> = + {} + + for (const entity of entities) { + grouped[entity.id] = { satisfied: new Set(), unsatisfied: new Set() } + } - if (!newly_found.size) break + for (const row of rows) { + const { property_id, entity_id, is_satisfied } = row + grouped[entity_id][is_satisfied ? 'satisfied' : 'unsatisfied'].add(property_id) } - return { deduced_satisfied_properties, found, reasons } + return grouped } /** - * Returns the set of unsatisfied properties that can be deduced from - * a set of satisfied properties and a set of unsatisfied properties, - * based on a list of normalized implications. If a property dictionary - * is provided, human-readable reasons are generated as well. + * Returns a dictionary with all assigned properties of entities, + * grouped by entity, value (satisfied / unsatisfied), and deduced status. */ -export function get_deduced_unsatisfied_properties( - satisfied_properties: Set, - unsatisfied_properties: Set, - implications: NormalizedImplication[], - options: { - properties_dict?: Record - stop_when_found?: string - }, +export function get_property_assignments_by_deduction( + db: Database, + entities: { id: string }[], + type: 'category' | 'functor', ) { - const found = new Set() - const reasons: Record = {} - const deduced_unsatisfied_properties = new Set(unsatisfied_properties) - - while (true) { - const newly_found = new Set() - - for (const implication of implications) { - if (!deduced_unsatisfied_properties.has(implication.conclusion)) continue - for (const p of implication.assumptions) { - const is_valid = - !deduced_unsatisfied_properties.has(p) && - !newly_found.has(p) && - is_subset(implication.assumptions, satisfied_properties, { - exception: p, - }) - if (!is_valid) continue - - if (satisfied_properties.has(p)) { - throw new Error(`Contradiction has been found for: ${p}`) - } - - if (options?.stop_when_found === p) { - deduced_unsatisfied_properties.add(p) - return { deduced_unsatisfied_properties, found, reasons } - } - - newly_found.add(p) - found.add(p) - - if (options.properties_dict) { - reasons[p] = get_contradiction_string( - implication, - options.properties_dict, - p, - ) - } - } + const rows = db + .prepare( + `SELECT property_id, ${type}_id as entity_id, is_satisfied, is_deduced + FROM ${type}_property_assignments`, + ) + .all() as { + property_id: string + entity_id: string + is_satisfied: 0 | 1 + is_deduced: 0 | 1 + }[] + + const grouped: Record< + string, + { + satisfied: { non_deduced: Set; deduced: Set } + unsatisfied: { non_deduced: Set; deduced: Set } } + > = {} - for (const p of newly_found) deduced_unsatisfied_properties.add(p) + for (const entity of entities) { + grouped[entity.id] = { + satisfied: { non_deduced: new Set(), deduced: new Set() }, + unsatisfied: { non_deduced: new Set(), deduced: new Set() }, + } + } - if (!newly_found.size) break + for (const row of rows) { + const { property_id, entity_id, is_satisfied, is_deduced } = row + grouped[entity_id][is_satisfied ? 'satisfied' : 'unsatisfied'][ + is_deduced ? 'deduced' : 'non_deduced' + ].add(property_id) } - return { deduced_unsatisfied_properties, found, reasons } + return grouped +} + +/** + * Checks if an entity is a dual, but not the + * original entity to prevent circular reasoning. + */ +export function is_dual_entity( + entity: EntityMeta, +): entity is EntityMeta & { dual: string } { + return Boolean(entity.dual) && entity.name.toLowerCase().startsWith('dual') } diff --git a/databases/catdat/scripts/utils/functors.ts b/databases/catdat/scripts/utils/functors.ts new file mode 100644 index 000000000..2a9731485 --- /dev/null +++ b/databases/catdat/scripts/utils/functors.ts @@ -0,0 +1,132 @@ +import { type Database } from 'better-sqlite3' +import { parse_json_set } from './helpers' + +type FunctorMeta = { + id: string + name: string + associated_satisfied_properties: { + source: Set + target: Set + } +} + +type NormalizedFunctorImplication = { + id: string + assumptions: Set + conclusion: string + associated_assumptions: { + source: Set + target: Set + } +} + +/** + * Returns the list of functors saved in the database along with + * the satisfied properties of their source and target category. + */ +export function get_functors(db: Database): FunctorMeta[] { + const rows = db + .prepare( + `SELECT + id, name, source, target, + ( + SELECT json_group_array(property_id) FROM ( + SELECT property_id + FROM category_property_assignments + WHERE category_id = source AND is_satisfied = TRUE + ) + ) as source_props, + ( + SELECT json_group_array(property_id) FROM ( + SELECT property_id + FROM category_property_assignments + WHERE category_id = target AND is_satisfied = TRUE + ) + ) as target_props + FROM functors + ORDER BY lower(name)`, + ) + .all() as { + id: string + name: string + source: string + target: string + source_props: string + target_props: string + }[] + + return rows.map((row) => ({ + id: row.id, + name: row.name, + associated_satisfied_properties: { + source: parse_json_set(row.source_props), + target: parse_json_set(row.target_props), + }, + })) +} + +/** + * Implications have the form + * P_1 + ... + P_n ===> Q_1 + ... + Q_m + * or + * P_1 + ... + P_n <===> Q_1 + ... + Q_m. + * This function decomposes them into normalized implications, + * which have the form + * P_1 + ... + P_n ===> Q. + */ +export function get_normalized_functor_implications( + db: Database, +): NormalizedFunctorImplication[] { + const all_implications_db = db + .prepare( + `SELECT + id, assumptions, source_assumptions, target_assumptions, + conclusions, is_equivalence + FROM functor_implications_view`, + ) + .all() as { + id: string + assumptions: string + source_assumptions: string + target_assumptions: string + conclusions: string + is_equivalence: 0 | 1 + }[] + + const implications: NormalizedFunctorImplication[] = [] + + for (const impl of all_implications_db) { + const assumptions = parse_json_set(impl.assumptions) + const conclusions = parse_json_set(impl.conclusions) + const source_assumptions = parse_json_set(impl.source_assumptions) + const target_assumptions = parse_json_set(impl.target_assumptions) + + for (const conclusion of conclusions) { + implications.push({ + id: impl.id, + assumptions, + conclusion, + associated_assumptions: { + source: source_assumptions, + target: target_assumptions, + }, + }) + } + + if (impl.is_equivalence) { + for (const assumption of assumptions) { + implications.push({ + id: impl.id, + assumptions: conclusions, + conclusion: assumption, + associated_assumptions: { + source: source_assumptions, + target: target_assumptions, + }, + }) + } + } + } + + return implications +} diff --git a/databases/catdat/scripts/utils/helpers.ts b/databases/catdat/scripts/utils/helpers.ts index 296c0ed40..fe7e31c5f 100644 --- a/databases/catdat/scripts/utils/helpers.ts +++ b/databases/catdat/scripts/utils/helpers.ts @@ -12,6 +12,14 @@ export function is_subset(a: Set, b: Set, options?: { exception: T }) { return true } +export function capitalize(txt: string) { + return txt[0].toUpperCase() + txt.slice(1) +} + +export function parse_json_set(json: string): Set { + return new Set(JSON.parse(json)) +} + export function get_client() { const db_path = path.resolve('databases', 'catdat', 'catdat.db') const db = new Database(db_path, { readonly: false }) diff --git a/databases/catdat/scripts/utils/implications.ts b/databases/catdat/scripts/utils/implications.ts new file mode 100644 index 000000000..b37eca5d5 --- /dev/null +++ b/databases/catdat/scripts/utils/implications.ts @@ -0,0 +1,108 @@ +import { type Database } from 'better-sqlite3' +import type { NormalizedImplication, PropertyMeta } from './deduction' +import { are_equal_sets, parse_json_set } from './helpers' + +function get_assumption_string( + implication: NormalizedImplication, + properties_dict: Record, + conditional = false, +): string { + const { assumptions } = implication + + return Array.from(assumptions) + .map( + (assumption) => + `${properties_dict[assumption][conditional ? 'conditional' : 'relation']} ${assumption}`, + ) + .join(' and ') +} + +function get_conclusion_string( + implication: NormalizedImplication, + properties_dict: Record, + conditional = false, +): string { + const { conclusion } = implication + + return `${properties_dict[conclusion][conditional ? 'conditional' : 'relation']} ${conclusion}` +} + +export function get_reason_string( + implication: NormalizedImplication, + properties_dict: Record, + type: 'category' | 'functor', +) { + const assumption_string = get_assumption_string(implication, properties_dict) + const conclusion_string = get_conclusion_string(implication, properties_dict) + + const ref = `by this result` + return `Since it ${assumption_string}, it ${conclusion_string} (${ref}).` +} + +export function get_contradiction_string( + implication: NormalizedImplication, + properties_dict: Record, + property: string, + type: 'category' | 'functor', +) { + const assumption_string = get_assumption_string(implication, properties_dict, true) + const conclusion_string = get_conclusion_string(implication, properties_dict, true) + + const has_multiple_assumptions = implication.assumptions.size > 1 + + const ref = `by this result` + + const contra = `Assume for contradiction that it ${properties_dict[property].relation} ${property}` + + return has_multiple_assumptions + ? `${contra}. Then it ${assumption_string}, so it ${conclusion_string} (${ref}) – contradiction.` + : `${contra}. Then it ${conclusion_string} (${ref}) – contradiction.` +} + +/** + * Clears all deduced implications. This is done before the deduction starts. + */ +export function clear_deduced_implications(db: Database, type: 'category' | 'functor') { + db.prepare(`DELETE FROM ${type}_implications WHERE is_deduced = TRUE`).run() +} + +type EntityImplicationWithDualProperties = { + assumptions: string + conclusions: string + dual_assumptions: string + dual_conclusions: string + dual_source_assumptions?: string + dual_target_assumptions?: string +} + +/** + * Checks if an implication can be dualized (i.e. if all the involved properties + * have a dual) and if the dual is different from it. + */ +export function is_dualizable(impl: EntityImplicationWithDualProperties): boolean { + const assumptions = parse_json_set(impl.assumptions) + const conclusions = parse_json_set(impl.conclusions) + const dual_assumptions = parse_json_set(impl.dual_assumptions) + const dual_conclusions = parse_json_set(impl.dual_conclusions) + + if (dual_assumptions.has(null) || dual_conclusions.has(null)) return false + + if (impl.dual_source_assumptions) { + const dual_source_assumptions = parse_json_set( + impl.dual_source_assumptions, + ) + if (dual_source_assumptions.has(null)) return false + } + + if (impl.dual_target_assumptions) { + const dual_target_assumptions = parse_json_set( + impl.dual_target_assumptions, + ) + if (dual_target_assumptions.has(null)) return false + } + + return !( + are_equal_sets(assumptions, dual_assumptions) && + are_equal_sets(conclusions, dual_conclusions) + ) +} diff --git a/databases/catdat/scripts/utils/schema.ts b/databases/catdat/scripts/utils/schema.ts index b83b2f48c..9ba778ed8 100644 --- a/databases/catdat/scripts/utils/schema.ts +++ b/databases/catdat/scripts/utils/schema.ts @@ -14,6 +14,10 @@ export function create_schema_hash(): string { return sha256_hex(schema) } +function sha256_hex(input: string): string { + return createHash('sha256').update(input).digest('hex') +} + export function write_schema_hash(hash: string) { fs.writeFileSync( path.join(schema_folder, 'schema.json'), @@ -31,7 +35,3 @@ export function get_saved_schema_hash() { return '' } } - -export function sha256_hex(input: string): string { - return createHash('sha256').update(input).digest('hex') -} diff --git a/src/components/ImplicationItem.svelte b/src/components/CategoryImplicationItem.svelte similarity index 94% rename from src/components/ImplicationItem.svelte rename to src/components/CategoryImplicationItem.svelte index 868d74426..b563cb0d7 100644 --- a/src/components/ImplicationItem.svelte +++ b/src/components/CategoryImplicationItem.svelte @@ -21,7 +21,7 @@ {#each implication.assumptions as assumption, i} {assumption} {#if i < implication.assumptions.length - 1} @@ -49,7 +49,7 @@ {#each implication.conclusions as conclusion, i} {conclusion} {#if i < implication.conclusions.length - 1} diff --git a/src/components/ImplicationList.svelte b/src/components/CategoryImplicationList.svelte similarity index 72% rename from src/components/ImplicationList.svelte rename to src/components/CategoryImplicationList.svelte index 76918f67d..b1151447d 100644 --- a/src/components/ImplicationList.svelte +++ b/src/components/CategoryImplicationList.svelte @@ -1,6 +1,6 @@ {#if properties.length} diff --git a/src/lib/commons/property.url.ts b/src/lib/commons/property.url.ts index 4f758e846..3a25af5d7 100644 --- a/src/lib/commons/property.url.ts +++ b/src/lib/commons/property.url.ts @@ -24,6 +24,6 @@ export function decode_property_ID(str: string): string { return decoded } -export function get_property_url(id: string, type: 'category' | 'functor' = 'category') { +export function get_property_url(id: string, type: 'category' | 'functor') { return `/${type}-property/${encode_property_ID(id)}` } diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index 679f2440d..bed2e1ef2 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -27,11 +27,11 @@ export type CommentObject = { id: number; comment: string } export type ImplicationDB = { id: string - is_equivalence: number + is_equivalence: 0 | 1 reason: string assumptions: string conclusions: string - is_deduced: number + is_deduced: 0 | 1 dualized_from?: string | null } @@ -51,7 +51,7 @@ export type PropertyDB = { description: string dual_property_id: string | null nlab_link: string | null - invariant_under_equivalences: number + invariant_under_equivalences: 0 | 1 } export type PropertyDisplay = Replace< @@ -70,7 +70,7 @@ export type CategoryPropertyDB = { id: string reason: string relation: string - is_deduced: number + is_deduced: 0 | 1 } export type CategoryProperty = Replace @@ -109,7 +109,7 @@ export type FunctorPropertyDB = { relation: string description: string nlab_link: string | null - invariant_under_equivalences: number + invariant_under_equivalences: 0 | 1 dual_property_id: string | null } @@ -124,7 +124,7 @@ export type FunctorProperty = Replace< export type FunctorImplicationDB = { id: string - is_equivalence: number + is_equivalence: 0 | 1 reason: string assumptions: string conclusions: string @@ -148,7 +148,7 @@ export type FunctorPropertyAssignmentDB = { id: string reason: string relation: string - is_deduced: number + is_deduced: 0 | 1 } export type FunctorPropertyAssignment = Replace< diff --git a/src/lib/server/consistency.ts b/src/lib/server/consistency.ts index ce09f3d14..5a6caee16 100644 --- a/src/lib/server/consistency.ts +++ b/src/lib/server/consistency.ts @@ -108,7 +108,7 @@ function get_normalized_category_implications() { id: string assumptions: string conclusions: string - is_equivalence: number + is_equivalence: 0 | 1 }>( sql`SELECT id, assumptions, conclusions, is_equivalence FROM category_implications_view`, ) @@ -118,22 +118,18 @@ function get_normalized_category_implications() { const implications: NormalizedCategoryImplication[] = [] for (const impl of rows) { - const assumptions: string[] = JSON.parse(impl.assumptions) - const conclusions: string[] = JSON.parse(impl.conclusions) + const assumptions = new Set(JSON.parse(impl.assumptions)) + const conclusions = new Set(JSON.parse(impl.conclusions)) for (const conclusion of conclusions) { - implications.push({ - id: impl.id, - assumptions: new Set(assumptions), - conclusion, - }) + implications.push({ id: impl.id, assumptions, conclusion }) } if (impl.is_equivalence) { for (const assumption of assumptions) { implications.push({ id: impl.id, - assumptions: new Set(conclusions), + assumptions: conclusions, conclusion: assumption, }) } diff --git a/src/routes/category-comparison/[...ids]/+page.svelte b/src/routes/category-comparison/[...ids]/+page.svelte index a1082c623..085b7fa89 100644 --- a/src/routes/category-comparison/[...ids]/+page.svelte +++ b/src/routes/category-comparison/[...ids]/+page.svelte @@ -66,7 +66,7 @@ {@const is_different = new Set(values).size > 1} - {property} + {property} {#each compared_categories as _, i} {@const value = values[i]} diff --git a/src/routes/category-implication/[id]/+page.svelte b/src/routes/category-implication/[id]/+page.svelte index eb40ce10a..344b3d18d 100644 --- a/src/routes/category-implication/[id]/+page.svelte +++ b/src/routes/category-implication/[id]/+page.svelte @@ -18,7 +18,7 @@ Assumptions: {#each data.implication.assumptions as property, index} - {property}{property}{#if index < data.implication.assumptions.length - 1} ,  {/if} @@ -28,7 +28,7 @@

Conclusions: {#each data.implication.conclusions as property, index} - {property}{property}{#if index < data.implication.conclusions.length - 1} ,  {/if} diff --git a/src/routes/category-implications/+page.svelte b/src/routes/category-implications/+page.svelte index 6c08c0111..02acfe9f2 100644 --- a/src/routes/category-implications/+page.svelte +++ b/src/routes/category-implications/+page.svelte @@ -1,7 +1,7 @@