Pure JS implementation of syntactic first-order unification (See: https://en.wikipedia.org/wiki/Unification_(computer_science))

unify.js

const assert = require('assert');
const _ = require('lodash');

const {is_identifier, is_variable, merge_identifiers, string_to_units} = require('./identifiers');

const {term_to_string} = require('./display');




const merge_equiv_set = (set, sets) => {
    

    const s = sets.find(s => !empty(intersect(set, s)));


    if(!s) {

        sets.push(unique(set));

        return saturate_equiv_set(set, sets);

    } 


    if(!empty(difference(set, s))) {

        union_in_place(s, set);

        return saturate_equiv_set(s, sets);

    }


    return sets;

};




const saturate_equiv_set = (set, sets = [set]) => {

    const arrays = set.filter(is_array);

    return equal_length(arrays) && _.zip(...arrays).every(arr => merge_equiv_set(arr, sets)) && sets;

};


const generate_substitution_singular = set => {


    // here, we can choose an arbitrary non-identifier

    const unioned = set.find(s => !is_identifier(s)) || merge_identifiers(set);

    const o = {};

    set.filter(is_identifier).forEach(id => o[id] = unioned);

    return o;

};  


const generate_substitution = sets => 

    _.assign(...sets.map(generate_substitution_singular));



const saturate_substitution = sub => {

    for(let k of Object.keys(sub)) {

        sub = _.mapValues(sub, v => apply_substitution(v, {[k]: sub[k]}));

    }

    return sub;

};
 
const apply_substitution = (term, substitution) =>

    is_identifier(term) ?
        (substitution[term] || term) : 
        term.map(t => apply_substitution(t, substitution));




const occurs_check_singular = ([k, v]) => k !== v && recursive_includes(v, k);

const recursive_includes = (arr, v) => Array.isArray(arr) ? arr.some(a => recursive_includes(a, v)) : arr === v;

const occurs_check = sub => !Object.entries(sub).some(occurs_check_singular) && sub;



const conflict_check = sub => 

    !Object.values(sub).some(has_multiple_consts) && !Object.entries(sub).some(const_assigned_to_term) && sub;



const has_multiple_consts = term => is_identifier(term) && string_to_units(term).filter(v => !is_variable(v)).length > 1;

const const_assigned_to_term = ([k, v]) =>

    string_to_units(k).find(u => !is_variable(u)) && !is_identifier(v);






const skip_debug = true;

const debug_print = f => skip_debug ? f : (...args) => {

    console.log('unify');

    console.log('\t', args.map(term_to_string));



    const o = f(...args);

    console.log(o);

    return o;

};



const unify = debug_print((...terms) => 

    // saturate_equiv_set, occurs_check, and conflict_check can return false

    // if one of them returns false, we want the whole composition to return false

    // functions run top-down


    compose_maybe(
        [
            saturate_equiv_set, 
            generate_substitution, 
            saturate_substitution, 
            occurs_check,
            conflict_check
        ], 
        terms
    )

);



const compose_maybe = (fns, x) => fns.reduce((v, fn) => v && fn(v), x);






module.exports = {
    unify
};





const call = (f, ...x) => {

    const o = f(...x);
    console.log(x, '=>', o);
    return o;

}



// Mocha unit tests

it.skip('saturate equiv set', () => {  

    call(saturate_equiv_set, ['[:x]', '[:y]', ['f', '[:x]'], ['f', '[:y]']]);

    call(saturate_equiv_set, [['f', '[:x]'], ['f', '[:y]']]);

    call(saturate_equiv_set, [['[:x]', ['S', '[:x]']], [['S', '[:y]'], '[:y]']]);

    call(saturate_equiv_set, [['[:a]', '[:a]'], [['[:b]', '[:b]'], [['[:c]', '[:c]'], ['[:n]', '[:m]']]]]);

});


it.skip('full unification', () => {  

    call(unify, '[:x]', '[:y]', ['f', '[:x]'], ['f', '[:y]']);

    call(unify, ['f', '[:x]'], ['f', '[:y]']);

    call(unify, ['[:x]', ['S', '[:x]']], [['S', '[:y]'], '[:y]']);

    call(unify, ['[:a]', '[:a]'], [['[:b]', '[:b]'], [['[:c]', '[:c]'], ['[:n]', '[:m]']]]);

    call(unify, [ 'f', '[:x]' ], [ 'f', "[:x']" ]);

    call(unify, [ 'f', '[:x]' ], 'c');

});



const empty = arr => arr.length === 0;

const intersect = (...arrs) => _.intersectionWith(...arrs, _.isEqual);
    
const difference = (a, b) => _.differenceWith(a, b, _.isEqual);

const union_in_place = (...arrs) => replace(arrs[0], _.unionWith(...arrs, _.isEqual));

const replace = (a, b) => a.splice(0, a.length, ...b) && a;

const unique = arr => _.uniqWith(arr, _.isEqual);

const equal_length = arrs => arrs.every(arr => arr.length === arrs[0].length);

const is_array = term => !is_identifier(term);