import { PredicateFormula, Quantifier } from '../../../types.js';
/**
* Scope information for quantifiers
*/
interface QuantifierScope {
id: string;
quantifier: Quantifier;
variable: string;
level: number;
parent: QuantifierScope | null;
children: QuantifierScope[];
formula: PredicateFormula;
}
/**
* Variable binding information
*/
interface VariableBinding {
variable: string;
boundBy: string | null; // null means free variable
occurrencePosition: { row: number; col: number };
}
/**
* Visualizer for quantifier scopes in predicate logic formulas
*/
export class QuantifierScopeVisualizer {
private scopeCounter: number = 0;
private scopeMap: Map<string, QuantifierScope>;
private bindings: VariableBinding[];
constructor() {
this.scopeMap = new Map();
this.bindings = [];
}
/**
* Visualize quantifier scopes in a predicate formula
* @param formula Formula to analyze
* @param format Output format
* @returns Visualization string
*/
visualize(formula: PredicateFormula, format: 'html' | 'svg' | 'text' = 'html'): string {
// Reset state
this.scopeCounter = 0;
this.scopeMap = new Map();
this.bindings = [];
// Analyze formula structure
const rootScope = this.analyzeFormula(formula, null, 0);
// Generate visualization
switch (format) {
case 'html':
return this.generateHTMLVisualization(formula, rootScope);
case 'svg':
return this.generateSVGVisualization(formula, rootScope);
case 'text':
return this.generateTextVisualization(formula, rootScope);
default:
return this.generateHTMLVisualization(formula, rootScope);
}
}
/**
* Analyze formula structure to build scope hierarchy
* @param formula Formula to analyze
* @param parentScope Parent scope
* @param level Nesting level
* @returns Current scope
*/
private analyzeFormula(
formula: PredicateFormula,
parentScope: QuantifierScope | null,
level: number
): QuantifierScope | null {
switch (formula.type) {
case 'quantified':
const scopeId = `scope_${this.scopeCounter++}`;
const scope: QuantifierScope = {
id: scopeId,
quantifier: formula.quantifier,
variable: formula.variable,
level: level,
parent: parentScope,
children: [],
formula: formula.formula
};
this.scopeMap.set(scopeId, scope);
// Add scope to parent's children
if (parentScope) {
parentScope.children.push(scope);
}
// Analyze inner formula with new scope
this.analyzeFormula(formula.formula, scope, level + 1);
return scope;
case 'binary':
this.analyzeFormula(formula.left, parentScope, level);
this.analyzeFormula(formula.right, parentScope, level);
return parentScope;
case 'unary':
this.analyzeFormula(formula.operand, parentScope, level);
return parentScope;
case 'variable':
// Check for variable binding
const bindingScope = this.findBindingScope(formula.name, parentScope);
this.bindings.push({
variable: formula.name,
boundBy: bindingScope?.id || null,
occurrencePosition: { row: 0, col: 0 } // Would need formula tokenization for accurate position
});
return parentScope;
default:
return parentScope;
}
}
/**
* Find the scope that binds a variable
* @param variable Variable name
* @param scope Current scope
* @returns Binding scope or null
*/
private findBindingScope(variable: string, scope: QuantifierScope | null): QuantifierScope | null {
if (!scope) return null;
if (scope.variable === variable) return scope;
return this.findBindingScope(variable, scope.parent);
}
/**
* Generate HTML visualization
* @param formula Original formula
* @param rootScope Root scope
* @returns HTML string
*/
private generateHTMLVisualization(formula: PredicateFormula, rootScope: QuantifierScope | null): string {
const styles = this.generateStyles();
const formulaHtml = this.generateFormulaWithScopes(formula, rootScope);
const scopeTreeHtml = this.generateScopeTree(rootScope);
const bindingsHtml = this.generateBindingsTable();
return `
<div class="quantifier-scope-visualization">
${styles}
<h3>Quantifier Scope Visualization</h3>
<div class="formula-container">
<h4>Formula with Scope Colors</h4>
${formulaHtml}
</div>
<div class="scope-tree-container">
<h4>Scope Hierarchy</h4>
${scopeTreeHtml}
</div>
<div class="bindings-container">
<h4>Variable Bindings</h4>
${bindingsHtml}
</div>
</div>
`;
}
/**
* Generate styles for HTML visualization
* @returns CSS style string
*/
private generateStyles(): string {
return `
<style>
.quantifier-scope-visualization {
font-family: Arial, sans-serif;
padding: 20px;
background-color: #f8f9fa;
border-radius: 10px;
box-shadow: 0 2px 4px rgba(0,0,0,0.1);
}
.formula-container, .scope-tree-container, .bindings-container {
margin: 20px 0;
border: 1px solid #dee2e6;
border-radius: 8px;
padding: 15px;
background-color: white;
}
.formula {
font-size: 24px;
margin: 10px 0;
text-align: center;
}
.quantifier {
padding: 2px 5px;
margin: 0 3px;
border-radius: 5px;
font-weight: bold;
border: 2px solid;
}
.bound-var {
padding: 2px 5px;
margin: 0 2px;
border-radius: 5px;
font-weight: bold;
border: 2px dashed;
}
.free-var {
padding: 2px 5px;
margin: 0 2px;
border-radius: 5px;
font-weight: bold;
border: 2px dashed #dc3545;
background-color: #f8d7da;
color: #721c24;
}
.scope-box {
border: 2px solid;
border-radius: 10px;
padding: 10px;
margin: 5px;
display: inline-block;
}
.scope-tree {
font-family: monospace;
white-space: pre;
margin-left: 20px;
}
.scope-node {
padding: 5px;
margin: 5px 0;
border-radius: 5px;
display: inline-block;
}
table {
width: 100%;
border-collapse: collapse;
margin: 10px 0;
}
th, td {
border: 1px solid #dee2e6;
padding: 8px;
text-align: left;
}
th {
background-color: #e9ecef;
}
.forall-scope {
background-color: rgba(54, 162, 235, 0.2);
border-color: rgba(54, 162, 235, 0.8);
}
.exists-scope {
background-color: rgba(255, 99, 132, 0.2);
border-color: rgba(255, 99, 132, 0.8);
}
.forall-var {
background-color: rgba(54, 162, 235, 0.4);
border-color: rgba(54, 162, 235, 0.8);
color: #004d99;
}
.exists-var {
background-color: rgba(255, 99, 132, 0.4);
border-color: rgba(255, 99, 132, 0.8);
color: #990033;
}
</style>
`;
}
/**
* Generate formula HTML with scope highlighting
* @param formula Formula to format
* @param scope Current scope
* @returns HTML string
*/
private generateFormulaWithScopes(formula: PredicateFormula, scope: QuantifierScope | null): string {
let html = '<div class="formula">';
const formatWithScopes = (f: PredicateFormula, s: QuantifierScope | null, level: number = 0): string => {
switch (f.type) {
case 'quantified':
const newScope = Array.from(this.scopeMap.values()).find(
sc => sc.parent === s && sc.variable === f.variable && sc.level === level + 1
);
const quantifiedClass = f.quantifier === 'forall' ? 'forall-scope' : 'exists-scope';
let quantifiedResult = `<span class="scope-box ${quantifiedClass}">`;
quantifiedResult += `<span class="quantifier">${f.quantifier === 'forall' ? '∀' : '∃'}</span>`;
quantifiedResult += `<span class="quantifier">${f.variable}</span>`;
quantifiedResult += '. ';
quantifiedResult += formatWithScopes(f.formula, newScope || null, level + 1);
quantifiedResult += '</span>';
return quantifiedResult;
case 'variable':
const bindingScope = this.findBindingScope(f.name, s);
if (bindingScope) {
const varClass = bindingScope.quantifier === 'forall' ? 'forall-var' : 'exists-var';
return `<span class="bound-var ${varClass}">${f.name}</span>`;
} else {
return `<span class="free-var">${f.name}</span>`;
}
case 'binary':
const left = formatWithScopes(f.left, s, level);
const right = formatWithScopes(f.right, s, level);
// Add parentheses if needed
const leftStr = f.left.type === 'binary' || f.left.type === 'quantified' ? `(${left})` : left;
const rightStr = f.right.type === 'binary' || f.right.type === 'quantified' ? `(${right})` : right;
let binaryOpSymbol: string;
switch (f.operator) {
case 'and': binaryOpSymbol = '∧'; break;
case 'or': binaryOpSymbol = '∨'; break;
case 'implies': binaryOpSymbol = '→'; break;
case 'iff': binaryOpSymbol = '↔'; break;
default: binaryOpSymbol = f.operator;
}
return `${leftStr} ${binaryOpSymbol} ${rightStr}`;
case 'unary':
const unaryOpSymbol = f.operator === 'not' ? '¬' : f.operator;
const operand = formatWithScopes(f.operand, s, level);
// Add parentheses if the operand is complex
if (f.operand.type === 'binary' || f.operand.type === 'quantified') {
return `${unaryOpSymbol}(${operand})`;
} else {
return `${unaryOpSymbol}${operand}`;
}
case 'predicate':
if (f.args.length === 0) {
return f.name;
} else {
const args = f.args.map(arg => formatWithScopes(arg, s, level)).join(', ');
return `${f.name}(${args})`;
}
default:
return f.toString();
}
};
html += formatWithScopes(formula, scope, 0);
html += '</div>';
return html;
}
/**
* Generate scope tree visualization
* @param rootScope Root scope
* @returns HTML string
*/
private generateScopeTree(rootScope: QuantifierScope | null): string {
if (!rootScope) {
return '<p>No quantifier scopes found in the formula.</p>';
}
let html = '<div class="scope-tree">';
const formatScope = (scope: QuantifierScope, level: number = 0): string => {
const indent = ' '.repeat(level);
const scopeClass = scope.quantifier === 'forall' ? 'forall-scope' : 'exists-scope';
let result = `${indent}<span class="scope-node ${scopeClass}">`;
result += `${scope.quantifier === 'forall' ? '∀' : '∃'}${scope.variable} (Level ${scope.level})</span>\n`;
scope.children.forEach(child => {
result += formatScope(child, level + 1);
});
return result;
};
html += formatScope(rootScope);
html += '</div>';
return html;
}
/**
* Generate bindings table
* @returns HTML string
*/
private generateBindingsTable(): string {
let html = `
<table>
<thead>
<tr>
<th>Variable</th>
<th>Status</th>
<th>Bound By</th>
</tr>
</thead>
<tbody>
`;
const variableMap = new Map<string, { boundCount: number; freeCount: number; boundBy: string[] }>();
this.bindings.forEach(binding => {
if (!variableMap.has(binding.variable)) {
variableMap.set(binding.variable, { boundCount: 0, freeCount: 0, boundBy: [] });
}
const stats = variableMap.get(binding.variable)!;
if (binding.boundBy) {
stats.boundCount++;
const scope = this.scopeMap.get(binding.boundBy)!;
const bindingInfo = `${scope.quantifier === 'forall' ? '∀' : '∃'}${scope.variable}`;
if (!stats.boundBy.includes(bindingInfo)) {
stats.boundBy.push(bindingInfo);
}
} else {
stats.freeCount++;
}
});
variableMap.forEach((stats, variable) => {
let status = '';
if (stats.boundCount > 0 && stats.freeCount > 0) {
status = 'Mixed (both bound and free)';
} else if (stats.boundCount > 0) {
status = 'Bound';
} else {
status = 'Free';
}
const boundBy = stats.boundBy.length > 0 ? stats.boundBy.join(', ') : '-';
html += `
<tr>
<td>${variable}</td>
<td>${status}</td>
<td>${boundBy}</td>
</tr>
`;
});
html += '</tbody></table>';
return html;
}
/**
* Generate SVG visualization
* @param formula Original formula
* @param rootScope Root scope
* @returns SVG string
*/
private generateSVGVisualization(formula: PredicateFormula, rootScope: QuantifierScope | null): string {
const width = 1200;
const height = 800;
const nodeSize = 60;
const nodeSpacing = 100;
let svg = `<svg width="${width}" height="${height}" xmlns="http://www.w3.org/2000/svg">\n`;
svg += '<rect x="0" y="0" width="100%" height="100%" fill="#f8f9fa" />\n';
// Title
svg += `<text x="${width/2}" y="30" text-anchor="middle" font-family="Arial" font-size="24" font-weight="bold">Quantifier Scope Visualization</text>\n`;
let y = 80;
// Formula with scope boxes
svg += this.drawFormulaWithScopeBoxes(formula, 50, y, rootScope);
// Scope hierarchy
y += 300;
svg += this.drawScopeHierarchy(rootScope, width/2, y, nodeSize, nodeSpacing);
svg += '</svg>';
return svg;
}
/**
* Draw formula with scope boxes in SVG
* @param formula Formula to draw
* @param x X position
* @param y Y position
* @param scope Current scope
* @returns SVG string
*/
private drawFormulaWithScopeBoxes(
formula: PredicateFormula,
x: number,
y: number,
scope: QuantifierScope | null
): string {
let svg = '';
let currentX = x;
const boxPadding = 10;
const textHeight = 20;
const drawBox = (content: string, color: string, level: number): string => {
const textWidth = content.length * 12; // Approximate width
const boxWidth = textWidth + boxPadding * 2;
const boxHeight = textHeight + boxPadding * 2;
let boxSvg = `<g transform="translate(${currentX}, ${y + level * 40})">\n`;
boxSvg += ` <rect x="0" y="0" width="${boxWidth}" height="${boxHeight}" fill="${color}" rx="5" />\n`;
boxSvg += ` <text x="${boxPadding}" y="${boxPadding + textHeight - 5}" font-family="Arial" font-size="16" fill="black">${content}</text>\n`;
boxSvg += '</g>\n';
currentX += boxWidth + 10;
return boxSvg;
};
const formatFormula = (f: PredicateFormula, s: QuantifierScope | null, level: number = 0): string => {
switch (f.type) {
case 'quantified':
const quantifiedSymbol = f.quantifier === 'forall' ? '∀' : '∃';
const quantifiedColor = f.quantifier === 'forall' ? 'rgba(54, 162, 235, 0.3)' : 'rgba(255, 99, 132, 0.3)';
const quantifiedScope = Array.from(this.scopeMap.values()).find(
sc => sc.parent === s && sc.variable === f.variable && sc.level === level + 1
);
let quantifiedResult = `<g>\n`;
quantifiedResult += ' ' + drawBox(`${quantifiedSymbol}${f.variable}.`, quantifiedColor, level);
quantifiedResult += formatFormula(f.formula, quantifiedScope || null, level + 1);
quantifiedResult += '</g>\n';
return quantifiedResult;
case 'variable':
const variableBindingScope = this.findBindingScope(f.name, s);
let variableColor = 'rgba(220, 53, 69, 0.3)'; // free variable color
if (variableBindingScope) {
variableColor = variableBindingScope.quantifier === 'forall'
? 'rgba(54, 162, 235, 0.5)'
: 'rgba(255, 99, 132, 0.5)';
}
return drawBox(f.name, variableColor, 0);
case 'binary':
let binarySymbol: string;
switch (f.operator) {
case 'and': binarySymbol = '∧'; break;
case 'or': binarySymbol = '∨'; break;
case 'implies': binarySymbol = '→'; break;
case 'iff': binarySymbol = '↔'; break;
default: binarySymbol = f.operator;
}
let binaryResult = formatFormula(f.left, s, level);
binaryResult += drawBox(binarySymbol, 'rgba(169, 169, 169, 0.3)', level);
binaryResult += formatFormula(f.right, s, level);
return binaryResult;
case 'predicate':
if (f.args.length === 0) {
return drawBox(f.name, 'rgba(40, 167, 69, 0.3)', level);
} else {
let result = drawBox(f.name + '(', 'rgba(40, 167, 69, 0.3)', level);
f.args.forEach((arg, index) => {
result += formatFormula(arg, s, level);
if (index < f.args.length - 1) {
result += drawBox(',', 'rgba(169, 169, 169, 0.3)', level);
}
});
result += drawBox(')', 'rgba(40, 167, 69, 0.3)', level);
return result;
}
default:
return '';
}
};
svg += '<g class="formula-svg">\n';
svg += formatFormula(formula, scope);
svg += '</g>\n';
return svg;
}
/**
* Draw scope hierarchy tree in SVG
* @param rootScope Root scope
* @param cx Center X position
* @param cy Center Y position
* @param nodeSize Node size
* @param spacing Node spacing
* @returns SVG string
*/
private drawScopeHierarchy(
rootScope: QuantifierScope | null,
cx: number,
cy: number,
nodeSize: number,
spacing: number
): string {
if (!rootScope) {
return `<text x="${cx}" y="${cy}" text-anchor="middle" font-family="Arial" font-size="16">No quantifier scopes found</text>\n`;
}
let svg = '';
// Calculate positions for all nodes
const positions = new Map<string, { x: number; y: number }>();
let currentX = cx;
const levelHeight = spacing;
const layoutScope = (scope: QuantifierScope, level: number): void => {
positions.set(scope.id, { x: currentX, y: cy + level * levelHeight });
scope.children.forEach(child => {
layoutScope(child, level + 1);
});
currentX += spacing;
};
layoutScope(rootScope, 0);
// Draw connections
svg += '<g class="scope-connections">\n';
const drawConnections = (scope: QuantifierScope): void => {
const parentPos = positions.get(scope.id)!;
scope.children.forEach(child => {
const childPos = positions.get(child.id)!;
svg += ` <line x1="${parentPos.x}" y1="${parentPos.y + nodeSize/2}" x2="${childPos.x}" y2="${childPos.y - nodeSize/2}" stroke="#dee2e6" stroke-width="2" />\n`;
drawConnections(child);
});
};
drawConnections(rootScope);
svg += '</g>\n';
// Draw scope nodes
svg += '<g class="scope-nodes">\n';
const drawNodes = (scope: QuantifierScope): void => {
const pos = positions.get(scope.id)!;
const quantSymbol = scope.quantifier === 'forall' ? '∀' : '∃';
const color = scope.quantifier === 'forall' ? '#36a2eb' : '#ff6384';
// Draw circle
svg += ` <circle cx="${pos.x}" cy="${pos.y}" r="${nodeSize/2}" fill="${color}" stroke="#2c3e50" stroke-width="2" />\n`;
// Draw text
svg += ` <text x="${pos.x}" y="${pos.y + 5}" text-anchor="middle" font-family="Arial" font-size="20" font-weight="bold" fill="white">${quantSymbol}${scope.variable}</text>\n`;
scope.children.forEach(child => drawNodes(child));
};
drawNodes(rootScope);
svg += '</g>\n';
return svg;
}
/**
* Generate text visualization
* @param formula Original formula
* @param rootScope Root scope
* @returns Text string
*/
private generateTextVisualization(formula: PredicateFormula, rootScope: QuantifierScope | null): string {
let text = 'Quantifier Scope Analysis\n';
text += '=======================\n\n';
text += 'Formula: ' + this.formatFormulaText(formula) + '\n\n';
// Scope hierarchy
text += 'Scope Hierarchy:\n';
if (rootScope) {
text += this.formatScopeTree(rootScope, 0);
} else {
text += ' No quantifier scopes found\n';
}
text += '\n';
// Variable analysis
text += 'Variable Analysis:\n';
const variableStats = this.getVariableStats();
for (const [variable, stats] of variableStats) {
text += ` ${variable}:\n`;
if (stats.freeOccurrences > 0) {
text += ` - Free occurrences: ${stats.freeOccurrences}\n`;
}
if (stats.boundScopes.length > 0) {
text += ` - Bound by: ${stats.boundScopes.join(', ')}\n`;
}
}
return text;
}
/**
* Format formula as text string
* @param formula Formula
* @returns Text string
*/
private formatFormulaText(formula: PredicateFormula): string {
switch (formula.type) {
case 'quantified':
const quantSymbol = formula.quantifier === 'forall' ? '∀' : '∃';
return `${quantSymbol}${formula.variable}. ${this.formatFormulaText(formula.formula)}`;
case 'variable':
return formula.name;
case 'binary':
const left = this.formatFormulaText(formula.left);
const right = this.formatFormulaText(formula.right);
let textOpSymbol: string;
switch (formula.operator) {
case 'and': textOpSymbol = '∧'; break;
case 'or': textOpSymbol = '∨'; break;
case 'implies': textOpSymbol = '→'; break;
case 'iff': textOpSymbol = '↔'; break;
default: textOpSymbol = formula.operator;
}
// Add parentheses if needed
const leftStr = formula.left.type === 'binary' || formula.left.type === 'quantified' ? `(${left})` : left;
const rightStr = formula.right.type === 'binary' || formula.right.type === 'quantified' ? `(${right})` : right;
return `${leftStr} ${textOpSymbol} ${rightStr}`;
case 'unary':
const textUnarySymbol = formula.operator === 'not' ? '¬' : formula.operator;
const operand = this.formatFormulaText(formula.operand);
if (formula.operand.type === 'binary' || formula.operand.type === 'quantified') {
return `${textUnarySymbol}(${operand})`;
} else {
return `${textUnarySymbol}${operand}`;
}
case 'predicate':
if (formula.args.length === 0) {
return formula.name;
} else {
const args = formula.args.map(arg => this.formatFormulaText(arg)).join(', ');
return `${formula.name}(${args})`;
}
default:
return '';
}
}
/**
* Format scope tree as text
* @param scope Current scope
* @param level Indentation level
* @returns Text string
*/
private formatScopeTree(scope: QuantifierScope, level: number): string {
const indent = ' '.repeat(level);
const quantSymbol = scope.quantifier === 'forall' ? '∀' : '∃';
let text = `${indent}${quantSymbol}${scope.variable} (Level ${scope.level})\n`;
scope.children.forEach(child => {
text += this.formatScopeTree(child, level + 1);
});
return text;
}
/**
* Get variable statistics
* @returns Map of variable to stats
*/
private getVariableStats(): Map<string, { boundScopes: string[]; freeOccurrences: number }> {
const stats = new Map<string, { boundScopes: string[]; freeOccurrences: number }>();
this.bindings.forEach(binding => {
if (!stats.has(binding.variable)) {
stats.set(binding.variable, { boundScopes: [], freeOccurrences: 0 });
}
const varStats = stats.get(binding.variable)!;
if (binding.boundBy) {
const scope = this.scopeMap.get(binding.boundBy)!;
const scopeStr = `${scope.quantifier === 'forall' ? '∀' : '∃'}${scope.variable}`;
if (!varStats.boundScopes.includes(scopeStr)) {
varStats.boundScopes.push(scopeStr);
}
} else {
varStats.freeOccurrences++;
}
});
return stats;
}
}
