Search code examples
prologlogic-programmingclojure-core.logicminikanren

Correct use of logic languages as a tool


I'm interested in the "use the right tool for the job" philosophy in programming, and I have a problem I thought might be solvable with logic programming. I mean this in a naive way, because I haven't done any logic programming and am just setting out to learn. But being at the stage where I am still trying to grasp the concepts and vocabulary I was hoping for some expert direction before potentially getting too deep.

What drew me to the idea of using logic programming was my vague knowledge of the idea of "unification," but my thought was to use it in a way that I am not sure is idiomatic or correct. Given two objects (or trees), I want to compare the two for equality via their properties (or leaves), and what I want to return is some notion of "difference"--i.e., given the ways in which these two objects are not different, what changes would have to made in one of them in order for the two to be some notion of equal?

For example let's say I have two objects chair and stool. Supposing that each is comprised of a list of properties or attributes, I'd like to build a system that can return something along the lines of "chair and stool would be equal if stool's legCount were 4 and hasBack were true."

For some reason, semantically I'm imagining this as a sort of remainder, like, chair minus stool equals one leg. Not sure if that's helpful or not...

I can think of some silly ways to do this with imperative code and some more elegant ways to do it using functional techniques, but I had a hunch that logic programming might be particularly suited to this. Any wisdom about which directions to look into would be very much appreciated, thank you!


Solution

  • Possibly you want to look into 'The least general generalisation' or 'anti unification' from the ILP literature:

    Here are some slides: http://soft.vub.ac.be/~cderoove/declarative_programming/decprog7.pdf

    Using the code from simply logical chapter 9 http://people.cs.bris.ac.uk/~flach/SL/SL.pdf:

    :-op(600,xfx,'<-').
    
    anti_unify(Term1,Term2,Term):-
        anti_unify(Term1,Term2,Term,[],S1,[],S2).
    
    anti_unify(Term1,Term2,Term1,S1,S1,S2,S2):-
        Term1 == Term2,!.
    anti_unify(Term1,Term2,V,S1,S1,S2,S2):-
        subs_lookup(S1,S2,Term1,Term2,V),!.
    anti_unify(Term1,Term2,Term,S10,S1,S20,S2):-
        nonvar(Term1),nonvar(Term2),
        functor(Term1,F,N),functor(Term2,F,N),!,
        functor(Term,F,N),
        anti_unify_args(N,Term1,Term2,Term,S10,S1,S20,S2).
    anti_unify(T1,T2,V,S10,[T1<-V|S10],S20,[T2<-V|S20]).
    
    
    
    anti_unify_args(0,Term1,Term2,Term,S1,S1,S2,S2).
    anti_unify_args(N,Term1,Term2,Term,S10,S1,S20,S2):-
        N>0, N1 is N-1,
        arg(N,Term1,Arg1),
        arg(N,Term2,Arg2),
        arg(N,Term,Arg),
        anti_unify(Arg1,Arg2,Arg,S10,S11,S20,S21),
        anti_unify_args(N1,Term1,Term2,Term,S11,S1,S21,S2).
    
    subs_lookup([T1<-V|Subs1],[T2<-V|Subs2],Term1,Term2,V):-
        T1 ==Term1,
        T2 ==Term2,!.
    subs_lookup([S1|Subs1],[S2|Subs2],Term1,Term2,V):-
       subs_lookup(Subs1,Subs2,Term1,Term2,V).
    

    Then you could query:

    ?- anti_unify(object(type=chair,legs=4,hasback=true,color=red),object(type=stool,legs=3,hasback=false,color=red),T,[],S1,[],S2).
    T = object(type=_1838, legs=_1808, hasback=_1778, color=red),
    S1 = [chair<-_1838, 4<-_1808, true<-_1778],
    S2 = [stool<-_1838, 3<-_1808, false<-_1778] .
    

    Which give you the Term which is the least general generalisation of our two objects alongside the substitutions you would make to get the objects back.