unify functions to fetch normalized implications

Author: ScriptRaccoon

databases/catdat/scripts/deduce-structure-properties.ts

@@ -7,15 +7,18 @@ import { type Database, SqliteError } from 'better-sqlite3'
 import { get_client, is_subset } from './utils/helpers'
 import {
 	get_structures,
-	get_normalized_implications,
 	get_properties_dict,
 	get_property_assignments,
 	is_dual_structure,
 	type StructureMeta,
-	type NormalizedImplication,
 	type PropertyMeta,
 } from './utils/deduction'
-import { get_contradiction_string, get_proof_string } from './utils/implications'
+import {
+	get_contradiction_string,
+	get_normalized_functor_implications,
+	get_proof_string,
+	type NormalizedImplication,
+} from './utils/implications'
 import type { StructureType } from './config'
 
 /**
@@ -31,8 +34,8 @@ export function get_deduced_satisfied_properties(
 		stop_when_found?: string
 	},
 	type: StructureType,
-	// used for source and target properties of a functor
-	associated_satisfied_properties?: Record<string, Set<string>>,
+	source_props?: Set<string>,
+	target_props?: Set<string>,
 ) {
 	const found = new Set<string>()
 	const proofs: Record<string, string> = {}
@@ -49,15 +52,21 @@ export function get_deduced_satisfied_properties(
 
 			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 (implication.source_assumptions) {
+				const is_applicable = is_subset(
+					implication.source_assumptions,
+					source_props ?? new Set(),
+				)
+
+				if (!is_applicable) continue
+			}
+
+			if (implication.target_assumptions) {
+				const is_applicable = is_subset(
+					implication.target_assumptions,
+					target_props ?? new Set(),
+				)
+
 				if (!is_applicable) continue
 			}
 
@@ -101,8 +110,8 @@ export function get_deduced_unsatisfied_properties(
 		stop_when_found?: string
 	},
 	type: StructureType,
-	// used for source and target properties of a functor
-	associated_satisfied_properties?: Record<string, Set<string>>,
+	source_props?: Set<string>,
+	target_props?: Set<string>,
 ) {
 	const found = new Set<string>()
 	const proofs: Record<string, string> = {}
@@ -122,15 +131,19 @@ export function get_deduced_unsatisfied_properties(
 					})
 				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 (implication.source_assumptions) {
+					const is_applicable = is_subset(
+						implication.source_assumptions,
+						source_props ?? new Set(),
+					)
+					if (!is_applicable) continue
+				}
+
+				if (implication.target_assumptions) {
+					const is_applicable = is_subset(
+						implication.target_assumptions,
+						target_props ?? new Set(),
+					)
 					if (!is_applicable) continue
 				}
 
@@ -257,7 +270,8 @@ function deduce_satisfied_properties(
 		implications,
 		{ properties_dict },
 		type,
-		structure.associated_satisfied_properties,
+		structure.source_props,
+		structure.target_props,
 	)
 
 	for (const p of found) satisfied_properties.add(p)
@@ -287,7 +301,8 @@ function deduce_unsatisfied_properties(
 		implications,
 		{ properties_dict },
 		type,
-		structure.associated_satisfied_properties,
+		structure.source_props,
+		structure.target_props,
 	)
 
 	for (const p of found) unsatisfied_properties.add(p)
@@ -398,8 +413,9 @@ export function deduce_properties_for_structures(type: StructureType) {
 
 	delete_deduced_properties(db, type)
 
-	const implications = get_normalized_implications(db, type)
+	const implications = get_normalized_functor_implications(db, type)
 	const structures = get_structures(db, type)
+
 	const properties_dict = get_properties_dict(db, type)
 	const get_assigned_properties = get_property_assignments(db, structures, type)
 

databases/catdat/scripts/redundancies.ts

@@ -1,9 +1,5 @@
 import { get_client } from './utils/helpers'
-import {
-	get_categories,
-	get_normalized_category_implications,
-	type NormalizedCategoryImplication,
-} from './utils/categories'
+import { get_categories } from './utils/categories'
 import {
 	get_deduced_satisfied_properties,
 	get_deduced_unsatisfied_properties,
@@ -12,8 +8,12 @@ import {
 	get_property_assignments_by_deduction,
 	type StructureMeta,
 } from './utils/deduction'
-import { get_functors, get_normalized_functor_implications } from './utils/functors'
+import { get_functors } from './utils/functors'
 import type { StructureType } from './config'
+import {
+	get_normalized_functor_implications,
+	NormalizedImplication,
+} from './utils/implications'
 
 const db = get_client()
 
@@ -36,11 +36,7 @@ function check_redundancies() {
 function check_redundant_property_assignments(type: StructureType) {
 	console.info(`\n--- Check redundant ${type} property assignments ---`)
 
-	// TODO: refactor this when > 2 types of structures are available
-	const implications =
-		type === 'category'
-			? get_normalized_category_implications(db)
-			: get_normalized_functor_implications(db)
+	const implications = get_normalized_functor_implications(db, type)
 
 	const structures: StructureMeta[] =
 		type === 'category' ? get_categories(db) : get_functors(db)
@@ -60,7 +56,8 @@ function check_redundant_property_assignments(type: StructureType) {
 			assignments[structure.id].satisfied.non_deduced,
 			implications,
 			ignore_dict[structure.id],
-			structure.associated_satisfied_properties,
+			structure.source_props,
+			structure.target_props,
 		)
 
 		if (redundant_satisfied_property) {
@@ -81,7 +78,8 @@ function check_redundant_property_assignments(type: StructureType) {
 			assignments[structure.id].unsatisfied.non_deduced,
 			implications,
 			ignore_dict[structure.id],
-			structure.associated_satisfied_properties,
+			structure.source_props,
+			structure.target_props,
 		)
 
 		if (redundant_unsatisfied_property) {
@@ -112,9 +110,10 @@ function check_redundant_property_assignments(type: StructureType) {
  */
 function get_redundant_satisfied_property(
 	satisfied_properties: Set<string>,
-	implications: NormalizedCategoryImplication[],
+	implications: NormalizedImplication[],
 	ignored: Set<string> = new Set(),
-	associated_satisfied_properties?: Record<string, Set<string>>,
+	source_props?: Set<string>,
+	target_props?: Set<string>,
 ) {
 	for (const p of [...satisfied_properties]) {
 		if (ignored.has(p)) continue
@@ -124,7 +123,8 @@ function get_redundant_satisfied_property(
 			implications,
 			{ stop_when_found: p },
 			'category',
-			associated_satisfied_properties,
+			source_props,
+			target_props,
 		)
 		if (deduced_satisfied_properties.has(p)) return p
 		satisfied_properties.add(p)
@@ -141,9 +141,10 @@ function get_redundant_satisfied_property(
 function get_redundant_unsatisfied_property(
 	satisfied_properties: Set<string>,
 	unsatisfied_properties: Set<string>,
-	implications: NormalizedCategoryImplication[],
+	implications: NormalizedImplication[],
 	ignored: Set<string> = new Set(),
-	associated_satisfied_properties?: Record<string, Set<string>>,
+	source_props?: Set<string>,
+	target_props?: Set<string>,
 ) {
 	for (const p of [...unsatisfied_properties]) {
 		if (ignored.has(p)) continue
@@ -154,7 +155,8 @@ function get_redundant_unsatisfied_property(
 			implications,
 			{ stop_when_found: p },
 			'category',
-			associated_satisfied_properties,
+			source_props,
+			target_props,
 		)
 		if (deduced_unsatisfied_properties.has(p)) return p
 		unsatisfied_properties.add(p)

databases/catdat/scripts/utils/categories.ts

@@ -1,97 +1,14 @@
 import { type Database } from 'better-sqlite3'
-import { parse_json_set } from './helpers'
-
-type CategoryMeta = {
-	id: string
-	name: string
-	dual: string | null
-}
-
-export type NormalizedCategoryImplication = {
-	id: string
-	assumptions: Set<string>
-	conclusion: string
-}
+import type { StructureMeta } from './deduction'
 
 /**
  * Returns the list of categories saved in the database.
  */
-export function get_categories(db: Database) {
+export function get_categories(db: Database): StructureMeta[] {
 	return db
-		.prepare<never[], CategoryMeta>(
+		.prepare<never[], StructureMeta>(
 			`SELECT id, name, dual_category_id as dual
             FROM categories_view ORDER BY lower(name)`,
 		)
 		.all()
 }
-
-/**
- * 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_category_implications(
-	db: Database,
-): NormalizedCategoryImplication[] {
-	// TODO: This needs to be unified with the functor case.
-
-	const all_implications_db = db
-		.prepare<
-			never[],
-			{
-				id: string
-				is_equivalence: 0 | 1
-				assumptions: string
-				conclusions: string
-			}
-		>(
-			`SELECT
-				i.id,
-				i.is_equivalence,
-				(
-					SELECT json_group_array(property_id)
-					FROM implication_properties ip
-					WHERE ip.implication_id  = i.id
-					AND ip.structure = 'self'
-					AND ip.kind = 'assumption'
-				) as assumptions,
-				(
-					SELECT json_group_array(property_id)
-					FROM implication_properties ip
-					WHERE ip.implication_id  = i.id
-					AND ip.structure = 'self'
-					AND ip.kind = 'conclusion'
-				) as conclusions
-			FROM implications i
-			WHERE i.type = 'category'
-			GROUP BY i.id`,
-		)
-		.all()
-
-	const implications: NormalizedCategoryImplication[] = []
-
-	for (const impl of all_implications_db) {
-		const assumptions = parse_json_set<string>(impl.assumptions)
-		const conclusions = parse_json_set<string>(impl.conclusions)
-
-		for (const conclusion of conclusions) {
-			implications.push({ id: impl.id, assumptions, conclusion })
-		}
-
-		if (impl.is_equivalence) {
-			for (const assumption of assumptions) {
-				implications.push({
-					id: impl.id,
-					assumptions: conclusions,
-					conclusion: assumption,
-				})
-			}
-		}
-	}
-
-	return implications
-}

databases/catdat/scripts/utils/deduction.ts

@@ -1,6 +1,6 @@
 import { type Database } from 'better-sqlite3'
-import { get_categories, get_normalized_category_implications } from './categories'
-import { get_functors, get_normalized_functor_implications } from './functors'
+import { get_categories } from './categories'
+import { get_functors } from './functors'
 import { StructureType } from '../config'
 
 /**
@@ -10,16 +10,8 @@ export type StructureMeta = {
 	id: string
 	name: string
 	dual?: string | null
-	// used for source and target properties of a functor
-	associated_satisfied_properties?: Record<string, Set<string>>
-}
-
-export type NormalizedImplication = {
-	id: string
-	assumptions: Set<string>
-	conclusion: string
-	// used for source and target assumptions of a functor in an implication
-	associated_assumptions?: Record<string, Set<string>>
+	source_props?: Set<string>
+	target_props?: Set<string>
 }
 
 export type PropertyMeta = {
@@ -38,18 +30,6 @@ export function get_structures(db: Database, type: StructureType): StructureMeta
 	throw new Error('Unsupported type')
 }
 
-/**
- * Returns the list of normalized implications saved in the database of a given type.
- */
-export function get_normalized_implications(
-	db: Database,
-	type: StructureType,
-): NormalizedImplication[] {
-	if (type === 'category') return get_normalized_category_implications(db)
-	if (type === 'functor') return get_normalized_functor_implications(db)
-	throw new Error('Unsupported type')
-}
-
 /**
  * Returns a dictionary of properties saved in the database.
  */