Fix deduction of dual categories + Refactoring

scripts/deduce-category-implications.ts

@@ -1,19 +1,27 @@
-import { type Client } from '@libsql/client'
+import type { Client } from '@libsql/client'
 import { are_equal_sets } from './shared'
-import dotenv from 'dotenv'
-
-dotenv.config({ quiet: true })
 
+/**
+ * Deduces implications from given ones.
+ */
 export async function deduce_category_implications(db: Client) {
 	await clear_deduced_category_implications(db)
 	await create_dualized_category_implications(db)
 	await create_self_dual_category_implications(db)
 }
 
+/**
+ * Clears all deduced implications. This is done as a first step.
+ */
 async function clear_deduced_category_implications(db: Client) {
 	await db.execute(`DELETE FROM implications WHERE is_deduced = TRUE`)
 }
 
+/**
+ * Dualizes all implications 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.
+ */
 async function create_dualized_category_implications(db: Client) {
 	const res = await db.execute(`
         SELECT
@@ -91,6 +99,10 @@ async function create_dualized_category_implications(db: Client) {
 	console.info(`Dualized ${dualizable_implications.length} category implications`)
 }
 
+/**
+ * Creates all trivial implications of the form
+ * self-dual + P ===> P^op
+ */
 async function create_self_dual_category_implications(db: Client) {
 	const { rows } = await db.execute(`
         INSERT INTO implication_input (

scripts/deduce-category-properties.ts

@@ -1,20 +1,21 @@
 import type { Transaction, Client } from '@libsql/client'
-import dotenv from 'dotenv'
 import {
 	get_assumption_string,
 	get_conclusion_string,
 	is_subset,
 	NormalizedCategoryImplication,
 } from './shared'
 
-dotenv.config({ quiet: true })
-
 type CategoryMeta = {
 	id: string
 	name: string
 	dual_category_id: string | null
 }
 
+/**
+ * Deduce properties of categories from given ones
+ * by using the list of implications.
+ */
 export async function deduce_category_properties(db: Client) {
 	const tx = await db.transaction()
 
@@ -30,7 +31,19 @@ export async function deduce_category_properties(db: Client) {
 		}
 
 		for (const category of categories) {
+			const allowed =
+				category.dual_category_id !== null &&
+				category.name.toLowerCase().startsWith('dual') // prevent circular deduction
+
+			if (!allowed) continue
+
 			await deduce_dual_category_properties(tx, category)
+			await deduce_satisfied_category_properties(tx, category.id, implications, {
+				check_conflicts: false,
+			})
+			await deduce_unsatisfied_category_properties(tx, category.id, implications, {
+				check_conflicts: false,
+			})
 		}
 
 		await tx.commit()
@@ -41,6 +54,20 @@ export async function deduce_category_properties(db: Client) {
 	}
 }
 
+/**
+ * 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
+ */
 async function get_normalized_category_implications(
 	tx: Transaction,
 ): Promise<NormalizedCategoryImplication[]> {
@@ -101,6 +128,9 @@ async function get_normalized_category_implications(
 	return implications
 }
 
+/**
+ * Returns the list of categories saved in the database.
+ */
 async function get_categories(tx: Transaction) {
 	const res = await tx.execute(`
 		SELECT id, name, dual_category_id
@@ -109,6 +139,10 @@ async function get_categories(tx: Transaction) {
 	return res.rows as unknown as CategoryMeta[]
 }
 
+/**
+ * Clears all the deduced properties.
+ * This runs before the deduction starts.
+ */
 async function delete_deduced_category_properties(tx: Transaction, category_id: string) {
 	await tx.execute({
 		sql: `
@@ -119,26 +153,38 @@ async function delete_deduced_category_properties(tx: Transaction, category_id:
 	})
 }
 
-async function deduce_satisfied_category_properties(
+/**
+ * Returns the list of properties that are satisfied or unsatisfied
+ * for a given category.
+ */
+async function get_decided_properties(
 	tx: Transaction,
 	category_id: string,
-	implications: NormalizedCategoryImplication[],
+	value: boolean,
 ) {
-	const satisfied_res = await tx.execute({
+	const res = await tx.execute({
 		sql: `
 			SELECT property_id
 			FROM category_property_assignments
-			WHERE
-				category_id = ?
-				AND is_satisfied = TRUE
-				AND is_deduced = FALSE
+			WHERE category_id = ? AND is_satisfied = ?
 		`,
-		args: [category_id],
+		args: [category_id, value],
 	})
 
-	const satisfied_props = new Set(
-		satisfied_res.rows.map((row) => row.property_id) as string[],
-	) as Set<string>
+	return new Set(res.rows.map((row) => row.property_id) as string[])
+}
+
+/**
+ * Deduce satisfied properties for a given category from given ones
+ * by using the list of normalized implications.
+ */
+async function deduce_satisfied_category_properties(
+	tx: Transaction,
+	category_id: string,
+	implications: NormalizedCategoryImplication[],
+	options: { check_conflicts: boolean } = { check_conflicts: true },
+) {
+	const satisfied_props = await get_decided_properties(tx, category_id, true)
 
 	const deduced_satisfied_props: string[] = []
 	const reasons: Record<string, string> = {}
@@ -175,13 +221,14 @@ async function deduce_satisfied_category_properties(
 			values.push(category_id, id, reasons[id], i + 1)
 		}
 
-		const insert_sql = `
-			INSERT INTO category_property_assignments (
-				category_id, property_id, is_satisfied, reason, position, is_deduced
-			)
-			VALUES
-			${value_fragments.join(',\n')}
-		`
+		const insert_sql = options.check_conflicts
+			? `INSERT INTO category_property_assignments
+				(category_id, property_id, is_satisfied, reason, position, is_deduced)
+				VALUES ${value_fragments.join(',\n')}`
+			: `INSERT INTO category_property_assignments
+				(category_id, property_id, is_satisfied, reason, position, is_deduced)
+				VALUES ${value_fragments.join(',\n')}
+				ON CONFLICT (category_id, property_id) DO NOTHING`
 
 		await tx.execute({ sql: insert_sql, args: values })
 	}
@@ -191,39 +238,18 @@ async function deduce_satisfied_category_properties(
 	)
 }
 
+/**
+ * Deduce unsatisfied properties for a given category from given ones
+ * by using the satisfied properties and the list of normalized implications.
+ */
 async function deduce_unsatisfied_category_properties(
 	tx: Transaction,
 	category_id: string,
 	implications: NormalizedCategoryImplication[],
+	options: { check_conflicts: boolean } = { check_conflicts: true },
 ) {
-	const satisfied_res = await tx.execute({
-		sql: `
-			SELECT property_id
-			FROM category_property_assignments
-			WHERE category_id = ? AND is_satisfied = TRUE
-		`,
-		args: [category_id],
-	})
-
-	const satisfied_props = new Set(
-		satisfied_res.rows.map((row) => row.property_id) as string[],
-	)
-
-	const unsatisfied_res = await tx.execute({
-		sql: `
-			SELECT property_id
-			FROM category_property_assignments
-			WHERE
-				category_id = ?
-				AND is_satisfied = FALSE
-				AND is_deduced = FALSE
-		`,
-		args: [category_id],
-	})
-
-	const unsatisfied_props = new Set(
-		unsatisfied_res.rows.map((row) => row.property_id) as string[],
-	)
+	const satisfied_props = await get_decided_properties(tx, category_id, true)
+	const unsatisfied_props = await get_decided_properties(tx, category_id, false)
 
 	const deduced_unsatisfied_props: string[] = []
 	const reasons: Record<string, string> = {}
@@ -278,12 +304,14 @@ async function deduce_unsatisfied_category_properties(
 			values.push(category_id, id, reasons[id], i + 1)
 		}
 
-		const insert_query = `
-			INSERT INTO category_property_assignments (
-				category_id, property_id, is_satisfied, reason, position, is_deduced
-			)
-			VALUES
-			${value_fragments.join(',\n')}`
+		const insert_query = options.check_conflicts
+			? `INSERT INTO category_property_assignments
+				(category_id, property_id, is_satisfied, reason, position, is_deduced)
+				VALUES ${value_fragments.join(',\n')}`
+			: `INSERT INTO category_property_assignments
+				(category_id, property_id, is_satisfied, reason, position, is_deduced)
+				VALUES ${value_fragments.join(',\n')}
+				ON CONFLICT (category_id, property_id) DO NOTHING`
 
 		await tx.execute({ sql: insert_query, args: values })
 	}
@@ -293,13 +321,11 @@ async function deduce_unsatisfied_category_properties(
 	)
 }
 
+/**
+ * Assign dual properties to dual categories:
+ * If C has property P, then C^op has property P^op (if defined).
+ */
 async function deduce_dual_category_properties(tx: Transaction, category: CategoryMeta) {
-	const allowed =
-		category.dual_category_id !== null &&
-		category.name.toLowerCase().startsWith('dual') // prevent circular deduction
-
-	if (!allowed) return
-
 	const res = await tx.execute({
 		sql: `
 			INSERT OR REPLACE INTO category_property_assignments
@@ -318,7 +344,9 @@ async function deduce_dual_category_properties(tx: Transaction, category: Catego
 			FROM category_property_assignments a
 			INNER JOIN properties p ON p.id = a.property_id
 			INNER JOIN relations r ON r.relation= p.relation
-			WHERE a.category_id = ? AND p.dual_property_id IS NOT NULL
+			WHERE
+				a.category_id = ?
+				AND p.dual_property_id IS NOT NULL				
 			ORDER BY lower(p.dual_property_id)
 		`,
 		args: [category.id, category.dual_category_id],

scripts/deduce-functor-implications.ts

@@ -1,20 +1,29 @@
-import { type Client } from '@libsql/client'
+import type { Client } from '@libsql/client'
 import { are_equal_sets } from './shared'
-import dotenv from 'dotenv'
-
-dotenv.config({ quiet: true })
 
 // TODO: remove code duplication with category implication deduction script
 
+/**
+ * Deduces functor implications from given ones.
+ */
 export async function deduce_functor_implications(db: Client) {
 	await clear_deduced_functor_implications(db)
 	await create_dualized_functor_implications(db)
 }
 
+/**
+ * Clears all deduced functor implications. This is done as a first step.
+ */
 async function clear_deduced_functor_implications(db: Client) {
 	await db.execute(`DELETE FROM functor_implications WHERE is_deduced = TRUE`)
 }
 
+/**
+ * Dualizes all functor implications 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.
+ */
 async function create_dualized_functor_implications(db: Client) {
 	const res = await db.execute(`
         SELECT