Parsing for equivalence rules?

[CrashBurnRepeat]

I'm trying to recreate in Julog Prolog statements like:

sister(X,Y):-
  parent(Z,X),
  parent(Z,Y),
  female(X),
  X\=Y.

The last term is required or else people can be their own sisters. My initial thought was to translate the last term as X!=Y and the expression was parsed without error, but returned incorrect results (saying that an individual did not have a sister when they did).

My solution has been to use not(unifies(X,Y)) but this seems a little verbose and I'm not sure it's truly equivalent to what I'm looking for. Can the != syntax be implemented without breaking the package, or is using unifies the recommended approach? If != is not the intended approach, can the failure be made more apparent (a throw perhaps?)

[CrashBurnRepeat]

@ztangent it also seems that not(X==Y) is probably the better solution? My apologies if I'm missing something simple 😅

[ztangent]

not(unifies(X, Y)) is the right approach here, and you can also do not(X ≐ Y) or !(X ≐ Y) if you're okay with using Unicode symbols. An example similar to yours is in one of the test scripts:

https://github.com/ztangent/Julog.jl/blob/9f0545d9e6de720fc8e732d3e959fcac419b7318/test/builtins.jl#L19-L29

== and != are used to compare constants (e.g. numbers), and are equivalent to =:= and =\= respectively in SWI-Prolog. Unfortunately Julia doesn't support adding new comparison operators like the ones used by Prolog, so I ended up deciding it'd be better to preserve the standard Julia meaning of == (i.e. exact equality), rather than having it mean unify.

[CrashBurnRepeat]

@ztangent Thanks for the explanation, that's really helpful!

I would still ask though why == still seems to work for this case. For instance, taking the test you referenced and converting not(unifies(A,B)) to not(A==B) still satisfies the test. Should it be able to? If not, should there be some sort of error thrown at parse time?

[ztangent]

Welcome! And yes, == happens to work in the test case because == would directly compare the values of the Julog constants hera and hera (or hera and zeus) which happens to return the same results as unifies(hera, hera) or unifies(hera, zeus). However, something like A == hera will return false if the variable A has not already been bound to hera by that point in the proof search, whereas unifies(A, hera) will succeed if A has not yet been bound (indeed, it will succeed, and then bind A to the value hera). And this will lead to different behavior in a number of cases.

[CrashBurnRepeat]

In that case, shouldn't A==B and A!=B throw a parsing error since it's declaratively incorrect and can lead to hard to diagnose errors? Or is there ever a case where this is declaratively correct?

[ztangent]

I'm confused by what you mean by 'declaratively correct' here -- '==' is useful because sometimes you do want to compare two numbers. This is maybe not the best example because you could write it in a different way, but: equal_modulo(A, B, C) <<= is(P, mod(A, C)) & is(Q, mod(B, C)) & P == Q is a valid clause that you might write if you wanted a predicate that says A and B have the same remainder modulo C.

[CrashBurnRepeat]

Ah, my apologies, I'm currently learning logical programming and so there are still nuances and terminology I'm working out 😅

I'm pretty sure I understand the distinction the modulo example is making, so I'd be happy to close the issue. In the future, would it be better just to message you directly rather than raise issues? I'm happy to provide my "novice's perspective" if that's something you'd find useful in testing out the package and the documentation.

[ztangent]

Feel free to continue raising issues! This was helpful to know -- hopefully people who face similar issues can find this issue. I'll also be clarifying the semantics of operators like == in the README when I next get the chance.

[CrashBurnRepeat]

Great, sounds good 👍 I'll do my best to ask good questions in the future.