Skip to content

Conversation

@levirs565
Copy link

Expression with square not sorted correctly because square does not get degree 2. You can see the difference before and after this PR in table below.

Expresssion Canocical Form Before this PR Canocical Form After this PR Status
x^2+x^3+x x^{3}+x+x^2 x^{3}+x^2+x After this PR expression sorted correctly
x^2+x^3+\sin(x) x^{3}+x^2+\sin(x) x^{3}+x^2+\sin(x) Sorted correctly.
\sin(x)+x^2+x^3 x^{3}+\sin(x)+x^2 x^{3}+x^2+\sin(x) This expression's cannocial form must equal with above expression's canonical form

Some test's expected result have been changed. You can see changed test in this table.

Expresssion Canocical Form Before this PR Canocical Form After this PR
x^2y^3+x^3y^2+xy^4+x^4y+x^2y^2 x^{4}y+xy^{4}+x^{3}y^2+x^2y^{3}+x^2y^2 x^{4}y+x^{3}y^2+x^2y^{3}+xy^{4}+x^2y^2
(b^3b^2)+(a^3a^2)+(b^6)+(a^5b)+(a^5) a^{5}b+b^{6}+a^{5}+a^2a^{3}+b^2b^{3} a^{5}b+b^{6}+a^2a^{3}+a^{5}+b^2b^{3}

Why I change the test's expected result?. Canocial form of those expression are inconsistent with other expressions that does not have square. You can see this table:

