import { ModalFormula } from '../types.js';
/**
* Utility class for modal formula transformations
* Includes normalization, duality, and simplification
*/
export class ModalTransforms {
/**
* Apply modal duality: □φ ≡ ¬◇¬φ and ◇φ ≡ ¬□¬φ
*/
static applyDuality(formula: ModalFormula, toBox: boolean = true): ModalFormula {
if (!('type' in formula) || formula.type !== 'modal') {
return formula;
}
const isNecessity = formula.operator === '□' || formula.operator === 'necessary';
const isPossibility = formula.operator === '◇' || formula.operator === 'possible';
if (toBox && isPossibility) {
// ◇φ → ¬□¬φ
const innerNeg: ModalFormula = {
type: 'unary',
operator: '¬',
operand: formula.operand
} as any;
const boxFormula: ModalFormula = {
type: 'modal',
operator: '□',
operand: innerNeg
};
return {
type: 'unary',
operator: '¬',
operand: boxFormula
} as any;
} else if (!toBox && isNecessity) {
// □φ → ¬◇¬φ
const innerNeg: ModalFormula = {
type: 'unary',
operator: '¬',
operand: formula.operand
} as any;
const diamondFormula: ModalFormula = {
type: 'modal',
operator: '◇',
operand: innerNeg
};
return {
type: 'unary',
operator: '¬',
operand: diamondFormula
} as any;
}
return formula;
}
/**
* Normalize formula to use only □ (convert ◇ using duality)
*/
static normalizeToBox(formula: ModalFormula): ModalFormula {
if (!('type' in formula)) {
return formula;
}
switch (formula.type) {
case 'variable':
return formula;
case 'modal':
const isPossibility = formula.operator === '◇' || formula.operator === 'possible';
if (isPossibility) {
// ◇φ → ¬□¬φ
const innerNeg: ModalFormula = {
type: 'unary',
operator: '¬',
operand: this.normalizeToBox(formula.operand)
} as any;
const boxFormula: ModalFormula = {
type: 'modal',
operator: '□',
operand: innerNeg
};
return {
type: 'unary',
operator: '¬',
operand: boxFormula
} as any;
}
return {
type: 'modal',
operator: formula.operator,
operand: this.normalizeToBox(formula.operand)
};
case 'unary':
return {
type: 'unary',
operator: (formula as any).operator,
operand: this.normalizeToBox((formula as any).operand)
} as any;
case 'binary':
return {
type: 'binary',
operator: (formula as any).operator,
left: this.normalizeToBox((formula as any).left),
right: this.normalizeToBox((formula as any).right)
} as any;
default:
return formula;
}
}
/**
* Normalize formula to use only ◇ (convert □ using duality)
*/
static normalizeToDiamond(formula: ModalFormula): ModalFormula {
if (!('type' in formula)) {
return formula;
}
switch (formula.type) {
case 'variable':
return formula;
case 'modal':
const isNecessity = formula.operator === '□' || formula.operator === 'necessary';
if (isNecessity) {
// □φ → ¬◇¬φ
const innerNeg: ModalFormula = {
type: 'unary',
operator: '¬',
operand: this.normalizeToDiamond(formula.operand)
} as any;
const diamondFormula: ModalFormula = {
type: 'modal',
operator: '◇',
operand: innerNeg
};
return {
type: 'unary',
operator: '¬',
operand: diamondFormula
} as any;
}
return {
type: 'modal',
operator: formula.operator,
operand: this.normalizeToDiamond(formula.operand)
};
case 'unary':
return {
type: 'unary',
operator: (formula as any).operator,
operand: this.normalizeToDiamond((formula as any).operand)
} as any;
case 'binary':
return {
type: 'binary',
operator: (formula as any).operator,
left: this.normalizeToDiamond((formula as any).left),
right: this.normalizeToDiamond((formula as any).right)
} as any;
default:
return formula;
}
}
/**
* Push negations inward (useful for normalization)
*/
static pushNegation(formula: ModalFormula): ModalFormula {
if (!('type' in formula) || formula.type !== 'unary') {
return formula;
}
const operand = (formula as any).operand;
// ¬¬φ → φ
if ('type' in operand && operand.type === 'unary') {
return this.pushNegation(operand.operand);
}
// ¬□φ → ◇¬φ
if ('type' in operand && operand.type === 'modal') {
const isBox = operand.operator === '□' || operand.operator === 'necessary';
const negatedInner: ModalFormula = {
type: 'unary',
operator: '¬',
operand: operand.operand
} as any;
if (isBox) {
return {
type: 'modal',
operator: '◇',
operand: this.pushNegation(negatedInner)
};
} else {
// ¬◇φ → □¬φ
return {
type: 'modal',
operator: '□',
operand: this.pushNegation(negatedInner)
};
}
}
// ¬(φ ∧ ψ) → (¬φ ∨ ¬ψ)
if ('type' in operand && operand.type === 'binary') {
const op = operand.operator;
const negLeft: ModalFormula = { type: 'unary', operator: '¬', operand: operand.left } as any;
const negRight: ModalFormula = { type: 'unary', operator: '¬', operand: operand.right } as any;
if (op === 'and' || op === '∧') {
return {
type: 'binary',
operator: '∨',
left: this.pushNegation(negLeft),
right: this.pushNegation(negRight)
} as any;
} else if (op === 'or' || op === '∨') {
// ¬(φ ∨ ψ) → (¬φ ∧ ¬ψ)
return {
type: 'binary',
operator: '∧',
left: this.pushNegation(negLeft),
right: this.pushNegation(negRight)
} as any;
}
}
return formula;
}
/**
* Simplify double negations and trivial cases
*/
static simplify(formula: ModalFormula): ModalFormula {
if (!('type' in formula)) {
return formula;
}
switch (formula.type) {
case 'variable':
return formula;
case 'unary':
const unaryOp = (formula as any).operand;
const simplifiedOperand = this.simplify(unaryOp);
// ¬¬φ → φ
if ('type' in simplifiedOperand && simplifiedOperand.type === 'unary') {
return this.simplify((simplifiedOperand as any).operand);
}
return {
type: 'unary',
operator: (formula as any).operator,
operand: simplifiedOperand
} as any;
case 'modal':
return {
type: 'modal',
operator: formula.operator,
operand: this.simplify(formula.operand)
};
case 'binary':
const binaryFormula = formula as any;
return {
type: 'binary',
operator: binaryFormula.operator,
left: this.simplify(binaryFormula.left),
right: this.simplify(binaryFormula.right)
} as any;
default:
return formula;
}
}
/**
* Full normalization: simplify, push negations, normalize to box
*/
static normalize(formula: ModalFormula): ModalFormula {
let result = this.simplify(formula);
result = this.pushNegation(result);
result = this.normalizeToBox(result);
result = this.simplify(result); // Simplify again after transformations
return result;
}
}
