Skip to content

Commit

Permalink
chore(lattice): Refactor interval lattice and numbers
Browse files Browse the repository at this point in the history
  • Loading branch information
@jubnzv
jubnzv committed Nov 4, 2024
1 parent 618c0e4 commit 5bc75a6
Show file tree
Hide file tree
Showing 2 changed files with 231 additions and 228 deletions.
253 changes: 34 additions & 219 deletions src/internals/lattice/interval.ts
View file
Original file line number Diff line number Diff line change
@@ -1,45 +1,25 @@
import { ExecutionException, InternalException } from "../exceptions";
import { Num, mInf, pInf, intNum, IntNum } from "./num";
import { Num, NumImpl } from "./num";

export type Interval = [Num, Num];
export type Interval = [NumImpl, NumImpl];

/**
* Infinite-length lattice representing interval of numbers.
*/
export class IntervalLattice {
static FullInterval: Interval = [mInf(), pInf()];
static EmptyInterval: Interval = [pInf(), mInf()];
static FullInterval: Interval = [Num.m(), Num.p()];
static EmptyInterval: Interval = [Num.p(), Num.m()];

static bottom: Interval = IntervalLattice.EmptyInterval;
static top: Interval = IntervalLattice.FullInterval;

static int2num(i: number): IntNum {
return intNum(i);
}

/**
* Number as interval.
*/
static num(i: number): Interval {
const n = IntervalLattice.int2num(i);
const n = Num.int(i);
return [n, n];
}

/**
* Compare two Nums.
*/
static compareNum(a: Num, b: Num): number {
if (a.kind === "IntNum" && b.kind === "IntNum") {
return a.value - b.value;
} else if (a.kind === b.kind) {
return 0;
} else if (a.kind === "MInf" || b.kind === "PInf") {
return -1;
} else {
return 1;
}
}

/**
* Least upper bound (lub) of two intervals.
*/
Expand All @@ -56,8 +36,8 @@ export class IntervalLattice {
if (IntervalLattice.isEmptyInterval(y)) {
return x;
}
const lower = IntervalLattice.minNum(x[0], y[0]);
const upper = IntervalLattice.maxNum(x[1], y[1]);
const lower = Num.min(x[0], y[0]);
const upper = Num.max(x[1], y[1]);
return [lower, upper];
}

Expand All @@ -75,58 +55,21 @@ export class IntervalLattice {
return interval[0].kind === "PInf" && interval[1].kind === "MInf";
}

/**
* Adds two Nums.
*/
static addNums(a: Num, b: Num): Num {
if (a.kind === "IntNum" && b.kind === "IntNum") {
return intNum(a.value + b.value);
}
if (
(a.kind === "PInf" && b.kind === "MInf") ||
(a.kind === "MInf" && b.kind === "PInf")
) {
throw ExecutionException.make("Cannot add +inf and -inf");
}
if (a.kind === "PInf" || b.kind === "PInf") {
return pInf();
}
if (a.kind === "MInf" || b.kind === "MInf") {
return mInf();
}
throw InternalException.make("Invalid Num types for addition");
}

/**
* Abstract binary `+` on intervals.
*/
static plus(a: Interval, b: Interval): Interval {
const low = IntervalLattice.addNums(a[0], b[0]);
const high = IntervalLattice.addNums(a[1], b[1]);
const low = Num.add(a[0], b[0]);
const high = Num.add(a[1], b[1]);
return [low, high];
}

/**
* Negate a Num.
*/
static negateNum(n: Num): Num {
if (n.kind === "IntNum") {
return intNum(-n.value);
} else if (n.kind === "PInf") {
return mInf();
} else if (n.kind === "MInf") {
return pInf();
} else {
throw new Error("Invalid Num type for negation");
}
}

/**
* Abstract unary `-` (negation) on intervals.
*/
static inv(a: Interval): Interval {
const low = IntervalLattice.negateNum(a[1]);
const high = IntervalLattice.negateNum(a[0]);
const low = Num.negate(a[1]);
const high = Num.negate(a[0]);
return [low, high];
}

Expand All @@ -137,131 +80,36 @@ export class IntervalLattice {
return IntervalLattice.plus(a, IntervalLattice.inv(b));
}

/**
* Multiply two Nums.
*/
static multiplyNums(a: Num, b: Num): Num {
// Handle cases involving infinities
if (a.kind === "IntNum" && b.kind === "IntNum") {
return intNum(a.value * b.value);
}
if (IntervalLattice.isZeroNum(a) || IntervalLattice.isZeroNum(b)) {
return intNum(0);
}
if (
(a.kind === "PInf" || a.kind === "MInf") &&
(b.kind === "PInf" || b.kind === "MInf")
) {
if (a.kind === b.kind) {
return pInf();
} else {
return mInf();
}
}
if (a.kind === "IntNum") {
if (
(a.value > 0 && b.kind === "PInf") ||
(a.value < 0 && b.kind === "MInf")
) {
return pInf();
}
if (
(a.value > 0 && b.kind === "MInf") ||
(a.value < 0 && b.kind === "PInf")
) {
return mInf();
}
if (a.value === 0) {
return intNum(0);
}
}
if (b.kind === "IntNum") {
return IntervalLattice.multiplyNums(b, a);
}
throw new Error("Invalid Num types for multiplication");
}

/**
* Abstract binary `*` on intervals.
*/
static times(a: Interval, b: Interval): Interval {
const products = [
IntervalLattice.multiplyNums(a[0], b[0]),
IntervalLattice.multiplyNums(a[0], b[1]),
IntervalLattice.multiplyNums(a[1], b[0]),
IntervalLattice.multiplyNums(a[1], b[1]),
Num.multiply(a[0], b[0]),
Num.multiply(a[0], b[1]),
Num.multiply(a[1], b[0]),
Num.multiply(a[1], b[1]),
];
const low = IntervalLattice.minNum(...products);
const high = IntervalLattice.maxNum(...products);
const low = Num.min(...products);
const high = Num.max(...products);
return [low, high];
}

/**
* Checks if a Num is zero.
*/
static isZeroNum(n: Num): boolean {
return n.kind === "IntNum" && n.value === 0;
}

/**
* Divide two Nums.
*/
static divideNums(a: Num, b: Num): Num {
// Handle division by zero
if (IntervalLattice.isZeroNum(b)) {
throw ExecutionException.make("Division by zero");
}
if (a.kind === "IntNum" && b.kind === "IntNum") {
return intNum(a.value / b.value);
}
// Handle division involving infinities
if (a.kind === "IntNum") {
if (b.kind === "PInf" || b.kind === "MInf") {
return intNum(0);
}
}
if (b.kind === "IntNum") {
if (b.value > 0) {
if (a.kind === "PInf" || a.kind === "MInf") {
return a;
}
} else if (b.value < 0) {
if (a.kind === "PInf") {
return mInf();
}
if (a.kind === "MInf") {
return pInf();
}
}
}
if (a.kind === b.kind) {
return intNum(1);
}
if (
(a.kind === "PInf" && b.kind === "MInf") ||
(a.kind === "MInf" && b.kind === "PInf")
) {
return intNum(-1);
}
throw InternalException.make("Invalid Num types for division");
}

/**
* Abstract `/` on intervals.
*/
static div(a: Interval, b: Interval): Interval {
// Handle division by intervals containing zero
if (IntervalLattice.containsZero(b)) {
throw new Error("Division by interval containing zero");
}
const quotients = [
IntervalLattice.divideNums(a[0], b[0]),
IntervalLattice.divideNums(a[0], b[1]),
IntervalLattice.divideNums(a[1], b[0]),
IntervalLattice.divideNums(a[1], b[1]),
Num.divide(a[0], b[0]),
Num.divide(a[0], b[1]),
Num.divide(a[1], b[0]),
Num.divide(a[1], b[1]),
];
const low = IntervalLattice.minNum(...quotients);
const high = IntervalLattice.maxNum(...quotients);
const low = Num.min(...quotients);
const high = Num.max(...quotients);
return [low, high];
}

Expand All @@ -270,15 +118,15 @@ export class IntervalLattice {
*/
static containsZero(interval: Interval): boolean {
const [low, high] = interval;
const lowCompare = IntervalLattice.compareNum(low, intNum(0));
const highCompare = IntervalLattice.compareNum(high, intNum(0));
const lowCompare = Num.compare(low, Num.int(0));
const highCompare = Num.compare(high, Num.int(0));
return lowCompare <= 0 && highCompare >= 0;
}

/**
* Abstract `==` on intervals.
*/
static eqq(a: Interval, b: Interval): Interval {
static eq(a: Interval, b: Interval): Interval {
if (
IntervalLattice.isFullInterval(a) ||
IntervalLattice.isFullInterval(b)
Expand All @@ -294,7 +142,7 @@ export class IntervalLattice {
) {
return IntervalLattice.num(1);
}
return [intNum(0), intNum(1)];
return [Num.int(0), Num.int(1)];
}

/**
Expand All @@ -307,46 +155,13 @@ export class IntervalLattice {
) {
return IntervalLattice.FullInterval;
}
if (IntervalLattice.compareNum(a[1], b[0]) < 0) {
if (Num.compare(a[1], b[0]) < 0) {
return IntervalLattice.num(1);
}
if (IntervalLattice.compareNum(a[0], b[1]) > 0) {
if (Num.compare(a[0], b[1]) > 0) {
return IntervalLattice.num(0);
}
return [intNum(0), intNum(1)];
}

/**
* Finds the minimum of given Num values.
*/
static minNum(...nums: Num[]): Num {
return nums.reduce((a, b) =>
IntervalLattice.compareNum(a, b) <= 0 ? a : b,
);
}

/**
* Finds the maximum of given Num values.
*/
static maxNum(...nums: Num[]): Num {
return nums.reduce((a, b) =>
IntervalLattice.compareNum(a, b) >= 0 ? a : b,
);
}

/**
* Helper method to display Num as string
*/
static numToString(n: Num): string {
if (n.kind === "IntNum") {
return n.value.toString();
} else if (n.kind === "PInf") {
return "+inf";
} else if (n.kind === "MInf") {
return "-inf";
} else {
return "unknown";
}
return [Num.int(0), Num.int(1)];
}

static widen(a: Interval, b: Interval): Interval {
Expand All @@ -355,16 +170,16 @@ export class IntervalLattice {
return [lower, upper];
}

static widenNum(a: Num, b: Num, isLower: boolean): Num {
if (IntervalLattice.compareNum(a, b) === 0) {
static widenNum(a: NumImpl, b: NumImpl, isLower: boolean): NumImpl {
if (Num.compare(a, b) === 0) {
return a;
}
if (isLower) {
// If the new lower bound is less than the old, keep it; otherwise, set to -∞
return IntervalLattice.compareNum(b, a) < 0 ? b : mInf();
return Num.compare(b, a) < 0 ? b : Num.m();
} else {
// If the new upper bound is greater than the old, keep it; otherwise, set to +∞
return IntervalLattice.compareNum(b, a) > 0 ? b : pInf();
return Num.compare(b, a) > 0 ? b : Num.p();
}
}
}
Loading

0 comments on commit 5bc75a6

Please sign in to comment.