feat: add improvements for First-Order Logic parsing, including quantifier scope and automatic predicate inference

Author: arnog

CHANGELOG.md

@@ -68,6 +68,24 @@
 
 ### Improvements
 
+- **([#263](https://github.com/cortex-js/compute-engine/issues/263))
+  First-Order Logic**: Added several improvements for working with First-Order
+  Logic expressions:
+  - **Configurable quantifier scope**: New `quantifierScope` parsing option
+    controls how quantifier scope is determined. Use `"tight"` (default) for
+    standard FOL conventions where quantifiers bind only the immediately
+    following formula, or `"loose"` for scope extending to the end of the
+    expression.
+    ```typescript
+    ce.parse('\\forall x. P(x)', { quantifierScope: 'tight' })  // default
+    ce.parse('\\forall x. P(x)', { quantifierScope: 'loose' })
+    ```
+  - **Automatic predicate inference**: Single uppercase letters followed by
+    parentheses (e.g., `P(x)`, `Q(a,b)`) are now automatically recognized as
+    predicate/function applications without requiring explicit declaration.
+    This enables natural FOL syntax like `\forall x. P(x) \rightarrow Q(x)`
+    to work out of the box.
+
 - **Polynomial Simplification**: The `simplify()` function now automatically
   cancels common polynomial factors in univariate rational expressions. For
   example, `(x² - 1)/(x - 1)` simplifies to `x + 1`, `(x³ - x)/(x² - 1)`

src/api.md

@@ -4943,6 +4943,7 @@ type ParseLatexOptions = NumberFormat & {
   getSymbolType: (symbol) => BoxedType;
   parseUnexpectedToken: (lhs, parser) => Expression | null;
   preserveLatex: boolean;
+  quantifierScope: "tight" | "loose";
 };
 ```
 
@@ -5024,6 +5025,38 @@ commands replaced, for example `\egroup` and `\bgroup`.
 
 **Default:** `false`
 
+#### ParseLatexOptions.quantifierScope
+
+```ts
+quantifierScope: "tight" | "loose";
+```
+
+Controls how quantifier scope is determined when parsing expressions
+like `\forall x. P(x) \rightarrow Q(x)`.
+
+- `"tight"`: The quantifier binds only to the immediately following
+  well-formed formula, stopping at logical connectives (`\rightarrow`,
+  `\implies`, `\land`, `\lor`, etc.). This follows standard First-Order
+  Logic conventions. Use explicit parentheses for wider scope:
+  `\forall x. (P(x) \rightarrow Q(x))`.
+
+- `"loose"`: The quantifier scope extends to the end of the expression
+  or until a lower-precedence operator is encountered.
+
+**Default:** `"tight"`
+
+##### Example
+
+```ts
+// With "tight" (default):
+// \forall x. P(x) \rightarrow Q(x)
+// parses as: (∀x. P(x)) → Q(x)
+
+// With "loose":
+// \forall x. P(x) \rightarrow Q(x)
+// parses as: ∀x. (P(x) → Q(x))
+```
+
 </MemberCard>
 
 ### Parser

src/compute-engine/index.ts

@@ -1946,6 +1946,7 @@ export class ComputeEngine implements IComputeEngine {
       },
       parseUnexpectedToken: (_lhs, _parser) => null,
       preserveLatex: false,
+      quantifierScope: 'tight',
     };
 
     const result = parse(

src/compute-engine/latex-syntax/dictionary/definitions-logic.ts

@@ -356,11 +356,32 @@ function serializeQuantifier(
   };
 }
 
+// Condition function for tight quantifier binding - stops at logical connectives
+function tightBindingCondition(
+  p: Parser,
+  terminator: Readonly<Terminator>
+): boolean {
+  return (
+    p.peek === '\\to' ||
+    p.peek === '\\rightarrow' ||
+    p.peek === '\\implies' ||
+    p.peek === '\\Rightarrow' ||
+    p.peek === '\\iff' ||
+    p.peek === '\\Leftrightarrow' ||
+    p.peek === '\\land' ||
+    p.peek === '\\wedge' ||
+    p.peek === '\\lor' ||
+    p.peek === '\\vee' ||
+    (terminator.condition?.(p) ?? false)
+  );
+}
+
 function parseQuantifier(
   kind: 'NotForAll' | 'NotExists' | 'ForAll' | 'Exists' | 'ExistsUnique'
 ): (parser: Parser, terminator: Readonly<Terminator>) => Expression | null {
   return (parser, terminator) => {
     const index = parser.index;
+    const useTightBinding = parser.options.quantifierScope !== 'loose';
 
     // There are several acceptable forms:
     // - \forall x, x>0
@@ -392,28 +413,13 @@ function parseQuantifier(
         parser.match(':') ||
         parser.match('\\colon')
       ) {
-        // Use tight binding: parse body but stop at logical connectives
-        // and arrows (→, ⇒, ∧, ∨, etc.)
-        // This follows standard FOL convention where quantifier scope
+        // Parse body with optional tight binding (stops at logical connectives)
+        // Tight binding follows standard FOL convention where quantifier scope
         // extends only to the immediately following well-formed formula.
-        // We use a condition function because arrows have higher precedence
-        // than comparisons in this system, but we want to include comparisons
-        // while excluding arrows/implications.
-        const body = parser.parseExpression({
-          ...terminator,
-          condition: (p) =>
-            p.peek === '\\to' ||
-            p.peek === '\\rightarrow' ||
-            p.peek === '\\implies' ||
-            p.peek === '\\Rightarrow' ||
-            p.peek === '\\iff' ||
-            p.peek === '\\Leftrightarrow' ||
-            p.peek === '\\land' ||
-            p.peek === '\\wedge' ||
-            p.peek === '\\lor' ||
-            p.peek === '\\vee' ||
-            (terminator.condition?.(p) ?? false),
-        });
+        const bodyTerminator = useTightBinding
+          ? { ...terminator, condition: (p: Parser) => tightBindingCondition(p, terminator) }
+          : terminator;
+        const body = parser.parseExpression(bodyTerminator);
         return [kind, symbol, missingIfEmpty(body)] as Expression;
       }
       const body = parser.parseEnclosure();
@@ -430,22 +436,11 @@ function parseQuantifier(
     // Either a separator or a parenthesis
     parser.skipSpace();
     if (parser.matchAny([',', '\\mid', ':', '\\colon'])) {
-      // Use tight binding for quantifier body - stop at logic operators
-      const body = parser.parseExpression({
-        ...terminator,
-        condition: (p) =>
-          p.peek === '\\to' ||
-          p.peek === '\\rightarrow' ||
-          p.peek === '\\implies' ||
-          p.peek === '\\Rightarrow' ||
-          p.peek === '\\iff' ||
-          p.peek === '\\Leftrightarrow' ||
-          p.peek === '\\land' ||
-          p.peek === '\\wedge' ||
-          p.peek === '\\lor' ||
-          p.peek === '\\vee' ||
-          (terminator.condition?.(p) ?? false),
-      });
+      // Parse body with optional tight binding
+      const bodyTerminator = useTightBinding
+        ? { ...terminator, condition: (p: Parser) => tightBindingCondition(p, terminator) }
+        : terminator;
+      const body = parser.parseExpression(bodyTerminator);
       return [kind, condition, missingIfEmpty(body)] as Expression;
     }
     if (parser.match('(')) {

src/compute-engine/latex-syntax/parse.ts

@@ -1496,8 +1496,13 @@ export class _Parser implements Parser {
       this.index = start;
       fn = parseSymbol(this);
       if (!this.isFunctionOperator(fn)) {
-        this.index = start;
-        return null;
+        // Check if this looks like a predicate: single uppercase letter
+        // followed by parentheses (e.g., P(x), Q(a,b))
+        // This enables automatic inference of predicates in FOL contexts
+        if (!this.looksLikePredicate(fn)) {
+          this.index = start;
+          return null;
+        }
       }
     }
 
@@ -2096,6 +2101,25 @@ export class _Parser implements Parser {
     return false;
   }
 
+  /**
+   * Check if a symbol looks like a predicate in First-Order Logic.
+   * A predicate is typically a single uppercase letter (P, Q, R, etc.)
+   * followed by parentheses containing arguments.
+   *
+   * This enables automatic inference of predicates without explicit declaration,
+   * so `\forall x. P(x)` works without having to declare `P` as a function.
+   */
+  private looksLikePredicate(id: MathJsonSymbol | null): boolean {
+    if (id === null || typeof id !== 'string') return false;
+
+    // Must be a single uppercase letter
+    if (!/^[A-Z]$/.test(id)) return false;
+
+    // Must be followed by an opening parenthesis or \left(
+    this.skipSpace();
+    return this.peek === '(' || this.peek === '\\left';
+  }
+
   /** Return all defs of the specified kind.
    * The defs at the end of the dictionary have priority, since they may
    * override previous definitions. (For example, there is a core definition

src/compute-engine/latex-syntax/types.ts

@@ -770,6 +770,32 @@ export type ParseLatexOptions = NumberFormat & {
    * **Default:** `false`
    */
   preserveLatex: boolean;
+
+  /**
+   * Controls how quantifier scope is determined when parsing expressions
+   * like `\forall x. P(x) \rightarrow Q(x)`.
+   *
+   * - `"tight"`: The quantifier binds only to the immediately following
+   *   well-formed formula, stopping at logical connectives (`\rightarrow`,
+   *   `\implies`, `\land`, `\lor`, etc.). This follows standard First-Order
+   *   Logic conventions. Use explicit parentheses for wider scope:
+   *   `\forall x. (P(x) \rightarrow Q(x))`.
+   *
+   * - `"loose"`: The quantifier scope extends to the end of the expression
+   *   or until a lower-precedence operator is encountered.
+   *
+   * **Default:** `"tight"`
+   *
+   * @example
+   * // With "tight" (default):
+   * // \forall x. P(x) \rightarrow Q(x)
+   * // parses as: (∀x. P(x)) → Q(x)
+   *
+   * // With "loose":
+   * // \forall x. P(x) \rightarrow Q(x)
+   * // parses as: ∀x. (P(x) → Q(x))
+   */
+  quantifierScope: 'tight' | 'loose';
 };
 
 /**

test/compute-engine/arithmetic.test.ts

@@ -1009,6 +1009,47 @@ describe('SUM', () => {
       ce.parse('\\sum_{n=1}^{4}(3n + 5)').evaluate().toString()
     ).toMatchInlineSnapshot(`50`);
   });
+
+  // Alternating weighted binomial: Sum((-1)^k * k * C(n,k)) = 0 for n >= 2
+  it('should simplify alternating weighted binomial sum to 0', () => {
+    expect(
+      ce.box(['Sum', ['Multiply', ['Power', -1, 'k'], 'k', ['Binomial', 'b', 'k']], ['Tuple', 'k', 0, 'b']]).simplify().toString()
+    ).toMatchInlineSnapshot(`0`);
+  });
+
+  it('should evaluate alternating weighted binomial sum', () => {
+    expect(
+      ce.box(['Sum', ['Multiply', ['Power', -1, 'k'], 'k', ['Binomial', 4, 'k']], ['Tuple', 'k', 0, 4]]).evaluate()?.toString()
+    ).toMatchInlineSnapshot(`0`);
+  });
+
+  // Sum of binomial squares: Sum(C(n,k)^2) = C(2n, n)
+  it('should simplify sum of binomial squares', () => {
+    expect(
+      ce.box(['Sum', ['Power', ['Binomial', 'b', 'k'], 2], ['Tuple', 'k', 0, 'b']]).simplify().toString()
+    ).toMatchInlineSnapshot(`Binomial(2b, b)`);
+  });
+
+  it('should evaluate sum of binomial squares', () => {
+    // C(8,4) = 70
+    expect(
+      ce.box(['Sum', ['Power', ['Binomial', 4, 'k'], 2], ['Tuple', 'k', 0, 4]]).evaluate()?.toString()
+    ).toMatchInlineSnapshot(`70`);
+  });
+
+  // Sum of k*(k+1): n(n+1)(n+2)/3
+  it('should simplify sum of k*(k+1)', () => {
+    expect(
+      ce.box(['Sum', ['Multiply', 'k', ['Add', 'k', 1]], ['Tuple', 'k', 1, 'b']]).simplify().toString()
+    ).toMatchInlineSnapshot(`1/3 * b^3 + b^2 + 2/3 * b`);
+  });
+
+  it('should evaluate sum of k*(k+1)', () => {
+    // 4*5*6/3 = 40
+    expect(
+      ce.box(['Sum', ['Multiply', 'k', ['Add', 'k', 1]], ['Tuple', 'k', 1, 4]]).evaluate()?.toString()
+    ).toMatchInlineSnapshot(`40`);
+  });
 });
 
 describe('PRODUCT', () => {
@@ -1155,6 +1196,34 @@ describe('PRODUCT', () => {
       ce.parse('\\prod_{n=5}^{5}(2n)').simplify().toString()
     ).toMatchInlineSnapshot(`10`);
   });
+
+  // Telescoping product: Product((k+1)/k) = b+1
+  it('should simplify telescoping product (k+1)/k', () => {
+    expect(
+      ce.parse('\\prod_{k=1}^{b}\\frac{k+1}{k}').simplify().toString()
+    ).toMatchInlineSnapshot(`b + 1`);
+  });
+
+  it('should evaluate telescoping product (k+1)/k', () => {
+    // (2/1)*(3/2)*(4/3)*(5/4) = 5
+    expect(
+      ce.parse('\\prod_{k=1}^{4}\\frac{k+1}{k}').evaluate().toString()
+    ).toMatchInlineSnapshot(`5`);
+  });
+
+  // Wallis-like product: Product(1 - 1/k^2) = (b+1)/(2b) = 1/(2b) + 1/2
+  it('should simplify Wallis-like product 1 - 1/k^2', () => {
+    expect(
+      ce.parse('\\prod_{k=2}^{b}(1 - \\frac{1}{k^2})').simplify().toString()
+    ).toMatchInlineSnapshot(`1 / (2b) + 1/2`);
+  });
+
+  it('should evaluate Wallis-like product 1 - 1/k^2', () => {
+    // (1-1/4)*(1-1/9)*(1-1/16) = (3/4)*(8/9)*(15/16) = 5/8 = 0.625
+    expect(
+      ce.parse('\\prod_{k=2}^{4}(1 - \\frac{1}{k^2})').evaluate().toString()
+    ).toMatchInlineSnapshot(`0.625`);
+  });
 });
 
 describe('GCD/LCM', () => {

test/compute-engine/latex-syntax/logic.test.ts

@@ -601,6 +601,8 @@ describe('Logic', () => {
     `);
   });
 
+  // Note: P(x) is automatically inferred as function application (predicate)
+  // because P is a single uppercase letter followed by parentheses
   it('should parse ForAll with set membership', () => {
     expect(ce.parse('\\forall x \\in S, P(x)').json).toMatchInlineSnapshot(`
       [
@@ -611,12 +613,8 @@ describe('Logic', () => {
           S,
         ],
         [
-          InvisibleOperator,
           P,
-          [
-            Delimiter,
-            x,
-          ],
+          x,
         ],
       ]
     `);