import { PredicateFormula } from '../types.js';
/**
* Utilities for variable substitution in predicate logic formulas
*/
/**
* Substitute a term for a variable in a formula
* @param formula The formula to perform substitution in
* @param variable The variable to replace
* @param term The term to substitute
* @returns The formula with substitutions applied
*/
export function substitute(
formula: PredicateFormula,
variable: string,
term: PredicateFormula
): PredicateFormula {
switch (formula.type) {
case 'variable':
// Replace this variable if it matches
return formula.name === variable ? term : formula;
case 'constant':
// Constants are never substituted
return formula;
case 'function':
// Recursively substitute in function arguments
return {
type: 'function',
name: formula.name,
args: formula.args.map(arg => substitute(arg, variable, term))
};
case 'predicate':
// Recursively substitute in predicate arguments
return {
type: 'predicate',
name: formula.name,
args: formula.args.map(arg => substitute(arg, variable, term))
};
case 'unary':
// Recursively substitute in operand
return {
type: 'unary',
operator: formula.operator,
operand: substitute(formula.operand, variable, term)
};
case 'binary':
// Recursively substitute in both sides
return {
type: 'binary',
operator: formula.operator,
left: substitute(formula.left, variable, term),
right: substitute(formula.right, variable, term)
};
case 'quantified':
// Don't substitute if the quantifier binds this variable
if (formula.variable === variable) {
return formula;
}
// Check for variable capture
const freeVars = getFreeVariables(term);
if (freeVars.has(formula.variable)) {
// Would cause variable capture - need alpha conversion first
throw new Error(
`Substitution would cause variable capture: ${formula.variable} appears free in ${formatFormula(term)}`
);
}
// Recursively substitute in body
return {
type: 'quantified',
quantifier: formula.quantifier,
variable: formula.variable,
formula: substitute(formula.formula, variable, term)
};
}
}
/**
* Get all free variables in a formula
* @param formula The formula to analyze
* @param bound Set of currently bound variables
* @returns Set of free variable names
*/
export function getFreeVariables(
formula: PredicateFormula,
bound: Set<string> = new Set()
): Set<string> {
const freeVars = new Set<string>();
switch (formula.type) {
case 'variable':
// Variable is free if not bound
if (!bound.has(formula.name)) {
freeVars.add(formula.name);
}
break;
case 'constant':
// Constants have no variables
break;
case 'function':
// Collect free variables from all arguments
for (const arg of formula.args) {
for (const v of getFreeVariables(arg, bound)) {
freeVars.add(v);
}
}
break;
case 'predicate':
// Collect free variables from all arguments
for (const arg of formula.args) {
for (const v of getFreeVariables(arg, bound)) {
freeVars.add(v);
}
}
break;
case 'unary':
// Collect free variables from operand
for (const v of getFreeVariables(formula.operand, bound)) {
freeVars.add(v);
}
break;
case 'binary':
// Collect free variables from both sides
for (const v of getFreeVariables(formula.left, bound)) {
freeVars.add(v);
}
for (const v of getFreeVariables(formula.right, bound)) {
freeVars.add(v);
}
break;
case 'quantified':
// Add this variable to bound set and check body
const newBound = new Set(bound);
newBound.add(formula.variable);
for (const v of getFreeVariables(formula.formula, newBound)) {
freeVars.add(v);
}
break;
}
return freeVars;
}
/**
* Check if two formulas are structurally equal
* @param f1 First formula
* @param f2 Second formula
* @returns True if formulas are equal
*/
export function formulaEquals(f1: PredicateFormula, f2: PredicateFormula): boolean {
if (f1.type !== f2.type) {
return false;
}
switch (f1.type) {
case 'variable':
return f2.type === 'variable' && f1.name === f2.name;
case 'constant':
return f2.type === 'constant' && f1.name === f2.name;
case 'function':
return (
f2.type === 'function' &&
f1.name === f2.name &&
f1.args.length === f2.args.length &&
f1.args.every((arg, i) => formulaEquals(arg, f2.args[i]))
);
case 'predicate':
return (
f2.type === 'predicate' &&
f1.name === f2.name &&
f1.args.length === f2.args.length &&
f1.args.every((arg, i) => formulaEquals(arg, f2.args[i]))
);
case 'unary':
return (
f2.type === 'unary' &&
f1.operator === f2.operator &&
formulaEquals(f1.operand, f2.operand)
);
case 'binary':
return (
f2.type === 'binary' &&
f1.operator === f2.operator &&
formulaEquals(f1.left, f2.left) &&
formulaEquals(f1.right, f2.right)
);
case 'quantified':
return (
f2.type === 'quantified' &&
f1.quantifier === f2.quantifier &&
f1.variable === f2.variable &&
formulaEquals(f1.formula, f2.formula)
);
}
}
/**
* Check if formula1 can be instantiated to formula2 by substituting variable
* @param template The template formula with variable
* @param instance The instance formula
* @param variable The variable to check substitution for
* @returns True if instantiation is possible, false otherwise
*/
export function canInstantiate(
template: PredicateFormula,
instance: PredicateFormula,
variable: string
): boolean {
// Try to find what term variable should be substituted with
const term = findSubstitution(template, instance, variable);
if (term === null) {
return false;
}
// Verify that applying this substitution gives us the instance
try {
const result = substitute(template, variable, term);
return formulaEquals(result, instance);
} catch {
// Substitution failed (e.g., variable capture)
return false;
}
}
/**
* Find the term that variable should be substituted with to transform template into instance
* @param template The template formula
* @param instance The instance formula
* @param variable The variable to find substitution for
* @returns The term to substitute, or null if no valid substitution exists
*/
function findSubstitution(
template: PredicateFormula,
instance: PredicateFormula,
variable: string
): PredicateFormula | null {
// Base case: if template is the variable we're looking for, return instance
if (template.type === 'variable' && template.name === variable) {
return instance;
}
// If types don't match, no substitution possible
if (template.type !== instance.type) {
return null;
}
// Check each case
switch (template.type) {
case 'variable':
// Different variable - must match exactly
return instance.type === 'variable' && template.name === instance.name
? template
: null;
case 'constant':
// Constants must match exactly
return instance.type === 'constant' && template.name === instance.name
? template
: null;
case 'function':
if (
instance.type === 'function' &&
template.name === instance.name &&
template.args.length === instance.args.length
) {
// Find substitution from first argument (all must agree)
let term: PredicateFormula | null = null;
for (let i = 0; i < template.args.length; i++) {
const argTerm = findSubstitution(template.args[i], instance.args[i], variable);
if (argTerm === null) {
return null;
}
if (argTerm.type === 'variable' && argTerm.name === variable) {
continue; // This argument doesn't constrain the substitution
}
if (term === null) {
term = argTerm;
} else if (!formulaEquals(term, argTerm)) {
return null; // Inconsistent substitution
}
}
return term;
}
return null;
case 'predicate':
if (
instance.type === 'predicate' &&
template.name === instance.name &&
template.args.length === instance.args.length
) {
// Find substitution from arguments
let term: PredicateFormula | null = null;
for (let i = 0; i < template.args.length; i++) {
const argTerm = findSubstitution(template.args[i], instance.args[i], variable);
if (argTerm === null) {
return null;
}
if (argTerm.type === 'variable' && argTerm.name === variable) {
continue;
}
if (term === null) {
term = argTerm;
} else if (!formulaEquals(term, argTerm)) {
return null;
}
}
return term;
}
return null;
case 'unary':
if (instance.type === 'unary' && template.operator === instance.operator) {
return findSubstitution(template.operand, instance.operand, variable);
}
return null;
case 'binary':
if (
instance.type === 'binary' &&
template.operator === instance.operator
) {
const leftTerm = findSubstitution(template.left, instance.left, variable);
const rightTerm = findSubstitution(template.right, instance.right, variable);
if (leftTerm === null || rightTerm === null) {
return null;
}
// Check if both sides give consistent substitution
const leftIsVar = leftTerm.type === 'variable' && leftTerm.name === variable;
const rightIsVar = rightTerm.type === 'variable' && rightTerm.name === variable;
if (leftIsVar && !rightIsVar) {
return rightTerm;
}
if (!leftIsVar && rightIsVar) {
return leftTerm;
}
if (leftIsVar && rightIsVar) {
return leftTerm; // Both unconstrained
}
if (formulaEquals(leftTerm, rightTerm)) {
return leftTerm;
}
return null; // Inconsistent
}
return null;
case 'quantified':
if (
instance.type === 'quantified' &&
template.quantifier === instance.quantifier &&
template.variable === instance.variable
) {
// Don't substitute under a quantifier that binds our variable
if (template.variable === variable) {
return formulaEquals(template.formula, instance.formula) ? template : null;
}
return findSubstitution(template.formula, instance.formula, variable);
}
return null;
}
}
/**
* Format a formula as a string for display
* @param formula The formula to format
* @returns Formatted string
*/
export function formatFormula(formula: PredicateFormula): string {
switch (formula.type) {
case 'variable':
return formula.name;
case 'constant':
return formula.name;
case 'function':
const args = formula.args.map(arg => formatFormula(arg)).join(', ');
return `${formula.name}(${args})`;
case 'predicate':
if (formula.args.length === 0) {
return formula.name;
} else {
const predArgs = formula.args.map(arg => formatFormula(arg)).join(', ');
return `${formula.name}(${predArgs})`;
}
case 'unary':
const operand = formatFormula(formula.operand);
const needsParens = formula.operand.type === 'binary' || formula.operand.type === 'quantified';
const operandStr = needsParens ? `(${operand})` : operand;
return `¬${operandStr}`;
case 'binary':
const left = formatFormula(formula.left);
const right = formatFormula(formula.right);
const leftNeedsParens = formula.left.type === 'binary' || formula.left.type === 'quantified';
const rightNeedsParens = formula.right.type === 'binary' || formula.right.type === 'quantified';
const leftStr = leftNeedsParens ? `(${left})` : left;
const rightStr = rightNeedsParens ? `(${right})` : right;
const operator = getSymbolForOperator(formula.operator);
return `${leftStr} ${operator} ${rightStr}`;
case 'quantified':
const quantSymbol = formula.quantifier === 'forall' ? '∀' : '∃';
const bodyStr = formatFormula(formula.formula);
return `${quantSymbol}${formula.variable}. ${bodyStr}`;
}
}
/**
* Get the symbol for a logical operator
* @param operator The operator
* @returns Symbol
*/
function getSymbolForOperator(operator: string): string {
switch (operator) {
case 'and': return '∧';
case 'or': return '∨';
case 'implies': return '→';
case 'iff': return '↔';
case 'xor': return '⊕';
default: return operator;
}
}