Expresssion Canocical Form Before this PR Canocical Form After this PR Status
x^2y^3+x^3y^2+xy^4+x^4y+x^2y^2 x^{4}y+xy^{4}+x^{3}y^2+x^2y^{3}+x^2y^2 x^{4}y+x^{3}y^2+x^2y^{3}+xy^{4}+x^2y^2 Different
(b^3b^2)+(a^3a^2)+(b^6)+(a^5b)+(a^5) a^{5}b+b^{6}+a^{5}+a^2a^{3}+b^2b^{3} a^{5}b+b^{6}+a^2a^{3}+a^{5}+b^2b^{3} Different
(b^3b^3)+(a^3a^3)+(b^6)+(a^5b)+(a^5) a^{3}a^{3}+a^{5}b+b^{3}b^{3}+b^{6}+a^{5} a^{3}a^{3}+a^{5}b+b^{3}b^{3}+b^{6}+a^{5}` Equal

Also, this change fix some sorting result when there are square in expression and sin function.

@arnog
Copy link
Member

arnog commented Sep 23, 2021

Thank you for investigating this issue and submitting this PR.
The Compute Engine codebase is undergoing a refactor which unfortunately makes merging this PR directly a little bit tricky. However, I will make sure to incorporate your changes and preserve their effect.
Again, thanks for your submission, it is very much appreciated.

arnog pushed a commit that referenced this pull request Jan 31, 2026
…#20)

ce.assume() now returns 'tautology' for redundant assumptions that are
already implied by existing assumptions, and 'contradiction' for
assumptions that conflict with existing ones.

Examples:
- ce.assume(['Greater', 'x', 0]) when x > 4 exists returns 'tautology'
- ce.assume(['Less', 'x', 0]) when x > 4 exists returns 'contradiction'
- ce.assume(['Equal', 'one', 1]) repeated returns 'tautology'
- ce.assume(['Less', 'one', 0]) when one=1 exists returns 'contradiction'

Implementation:
- Added bounds checking logic in assumeInequality() that extracts the
  symbol from the inequality and checks against existing bounds
- Handles canonical form normalization (Greater(x,k) → Less(k,x))
- Correctly determines "effective" relationship based on operator and
  which operand contains the symbol

https://claude.ai/code/session_01Xx26gPU9ThyiypRqdLcmZQ
arnog added a commit that referenced this pull request Feb 1, 2026
* fix: implement value resolution from equality assumptions (#18)

When ce.assume(['Equal', symbol, value]) is called, the symbol now
correctly evaluates to the assumed value. Previously, the symbol would
remain unevaluated even after the assumption was made.

Changes:
- Fixed assumeEquality to set the symbol value when it already has a
  definition (which happens when accessed via .unknowns)
- Updated BoxedSymbol.N() to check the evaluation context value for
  non-constant symbols, enabling correct comparison evaluation

Examples that now work:
- ce.box('one').evaluate().json → 1 (was: "one")
- ce.box(['Equal', 'one', 1]).evaluate() → True (was: unchanged)
- ce.box(['Equal', 'one', 0]).evaluate() → False

https://claude.ai/code/session_01Xx26gPU9ThyiypRqdLcmZQ

* feat: implement inequality evaluation using assumptions (#19)

When inequality assumptions like `ce.assume(['Greater', 'x', 4])` are made,
comparisons can now use transitive reasoning to determine results.

For example, `x > 4` implies `x > 0`, so `['Greater', 'x', 0]` evaluates
to True instead of remaining symbolic.

Implementation:
- Added `getInequalityBoundsFromAssumptions()` to extract lower/upper bounds
  from normalized assumption forms like `Less(Add(Negate(x), k), 0)`
- Modified `cmp()` in compare.ts to use these bounds when comparing symbols

Examples that now work:
- ce.box(['Greater', 'x', 0]).evaluate() → True (when x > 4 assumed)
- ce.box(['Less', 'x', 0]).evaluate() → False
- ce.box('x').isGreater(0) → true
- ce.box('x').isPositive → true

https://claude.ai/code/session_01Xx26gPU9ThyiypRqdLcmZQ

* fix: forget() and scoped assumptions now properly clear values (#24, #25)

Bug #24: forget() now clears assumed values from evaluation context
- After ce.assume(['Equal', 'x', 5]) and ce.forget('x'), x now correctly
  evaluates to 'x' instead of 5
- Added cleanup loop in forget() to delete values from all context frames

Bug #25: Scoped assumptions clean up on popScope()
- Assumptions made inside pushScope()/popScope() now properly clean up
- Added _setCurrentContextValue() method to store values in current context
- Modified assumeEquality() to use scoped value storage
- Values set by assumptions are automatically removed when scope exits

Files modified:
- src/compute-engine/index.ts - Added _setCurrentContextValue(), forget() cleanup
- src/compute-engine/global-types.ts - Added method signature
- src/compute-engine/assume.ts - Use scoped value storage
- test/compute-engine/bug-fixes.test.ts - Tests for both bugs
- CHANGELOG.md, requirements/TODO.md, requirements/DONE.md - Documentation

https://claude.ai/code/session_01Xx26gPU9ThyiypRqdLcmZQ

* feat: implement type inference from assumptions (#21)

When assumptions are made, symbol types are now correctly inferred:

- Inequality assumptions (>, <, >=, <=) set the symbol's type to 'real'
- Equality assumptions infer the type from the value:
  - Equal to integer → type 'integer'
  - Equal to rational → type 'real'
  - Equal to real → type 'real'
  - Equal to complex → type 'number'

Implementation:
- Added inferTypeFromValue() function to promote specific types
  (e.g., finite_integer → integer)
- Updated assumeEquality() to use inferTypeFromValue when updating types
- Updated assumeInequality() to set type 'real' even for auto-declared symbols

Examples:
  ce.assume(ce.box(['Greater', 'x', 4]));
  ce.box('x').type.toString();  // → 'real' (was: 'unknown')

  ce.assume(ce.box(['Equal', 'one', 1]));
  ce.box('one').type.toString();  // → 'integer' (was: 'unknown')

Files modified:
- src/compute-engine/assume.ts - Added inferTypeFromValue(), updated type inference
- test/compute-engine/assumptions.test.ts - Enabled 6 tests
- CHANGELOG.md, requirements/TODO.md, requirements/DONE.md - Documentation

https://claude.ai/code/session_01Xx26gPU9ThyiypRqdLcmZQ

* feat: implement tautology and contradiction detection for assumptions (#20)

ce.assume() now returns 'tautology' for redundant assumptions that are
already implied by existing assumptions, and 'contradiction' for
assumptions that conflict with existing ones.

Examples:
- ce.assume(['Greater', 'x', 0]) when x > 4 exists returns 'tautology'
- ce.assume(['Less', 'x', 0]) when x > 4 exists returns 'contradiction'
- ce.assume(['Equal', 'one', 1]) repeated returns 'tautology'
- ce.assume(['Less', 'one', 0]) when one=1 exists returns 'contradiction'

Implementation:
- Added bounds checking logic in assumeInequality() that extracts the
  symbol from the inequality and checks against existing bounds
- Handles canonical form normalization (Greater(x,k) → Less(k,x))
- Correctly determines "effective" relationship based on operator and
  which operand contains the symbol

https://claude.ai/code/session_01Xx26gPU9ThyiypRqdLcmZQ

---------

Co-authored-by: Claude <noreply@anthropic.com>
arnog added a commit that referenced this pull request Feb 1, 2026
* fix: implement value resolution from equality assumptions (#18)

When ce.assume(['Equal', symbol, value]) is called, the symbol now
correctly evaluates to the assumed value. Previously, the symbol would
remain unevaluated even after the assumption was made.

Changes:
- Fixed assumeEquality to set the symbol value when it already has a
  definition (which happens when accessed via .unknowns)
- Updated BoxedSymbol.N() to check the evaluation context value for
  non-constant symbols, enabling correct comparison evaluation

Examples that now work:
- ce.box('one').evaluate().json → 1 (was: "one")
- ce.box(['Equal', 'one', 1]).evaluate() → True (was: unchanged)
- ce.box(['Equal', 'one', 0]).evaluate() → False

https://claude.ai/code/session_01Xx26gPU9ThyiypRqdLcmZQ

* feat: implement inequality evaluation using assumptions (#19)

When inequality assumptions like `ce.assume(['Greater', 'x', 4])` are made,
comparisons can now use transitive reasoning to determine results.

For example, `x > 4` implies `x > 0`, so `['Greater', 'x', 0]` evaluates
to True instead of remaining symbolic.

Implementation:
- Added `getInequalityBoundsFromAssumptions()` to extract lower/upper bounds
  from normalized assumption forms like `Less(Add(Negate(x), k), 0)`
- Modified `cmp()` in compare.ts to use these bounds when comparing symbols

Examples that now work:
- ce.box(['Greater', 'x', 0]).evaluate() → True (when x > 4 assumed)
- ce.box(['Less', 'x', 0]).evaluate() → False
- ce.box('x').isGreater(0) → true
- ce.box('x').isPositive → true

https://claude.ai/code/session_01Xx26gPU9ThyiypRqdLcmZQ

* fix: forget() and scoped assumptions now properly clear values (#24, #25)

Bug #24: forget() now clears assumed values from evaluation context
- After ce.assume(['Equal', 'x', 5]) and ce.forget('x'), x now correctly
  evaluates to 'x' instead of 5
- Added cleanup loop in forget() to delete values from all context frames

Bug #25: Scoped assumptions clean up on popScope()
- Assumptions made inside pushScope()/popScope() now properly clean up
- Added _setCurrentContextValue() method to store values in current context
- Modified assumeEquality() to use scoped value storage
- Values set by assumptions are automatically removed when scope exits

Files modified:
- src/compute-engine/index.ts - Added _setCurrentContextValue(), forget() cleanup
- src/compute-engine/global-types.ts - Added method signature
- src/compute-engine/assume.ts - Use scoped value storage
- test/compute-engine/bug-fixes.test.ts - Tests for both bugs
- CHANGELOG.md, requirements/TODO.md, requirements/DONE.md - Documentation

https://claude.ai/code/session_01Xx26gPU9ThyiypRqdLcmZQ

* feat: implement type inference from assumptions (#21)

When assumptions are made, symbol types are now correctly inferred:

- Inequality assumptions (>, <, >=, <=) set the symbol's type to 'real'
- Equality assumptions infer the type from the value:
  - Equal to integer → type 'integer'
  - Equal to rational → type 'real'
  - Equal to real → type 'real'
  - Equal to complex → type 'number'

Implementation:
- Added inferTypeFromValue() function to promote specific types
  (e.g., finite_integer → integer)
- Updated assumeEquality() to use inferTypeFromValue when updating types
- Updated assumeInequality() to set type 'real' even for auto-declared symbols

Examples:
  ce.assume(ce.box(['Greater', 'x', 4]));
  ce.box('x').type.toString();  // → 'real' (was: 'unknown')

  ce.assume(ce.box(['Equal', 'one', 1]));
  ce.box('one').type.toString();  // → 'integer' (was: 'unknown')

Files modified:
- src/compute-engine/assume.ts - Added inferTypeFromValue(), updated type inference
- test/compute-engine/assumptions.test.ts - Enabled 6 tests
- CHANGELOG.md, requirements/TODO.md, requirements/DONE.md - Documentation

https://claude.ai/code/session_01Xx26gPU9ThyiypRqdLcmZQ

* feat: implement tautology and contradiction detection for assumptions (#20)

ce.assume() now returns 'tautology' for redundant assumptions that are
already implied by existing assumptions, and 'contradiction' for
assumptions that conflict with existing ones.

Examples:
- ce.assume(['Greater', 'x', 0]) when x > 4 exists returns 'tautology'
- ce.assume(['Less', 'x', 0]) when x > 4 exists returns 'contradiction'
- ce.assume(['Equal', 'one', 1]) repeated returns 'tautology'
- ce.assume(['Less', 'one', 0]) when one=1 exists returns 'contradiction'

Implementation:
- Added bounds checking logic in assumeInequality() that extracts the
  symbol from the inequality and checks against existing bounds
- Handles canonical form normalization (Greater(x,k) → Less(k,x))
- Correctly determines "effective" relationship based on operator and
  which operand contains the symbol

https://claude.ai/code/session_01Xx26gPU9ThyiypRqdLcmZQ

---------

Co-authored-by: Claude <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Development

Successfully merging this pull request may close these issues.

2 participants