/**
* ProbLog Validator - Syntax and Semantic Validation
* Validates probabilistic logic programs for correctness
*/
import {
ProbabilisticProgram,
ProbabilisticAnalysis
} from '../../types.js';
import { Loggers } from '../../utils/logger.js';
const logger = Loggers.manager;
export class ProbLogValidator {
/**
* Validate probabilistic program
*/
validate(program: ProbabilisticProgram): ProbabilisticAnalysis {
const errors: string[] = [];
const warnings: string[] = [];
// 1. Probability range validation
this.validateProbabilityRanges(program, errors);
// 2. Cyclic dependency detection
const cycles = this.detectCycles(program);
if (cycles.length > 0) {
warnings.push(
`Cyclic dependencies detected: ${cycles.join(', ')}. ` +
`This may cause infinite loops or undefined behavior.`
);
}
// 3. Undefined predicates
const undefined = this.findUndefinedPredicates(program);
if (undefined.size > 0) {
warnings.push(
`Undefined predicates used in rules: ${[...undefined].join(', ')}. ` +
`Consider adding probabilistic facts for these.`
);
}
// 4. Evidence consistency
if (program.evidence) {
const inconsistent = this.checkEvidenceConsistency(program);
if (inconsistent.length > 0) {
errors.push(
`Evidence contains contradictions: ${inconsistent.join(', ')}`
);
}
}
// 5. Check for empty program
if (program.facts.length === 0 && program.rules.length === 0) {
errors.push('Program is empty. Add at least one fact or rule.');
}
const isValid = errors.length === 0;
const explanation = this.generateExplanation(isValid, errors, warnings);
logger.debug('Validation complete', {
isValid,
errorCount: errors.length,
warningCount: warnings.length
});
return {
isValid,
errors,
warnings,
explanation
};
}
/**
* Validate probability ranges
*/
private validateProbabilityRanges(program: ProbabilisticProgram, errors: string[]): void {
for (const fact of program.facts) {
if (fact.probability < 0 || fact.probability > 1) {
errors.push(
`Invalid probability for fact "${fact.fact}": ${fact.probability} ` +
`(must be between 0 and 1)`
);
}
if (isNaN(fact.probability)) {
errors.push(
`Probability for fact "${fact.fact}" is NaN`
);
}
}
for (const rule of program.rules) {
if (rule.probability !== undefined) {
if (rule.probability < 0 || rule.probability > 1) {
errors.push(
`Invalid probability for rule "${rule.head}": ${rule.probability} ` +
`(must be between 0 and 1)`
);
}
if (isNaN(rule.probability)) {
errors.push(
`Probability for rule "${rule.head}" is NaN`
);
}
}
}
}
/**
* Detect cyclic dependencies in rules
*/
private detectCycles(program: ProbabilisticProgram): string[] {
// Build dependency graph
const graph = new Map<string, Set<string>>();
for (const rule of program.rules) {
if (!graph.has(rule.head)) {
graph.set(rule.head, new Set());
}
for (const bodyAtom of rule.body) {
graph.get(rule.head)!.add(bodyAtom);
}
}
// Detect cycles using DFS
const cycles: string[] = [];
const visited = new Set<string>();
const recStack = new Set<string>();
const dfs = (node: string, path: string[]): void => {
visited.add(node);
recStack.add(node);
path.push(node);
const neighbors = graph.get(node);
if (neighbors) {
for (const neighbor of neighbors) {
if (!visited.has(neighbor)) {
dfs(neighbor, [...path]);
} else if (recStack.has(neighbor)) {
const cycleStart = path.indexOf(neighbor);
if (cycleStart >= 0) {
cycles.push(path.slice(cycleStart).join(' → ') + ' → ' + neighbor);
}
}
}
}
recStack.delete(node);
};
for (const node of graph.keys()) {
if (!visited.has(node)) {
dfs(node, []);
}
}
return cycles;
}
/**
* Find undefined predicates
*/
private findUndefinedPredicates(program: ProbabilisticProgram): Set<string> {
const defined = new Set<string>();
const used = new Set<string>();
// Collect defined predicates
for (const fact of program.facts) {
defined.add(this.extractPredicate(fact.fact));
}
for (const rule of program.rules) {
defined.add(this.extractPredicate(rule.head));
}
// Collect used predicates
for (const rule of program.rules) {
for (const bodyAtom of rule.body) {
used.add(this.extractPredicate(bodyAtom));
}
}
// Find difference
const undefined = new Set<string>();
for (const predicate of used) {
if (!defined.has(predicate)) {
undefined.add(predicate);
}
}
return undefined;
}
/**
* Extract predicate name from atom
*/
private extractPredicate(atom: string): string {
// Extract predicate name from atom like "rain(monday)" -> "rain"
const match = atom.match(/^(\w+)/);
return match ? match[1] : atom;
}
/**
* Check evidence consistency
*/
private checkEvidenceConsistency(program: ProbabilisticProgram): string[] {
const inconsistent: string[] = [];
if (!program.evidence) return inconsistent;
// Check for complementary facts
for (const [fact, value] of Object.entries(program.evidence)) {
const negatedFact = `not_${fact}`;
const negatedValue = program.evidence[negatedFact];
if (negatedValue !== undefined && value === negatedValue) {
inconsistent.push(`${fact} and ${negatedFact} cannot both be ${value}`);
}
}
return inconsistent;
}
/**
* Generate explanation based on validation results
*/
private generateExplanation(isValid: boolean, errors: string[], warnings: string[]): string {
if (isValid && warnings.length === 0) {
return 'Program is valid and well-formed.';
}
const parts: string[] = [];
if (!isValid) {
parts.push(`Program has ${errors.length} error(s):`);
errors.forEach((err, i) => {
parts.push(` ${i + 1}. ${err}`);
});
}
if (warnings.length > 0) {
parts.push(`\nProgram has ${warnings.length} warning(s):`);
warnings.forEach((warn, i) => {
parts.push(` ${i + 1}. ${warn}`);
});
}
if (!isValid) {
parts.push('\nProgram cannot be executed until errors are fixed.');
} else {
parts.push('\nProgram is valid but consider addressing warnings.');
}
return parts.join('\n');
}
/**
* Validate query against program
*/
validateQuery(query: string, program: ProbabilisticProgram): {
isValid: boolean;
message: string;
} {
const queryPredicate = this.extractPredicate(query);
// Check if query predicate is defined in the program
const defined = new Set<string>();
for (const fact of program.facts) {
defined.add(this.extractPredicate(fact.fact));
}
for (const rule of program.rules) {
defined.add(this.extractPredicate(rule.head));
}
if (!defined.has(queryPredicate)) {
return {
isValid: false,
message: `Query predicate "${queryPredicate}" is not defined in the program. ` +
`Available predicates: ${[...defined].join(', ')}`
};
}
return {
isValid: true,
message: 'Query is valid.'
};
}
/**
* Validate evidence against program
*/
validateEvidence(evidence: Record<string, boolean>, program: ProbabilisticProgram): {
isValid: boolean;
message: string;
} {
const defined = new Set<string>();
for (const fact of program.facts) {
defined.add(this.extractPredicate(fact.fact));
}
for (const rule of program.rules) {
defined.add(this.extractPredicate(rule.head));
}
const undefinedEvidence: string[] = [];
for (const evidenceFact of Object.keys(evidence)) {
const predicate = this.extractPredicate(evidenceFact);
if (!defined.has(predicate)) {
undefinedEvidence.push(evidenceFact);
}
}
if (undefinedEvidence.length > 0) {
return {
isValid: false,
message: `Evidence contains undefined predicates: ${undefinedEvidence.join(', ')}. ` +
`Available predicates: ${[...defined].join(', ')}`
};
}
return {
isValid: true,
message: 'Evidence is valid.'
};
}
}
