fix: Implement recursive expansion for axioms A5 and A6

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)

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)
+    })
+  })
 })