Display contradiction proofs on the search results page

src/lib/server/consistency.ts

@@ -10,62 +10,100 @@ type NormalizedCategoryImplication = {
 	conclusion: string
 }
 
-export function check_consistency(
+export function get_contradiction(
 	satisfied_properties: Set<string>,
 	unsatisfied_properties: Set<string>,
-): { consistent: boolean } | null {
+): string[] | null {
 	for (const p of satisfied_properties) {
-		if (unsatisfied_properties.has(p)) return { consistent: false }
+		if (unsatisfied_properties.has(p)) return [`${p} ⟹ ${p}`]
 	}
 
 	const implications = get_normalized_category_implications()
-	if (!implications) return null
 
-	return check_consistency_worker(
+	return contradiction_worker(
 		satisfied_properties,
 		unsatisfied_properties,
 		implications,
 	)
 }
 
-function check_consistency_worker(
+function contradiction_worker(
 	satisfied_properties: Set<string>,
 	unsatisfied_properties: Set<string>,
 	implications: NormalizedCategoryImplication[],
-): { consistent: boolean } {
+): string[] | null {
 	for (const p of satisfied_properties) {
-		if (unsatisfied_properties.has(p)) return { consistent: false }
+		if (unsatisfied_properties.has(p)) return [`${p} ⟹ ${p}`]
 	}
 
+	const deduction_dict: Record<string, NormalizedCategoryImplication> = {}
 	const deduced_satisfied_properties = new Set(satisfied_properties)
 
-	function get_next_implication() {
+	// bfs to find contradiction
+
+	let contradictory_property: string | null = null
+
+	while (!contradictory_property) {
+		const new_properties = new Set<string>()
+
 		for (const implication of implications) {
 			const is_valid =
 				is_subset(implication.assumptions, deduced_satisfied_properties) &&
-				!deduced_satisfied_properties.has(implication.conclusion)
-			if (is_valid) return implication
+				!deduced_satisfied_properties.has(implication.conclusion) &&
+				!new_properties.has(implication.conclusion)
+			if (!is_valid) continue
+
+			new_properties.add(implication.conclusion)
+			deduction_dict[implication.conclusion] = implication
+
+			if (unsatisfied_properties.has(implication.conclusion)) {
+				contradictory_property = implication.conclusion
+				break
+			}
 		}
-		return null
+
+		if (!new_properties.size) break
+
+		for (const p of new_properties) deduced_satisfied_properties.add(p)
 	}
 
-	while (true) {
-		const implication = get_next_implication()
-		if (!implication) break
+	if (!contradictory_property) return null
 
-		if (unsatisfied_properties.has(implication.conclusion)) {
-			return { consistent: false }
-		}
+	return build_shortest_proof(
+		satisfied_properties,
+		deduction_dict,
+		contradictory_property,
+	)
+}
+
+function build_shortest_proof(
+	satisfied_properties: Set<string>,
+	deduction_dict: Record<string, NormalizedCategoryImplication>,
+	target_property: string,
+) {
+	const proof: string[] = []
+
+	const visited_properties = new Set<string>()
+
+	function derive(property: string) {
+		if (visited_properties.has(property)) return
+		if (satisfied_properties.has(property)) return
+		visited_properties.add(property)
 
-		deduced_satisfied_properties.add(implication.conclusion)
+		const implication = deduction_dict[property]
+		if (!implication) throw new Error(`Missing deduction for property: ${property}`)
+
+		for (const p of implication.assumptions) derive(p)
+
+		proof.push(stringify_implication(implication))
 	}
 
-	return { consistent: true }
+	derive(target_property)
+
+	return proof
 }
 
-export function get_normalized_category_implications():
-	| NormalizedCategoryImplication[]
-	| null {
+function get_normalized_category_implications() {
 	const { rows, err } = query<{
 		id: string
 		assumptions: string
@@ -75,7 +113,7 @@ export function get_normalized_category_implications():
 		sql`SELECT id, assumptions, conclusions, is_equivalence FROM category_implications_view`,
 	)
 
-	if (err) return null
+	if (err) throw err
 
 	const implications: NormalizedCategoryImplication[] = []
 
@@ -105,16 +143,19 @@ export function get_normalized_category_implications():
 	return implications
 }
 
+function stringify_implication(implication: NormalizedCategoryImplication) {
+	return `${[...implication.assumptions].join(' ∧ ')} ⟹ ${implication.conclusion}`
+}
+
 export function get_missing_combinations() {
 	const implications = get_normalized_category_implications()
-	if (!implications) return null
 
 	const { rows: properties, err } = query<{
 		id: string
 		dual_property_id: string | null
 	}>(sql`SELECT id, dual_property_id FROM category_properties ORDER BY lower(id)`)
 
-	if (err) return null
+	if (err) throw err
 
 	const { rows: existing, err: err_existing } = query<{
 		p: string
@@ -127,7 +168,7 @@ export function get_missing_combinations() {
 		WHERE cp.is_satisfied = TRUE AND cnp.is_satisfied = FALSE
 	`)
 
-	if (err_existing) return null
+	if (err_existing) throw err_existing
 
 	const witnessed_pairs = new Set(existing.map(({ p, q }) => `${p}|${q}`))
 
@@ -147,13 +188,13 @@ export function get_missing_combinations() {
 				continue
 			}
 
-			const { consistent } = check_consistency_worker(
+			const contradiction = contradiction_worker(
 				new Set([p.id]),
 				new Set([q.id]),
 				implications,
 			)
 
-			if (consistent) missing_pairs.push([p.id, q.id])
+			if (!contradiction) missing_pairs.push([p.id, q.id])
 		}
 	}
 

src/lib/server/search.ts

@@ -4,7 +4,7 @@ import { query } from '$lib/server/db.catdat'
 import { error } from '@sveltejs/kit'
 import sql from 'sql-template-tag'
 import { SEARCH_SEPARATOR } from '$lib/commons/search.config'
-import { check_consistency } from '$lib/server/consistency'
+import { get_contradiction } from '$lib/server/consistency'
 
 type NamedObject = {
 	id: string
@@ -71,29 +71,31 @@ export function search_handler(event: RequestEvent, type: 'category' | 'functor'
 
 	// TODO: implement this for functors as well
 	if (type === 'category') {
-		const check = check_consistency(
-			new Set(satisfied_properties),
-			new Set(unsatisfied_properties),
-		)
-
-		if (!check) error(500, 'Consistency check failed')
-
-		if (!check.consistent) {
-			event.setHeaders({
-				// shared cache for 30min
-				'cache-control': 'public, max-age=0, s-maxage=1800',
-			})
-
-			return {
-				is_consistent: false,
-				all_properties,
-				satisfied_properties,
-				unsatisfied_properties,
-				found_objects: [],
-				dual_satisfied_properties,
-				dual_unsatisfied_properties,
-				dual_search_available,
+		try {
+			const contradiction = get_contradiction(
+				new Set(satisfied_properties),
+				new Set(unsatisfied_properties),
+			)
+
+			if (contradiction) {
+				event.setHeaders({
+					// shared cache for 30min
+					'cache-control': 'public, max-age=0, s-maxage=1800',
+				})
+
+				return {
+					contradiction,
+					all_properties,
+					satisfied_properties,
+					unsatisfied_properties,
+					found_objects: [],
+					dual_satisfied_properties,
+					dual_unsatisfied_properties,
+					dual_search_available,
+				}
 			}
+		} catch (err) {
+			error(500, 'Consistency check failed')
 		}
 	}
 
@@ -123,7 +125,7 @@ export function search_handler(event: RequestEvent, type: 'category' | 'functor'
 	})
 
 	return {
-		is_consistent: true,
+		contradiction: null,
 		all_properties,
 		satisfied_properties,
 		unsatisfied_properties,

src/routes/category-search/results/+page.svelte

@@ -63,7 +63,7 @@
 	</div>
 {/if}
 
-{#if data.is_consistent}
+{#if !data.contradiction}
 	<p class="hint">
 		{pluralize(data.found_objects.length, {
 			one: 'Found {count} category',
@@ -73,8 +73,14 @@
 	<CategoryList categories={data.found_objects ?? []} />
 {:else}
 	<p class="hint">
-		<Fa icon={faWarning} /> No categories found because the requirements are inconsistent.
+		<Fa icon={faWarning} /> No categories found because the requirements are inconsistent:
 	</p>
+
+	<ol class="hint">
+		{#each data.contradiction as segment}
+			<li>{segment}</li>
+		{/each}
+	</ol>
 {/if}
 
 <menu>

src/routes/missing/+page.server.ts

@@ -87,18 +87,18 @@ export const load = async () => {
 		0,
 	)
 
-	const missing_combinations = get_missing_combinations()
+	try {
+		const missing_combinations = get_missing_combinations()
 
-	if (!missing_combinations) {
+		return {
+			categories_with_unknown_properties,
+			total_unknown_pairs,
+			categories_with_missing_morphisms,
+			undistinguishable_category_pairs,
+			functors_with_unknown_properties,
+			missing_combinations,
+		}
+	} catch (err) {
 		error(500, 'Failed to load missing combinations')
 	}
-
-	return {
-		categories_with_unknown_properties,
-		total_unknown_pairs,
-		categories_with_missing_morphisms,
-		undistinguishable_category_pairs,
-		functors_with_unknown_properties,
-		missing_combinations,
-	}
 }