Skip to content

Conversation

@arnog
Copy link
Member

@arnog arnog commented Feb 1, 2026

No description provided.

claude and others added 8 commits January 31, 2026 21:32
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
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
)

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
Resolved conflicts keeping our bug fixes (#24, #25) and task #19 implementation:
- assume.ts: Keep _setCurrentContextValue for scoped assumptions
- CHANGELOG.md: Include inequality evaluation feature
- DONE.md: Include tasks #19, #24, #25 documentation

https://claude.ai/code/session_01Xx26gPU9ThyiypRqdLcmZQ
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
…#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 arnog merged commit 9878c5e into main Feb 1, 2026
1 check failed
@arnog arnog deleted the claude/complete-task-18-NewVw branch February 1, 2026 03:39
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.

3 participants