diff --git a/src/core/prover.ts b/src/core/prover.ts index c32c696..fbf21b8 100644 --- a/src/core/prover.ts +++ b/src/core/prover.ts @@ -613,6 +613,108 @@ function collapseInfinity(node: ASTNode): ASTNode { return node } +/** + * Recursively expand Male expressions using axiom A5: ♂x = (♂x -> x) + * + * This function repeatedly applies A5 to expand expressions like: + * - ♂v + * - (♂v -> v) -> v + * - ((♂v -> v) -> v) -> v + * - etc. + * + * All of these can be unified with ♂v because: + * 1. ♂v = (♂v -> v) by A5 + * 2. Substituting ♂v: ♂v = ((♂v -> v) -> v) + * 3. Therefore: ♂v = (((♂v -> v) -> v) -> v) + * 4. And so on recursively... + */ +function expandMale(node: ASTNode): ASTNode { + // Base case: ♂x expression + if (isMaleExpr(node)) { + return node + } + + // Recursive case: (a -> b) where a can expand to the full ♂x -> x pattern + if (isLinkExpr(node)) { + // Try to collapse this link to ♂x if it matches the pattern (♂x -> x) + // and recursively if it matches ((♂x -> x) -> x), etc. + const collapsedLeft = expandMale(node.left) + + // Check if left is ♂x and right is x (the operand of ♂x) + if (isMaleExpr(collapsedLeft)) { + const x = collapsedLeft.operand + if (astEqual(node.right, x)) { + // This is (♂x -> x), which equals ♂x by A5 + return collapsedLeft + } + } + + // Recursively try to collapse children + const collapsedRight = expandMale(node.right) + if (collapsedLeft !== node.left || collapsedRight !== node.right) { + return { + type: 'Link', + left: collapsedLeft, + right: collapsedRight, + } as LinkExpr + } + } + + // Other node types: return as-is + return node +} + +/** + * Recursively expand Female expressions using axiom A6: x♀ = (x -> x♀) + * + * This function repeatedly applies A6 to expand expressions like: + * - r♀ + * - r -> r♀ + * - r -> (r -> r♀) + * - etc. + * + * All of these can be unified with r♀ because: + * 1. r♀ = (r -> r♀) by A6 + * 2. Substituting r♀: r♀ = (r -> (r -> r♀)) + * 3. Therefore: r♀ = (r -> (r -> (r -> r♀))) + * 4. And so on recursively... + */ +function expandFemale(node: ASTNode): ASTNode { + // Base case: x♀ expression + if (isFemaleExpr(node)) { + return node + } + + // Recursive case: (a -> b) where b can expand to the full x -> x♀ pattern + if (isLinkExpr(node)) { + // Try to collapse this link to x♀ if it matches the pattern (x -> x♀) + // and recursively if it matches (x -> (x -> x♀)), etc. + const collapsedRight = expandFemale(node.right) + + // Check if right is x♀ and left is x (the operand of x♀) + if (isFemaleExpr(collapsedRight)) { + const x = collapsedRight.operand + if (astEqual(node.left, x)) { + // This is (x -> x♀), which equals x♀ by A6 + return collapsedRight + } + } + + // Recursively try to collapse children + const collapsedLeft = expandFemale(node.left) + if (collapsedLeft !== node.left || collapsedRight !== node.right) { + return { + type: 'Link', + left: collapsedLeft, + right: collapsedRight, + } as LinkExpr + } + } + + // Other node types: return as-is + return node +} + /** * Generate hints for failed equality verification */ @@ -879,6 +981,84 @@ export function checkEquality(left: ASTNode, right: ASTNode, state: ProverState) } } + // Try recursive expansion for Male expressions using axiom A5: ♂x = (♂x -> x) + const expandedMaleLeft = expandMale(expLeft) + const expandedMaleRight = expandMale(expRight) + const maleLeftWasExpanded = !astEqual(expLeft, expandedMaleLeft) + const maleRightWasExpanded = !astEqual(expRight, expandedMaleRight) + + if (maleLeftWasExpanded || maleRightWasExpanded) { + // Build detailed explanation of expansion steps + let details = '' + if (maleLeftWasExpanded && maleRightWasExpanded) { + details = `Обе стороны сворачиваются в ♂x:\n ${expLeftStr} → ${toCanonicalString(expandedMaleLeft)}\n ${expRightStr} → ${toCanonicalString(expandedMaleRight)}` + } else if (maleLeftWasExpanded) { + details = `Левая сторона сворачивается в ♂x: ${expLeftStr} → ${toCanonicalString(expandedMaleLeft)}` + } else { + details = `Правая сторона сворачивается в ♂x: ${expRightStr} → ${toCanonicalString(expandedMaleRight)}` + } + + proofSteps.push({ + index: proofSteps.length + 1, + action: 'Рекурсивное свёртывание по А5', + before: `${expLeftStr} = ${expRightStr}`, + after: `${toCanonicalString(expandedMaleLeft)} = ${toCanonicalString(expandedMaleRight)}`, + axiom: AXIOMS.A5, + details, + }) + + // Check equality after expansion + if (astEqual(expandedMaleLeft, expandedMaleRight)) { + appliedAxioms.push(AXIOMS.A5) + return { + success: true, + message: 'Применена аксиома А5: ♂x = (♂x → x) с рекурсивным свёртыванием', + steps: ['♂x : (♂x -> x) recursively applied'], + proofSteps, + appliedAxioms, + } + } + } + + // Try recursive expansion for Female expressions using axiom A6: x♀ = (x -> x♀) + const expandedFemaleLeft = expandFemale(expLeft) + const expandedFemaleRight = expandFemale(expRight) + const femaleLeftWasExpanded = !astEqual(expLeft, expandedFemaleLeft) + const femaleRightWasExpanded = !astEqual(expRight, expandedFemaleRight) + + if (femaleLeftWasExpanded || femaleRightWasExpanded) { + // Build detailed explanation of expansion steps + let details = '' + if (femaleLeftWasExpanded && femaleRightWasExpanded) { + details = `Обе стороны сворачиваются в x♀:\n ${expLeftStr} → ${toCanonicalString(expandedFemaleLeft)}\n ${expRightStr} → ${toCanonicalString(expandedFemaleRight)}` + } else if (femaleLeftWasExpanded) { + details = `Левая сторона сворачивается в x♀: ${expLeftStr} → ${toCanonicalString(expandedFemaleLeft)}` + } else { + details = `Правая сторона сворачивается в x♀: ${expRightStr} → ${toCanonicalString(expandedFemaleRight)}` + } + + proofSteps.push({ + index: proofSteps.length + 1, + action: 'Рекурсивное свёртывание по А6', + before: `${expLeftStr} = ${expRightStr}`, + after: `${toCanonicalString(expandedFemaleLeft)} = ${toCanonicalString(expandedFemaleRight)}`, + axiom: AXIOMS.A6, + details, + }) + + // Check equality after expansion + if (astEqual(expandedFemaleLeft, expandedFemaleRight)) { + appliedAxioms.push(AXIOMS.A6) + return { + success: true, + message: 'Применена аксиома А6: x♀ = (x → x♀) с рекурсивным свёртыванием', + steps: ['x♀ : (x -> x♀) recursively applied'], + proofSteps, + appliedAxioms, + } + } + } + // ∞ = ∞ -> ∞ (with recursive collapse support) // Try to collapse both sides using axiom A4: ∞ = (∞ -> ∞) const collapsedLeft = collapseInfinity(expLeft) diff --git a/tests/unit/prover.test.ts b/tests/unit/prover.test.ts index c888846..6090918 100644 --- a/tests/unit/prover.test.ts +++ b/tests/unit/prover.test.ts @@ -434,4 +434,94 @@ describe('Prover', () => { expect(result.appliedAxioms!.some(a => a.id === 'A4')).toBe(true) }) }) + + describe('Male expansion (issue #53)', () => { + it('should verify ♂v = ♂v -> v -> v -> v (left-associative)', () => { + const eq = normalize(parseExpr('♂v = ♂v -> v -> v -> v')) + const result = verify(eq, state()) + expect(result.success).toBe(true) + expect(result.appliedAxioms!.some(a => a.id === 'A5')).toBe(true) + }) + + it('should verify ♂v = (♂v -> v) -> v', () => { + const eq = normalize(parseExpr('♂v = (♂v -> v) -> v')) + const result = verify(eq, state()) + expect(result.success).toBe(true) + expect(result.appliedAxioms!.some(a => a.id === 'A5')).toBe(true) + }) + + it('should verify ♂v = ((♂v -> v) -> v) -> v', () => { + const eq = normalize(parseExpr('♂v = ((♂v -> v) -> v) -> v')) + const result = verify(eq, state()) + expect(result.success).toBe(true) + expect(result.appliedAxioms!.some(a => a.id === 'A5')).toBe(true) + }) + + it('should verify (♂v -> v) -> v = ♂v (reverse direction)', () => { + const eq = normalize(parseExpr('(♂v -> v) -> v = ♂v')) + const result = verify(eq, state()) + expect(result.success).toBe(true) + expect(result.appliedAxioms!.some(a => a.id === 'A5')).toBe(true) + }) + + it('should verify ((♂v -> v) -> v) -> v = ♂v (deep nesting)', () => { + const eq = normalize(parseExpr('((♂v -> v) -> v) -> v = ♂v')) + const result = verify(eq, state()) + expect(result.success).toBe(true) + expect(result.appliedAxioms!.some(a => a.id === 'A5')).toBe(true) + }) + + it('should verify ♂a = ♂a -> a -> a -> a (3-level nesting)', () => { + const eq = normalize(parseExpr('♂a = ♂a -> a -> a -> a')) + const result = verify(eq, state()) + expect(result.success).toBe(true) + expect(result.appliedAxioms!.some(a => a.id === 'A5')).toBe(true) + }) + + it('should still respect the original ♂x = ♂x -> x case', () => { + // This is a regression test to ensure the simple case still works + const eq = normalize(parseExpr('♂a = ♂a -> a')) + const result = verify(eq, state()) + expect(result.success).toBe(true) + expect(result.appliedAxioms!.some(a => a.id === 'A5')).toBe(true) + }) + }) + + describe('Female expansion (issue #53)', () => { + it('should verify r♀ = r -> (r -> r♀)', () => { + const eq = normalize(parseExpr('r♀ = r -> (r -> r♀)')) + const result = verify(eq, state()) + expect(result.success).toBe(true) + expect(result.appliedAxioms!.some(a => a.id === 'A6')).toBe(true) + }) + + it('should verify r♀ = r -> (r -> (r -> r♀))', () => { + const eq = normalize(parseExpr('r♀ = r -> (r -> (r -> r♀))')) + const result = verify(eq, state()) + expect(result.success).toBe(true) + expect(result.appliedAxioms!.some(a => a.id === 'A6')).toBe(true) + }) + + it('should verify r -> (r -> r♀) = r♀ (reverse direction)', () => { + const eq = normalize(parseExpr('r -> (r -> r♀) = r♀')) + const result = verify(eq, state()) + expect(result.success).toBe(true) + expect(result.appliedAxioms!.some(a => a.id === 'A6')).toBe(true) + }) + + it('should verify r -> (r -> (r -> r♀)) = r♀ (deep nesting)', () => { + const eq = normalize(parseExpr('r -> (r -> (r -> r♀)) = r♀')) + const result = verify(eq, state()) + expect(result.success).toBe(true) + expect(result.appliedAxioms!.some(a => a.id === 'A6')).toBe(true) + }) + + it('should still respect the original x♀ = x -> x♀ case', () => { + // This is a regression test to ensure the simple case still works + const eq = normalize(parseExpr('r♀ = r -> r♀')) + const result = verify(eq, state()) + expect(result.success).toBe(true) + expect(result.appliedAxioms!.some(a => a.id === 'A6')).toBe(true) + }) + }) })