Use of Julog to parse first order formulas in usual binary logic

[gilles-paul]

Use of Julog to parse first order formulas in usual binary logic

[gilles-paul]

Following your useful instructions I was able to parse some simple expressions such as : "A" (variable) "F" constant, any of these between parentheses even nested like (A) or ((A)).
Negations are also recognized "!A" is parsed and of course (!A) or (!(A)) or !!A !(!A) etc...
When it comes to write the rule for my first binary connector '&' i'm stuck. I don't know how to write the correct rule in the clauses.
I think it can be useful to list the possible pairs of arguments, success would be that one of these pairs is a pair of terms recognized as formulas. I wrote a usual function to do that
Here's my code

using Julog

varP(X) = length(X) == 1 && X[1] in "ABCDEGHIJKLMNOPQRSTUWXYZ"
#test de parenthèsage
inparP(f) = f[1] == '(' && f[length(f)] == ')'
#ramène l'expression entre parenthèses
betweenpar(f) = f[2:length(f)-1]
#symbole de négation en tête
negation(f) = f[1]=='!'
# ce qui suit le symbole !
queue(f)=f[2:end]
# list of possible pairs of arguments for & connector
# can be empty at first pass even if connector & detected
candidates_and(f)=[(f[1:i-1],f[i+1:end]) for i in 2:length(f)-1 if f[i]=='&']


clauses = @julog [
    constante("V") <<= true,
    constante("F") <<= true,
    variable(X) <<= varP(X),
    formule(X) <<= constante(X),
    formule(X) <<= variable(X),
    formule(X) <<= inparP(X) & formule(betweenpar(X)),
    formule(X) <<= negation(X) & formule(queue(X)),
    #clause for ninary operator &
    #formule(X) <<= ???????
 ]

query = @julog formule("X&Y") # Of course fails because no clause for this case
sat, subst = resolve(query, clauses, funcs=Dict(:varP => varP, :inparP =>inparP, :betweenpar => betweenpar,
:negation => negation, :queue => queue,  :candidates_and =>candidates_and))

println(sat)
println(subst)

[gilles-paul]

I worked a little on the subject this morning. I guess that the problem is connected with my definition of the variables. Although the number of possibilities is finite, it seems that Julog doesn't know and does not systematically test all possibilities.
So I restricted the variables to only three possibilities, says A, B and C for test.
Actually about atomic formulas we only have the two constants 'V' and 'F and the three variables 'A', 'B' and 'C' which are declared one by one separately. Now my test will be "Is X of the form one formula + symbol & + another formula.
For a lookup with atomic solutions it should not be more than 25 trials ...

using Julog

inparP(f) = f[1] == '(' && f[length(f)] == ')'
#ramène l'expression entre parenthèses
betweenpar(f) = f[2:length(f)-1]
#symbole de négation en tête
negation(f) = f[1]=='!'
# ce qui suit le symbole !
queue(f)=f[2:end]
# test de conjonction
conj(X,Y,Z)= X==string(Y,"&",Z)

clauses = @julog [
    constante("V") <<= true,
    constante("F") <<= true,
    variable("A") <<= true,
    variable("B") <<= true,
    variable("C") <<= true,
    formule(X) <<= constante(X),
    formule(X) <<= variable(X),
    formule(X) <<= inparP(X) & formule(betweenpar(X)),
    formule(X) <<= negation(X) & formule(queue(X)),
    #clause for binary operator &
    formule(X) <<= formule(Y) & formule(Z) & conj(X,Y,Z),
 ]

query = @julog formule("A&B") 
sat, subst = resolve(query, clauses, funcs=Dict(:conj => conj, :inparP => inparP, :betweenpar => betweenpar,
:negation => negation, :queue => queue))

println(sat)
println(subst)

`Although this code compiles without any error it runs indefinitely without stopping .
Can you explain ?
Thank you``

[ztangent]

My guess is that the following rule is causing infinite loops:

    formule(X) <<= formule(Y) & formule(Z) & conj(X,Y,Z),

If you instead rewrite it as:

    formule(X) <<= conj(X, Y, Z) & formule(Y) & formule(Z)

Then Julog will try to prove conj first instead of repeatedly trying to prove formule in a depth-first-search.

This is a general issue when writing Prolog-style programs, see this link for another example!

[ztangent]

Also, you might be able to express the list of all variables more concisely using a Prolog-style list. So instead of having:

    variable("A") <<= true,
    variable("B") <<= true,
    variable("C") <<= true,

You could instead add the clauses:

    member(X, [X | Y]) <<= true,
    member(X, [Y | YS]) <<= member(X, YS),
    variable(X) <<= member(X, ["A", "B", "C"]),

[gilles-paul]

If you instead rewrite it as:

formule(X) <<= conj(X, Y, Z) & formule(Y) & formule(Z)

I tried. This time no looping but answer 'false' ??? for simple query with "A&B" as a would-be formula.
Now I tried alone :
query = @julog formule(Y)
which finds the 5 possible solutions (2 constants and three variables
But if I want to find all possible couples of formulas
I tried something like
query = @julog formule(Y) & formule(Z)
which is not accepted by the compilatior (wrong syntax for query).
So how to write the query for the 25 solutions of the product ?
I noted your suggestion to declare variables and I will do it in the final version, if I can pass this step of the '&' (and the '|' which will be very similar).

[gilles-paul]

Answer to my last question found

clauses = @julog [
    constante("V") <<= true,
    constante("F") <<= true,
    variable("A") <<= true,
    variable("B") <<= true,
    variable("C") <<= true,
    #variable(X) <<= varP(X),
    formule(X) <<= constante(X),
    formule(X) <<= variable(X),
    formule(X) <<= inparP(X) & formule(betweenpar(X)),
    formule(X) <<= negation(X) & formule(queue(X)),
    formules(X,Y) <<= formule(X) & formule(Y),
 ]

query = @julog formules(Y,Z)
sat, subst = resolve(query, clauses, funcs=Dict(:conj => conj, :inparP => inparP, :betweenpar => betweenpar,
:negation => negation, :queue => queue))

BUT doesn't solve the '&' problem
clauses like formule(X) <<= formules(Y,Z) & conj(X,Y,Z) (or reverse order) both accepted but either looping or answer 'false' for "A&B".

[gilles-paul]

It seems to me that the problem is about the recursivity of the definition of 'formule'. In the two preceding cases, I mean negation and grouping by parentheses, the recursivity was 'terminal' (AKA tail recursivity) so not real recursivity..
If I change the code for this introducing new predicate 'conjonction' it works, but if I add later something that a formule can be a conjonction, (indirect but real recursivity) behaviour is the same : false answer or looping .

clauses = @julog [
    constante("V") <<= true,
    constante("F") <<= true,
    variable("A") <<= true,
    variable("B") <<= true,
    variable("C") <<= true,
    #variable(X) <<= varP(X),
    formule(X) <<= constante(X),
    formule(X) <<= variable(X),
    formule(X) <<= inparP(X) & formule(betweenpar(X)),
    formule(X) <<= negation(X) & formule(queue(X)),
    formules(X,Y) <<= formule(X) & formule(Y),
    conjonction(X)<<= formules(Y,Z) & conj(X,Y,Z),
 ]

query = @julog conjonction("A&B")
sat, subst = resolve(query, clauses, funcs=Dict(:conj => conj, :inparP => inparP, :betweenpar => betweenpar,
:negation => negation, :queue => queue))

[ztangent]

So here's my guess as to why it's returning false: You have to be careful when using custom Julia functions, because they lead to weird behavior when they operate on variables which are still not bound. In particular, I think that your conjunction check:

# test de conjonction
conj(X,Y,Z)= X==string(Y,"&",Z)

is actually returning false when the variables Y and Z are not yet bound. To get around this, you might want to rewrite your program to use as much pure Julog / Prolog as possible --- i.e., avoiding the use of custom functions, represent strings as Julog style lists of characters, and use Prolog-style list functions to manipulate them.

[gilles-paul]

Your guess is correct
query = @julog conj("A&B",Y,Z)
doesn't find the only one evident solution...
But amazingly 'conjonction' as above works ???
I will come back to this later.
But maybe better to forbid at all the use of 'custom' functions leading to such situations. Debugging prolog style programs is not so simple.
When I find time I will rebuild all according your suggestions. By the way as an ex-Lisper during the full 80's decade I am familiar with 'Content of A Register, and so on, CADDR, CADAR and all the family).I would say it's more Lisp style than Prolog style.
Thanks for your answer.

[gilles-paul]

Excuse me I posted this comment the wrong place. it should be here.
I want to restart everything all over from scratch !
OK I tried

using Julog
clauses = @julog [
    constante(V) <<= true,
    constante(F) <<= true
 ]
#println(conj("A&B","A","B"))
query = @julog constante(X)
sat, subst = resolve(query, clauses )
println(sat)
println(subst)

Answer

true
Any[{X => #2}, {X => #3}]

what do these #2 and #3 stand for ?
I’m completely lost !

[gilles-paul]

using Julog
clauses = @julog [
   member(X, [X | Y]) <<= true,
   member(X, [Y | Z]) <<= member(X, Z),
   constante(X)<<= member(X,["V","F"]),
    variable(X) <<= member(X, ["A", "B", "C"]),
    formule(X)<<=constante(X),
    formule(X)<<= variable(X),
]

query = @julog formule(X)
sat, subst = resolve(query, clauses )
println(sat)
println(subst)

This (your suggestion) works to define constants and variables as strings. But if I want to define them as chars, by replacing everywhere double quotes by single ones, it doesn't work, why ?
The idea to describe the 'final' elements (leaves of the tree) as characters would be useful in the case I decide to abandon the string representation for the list representation writing [!, A] for the negation of the variable A. Why not ? But as I understood the Lisp primitives are not available in the clauses, and the 'infix' notation difficult to detect and translate.
Such beginning suggests that formulas, all of them, will be tested as Julia strings. So a negation (for example) will be a string beginning with the special character '!' and with tail a formula .. But how to access these ? Using usual Julia syntax, X[1] X[2:end] inside julog clauses,is refused.It worked with my 'custom function' but how to get rid of that (they are causing the trouble, aren't they ?. the notation [X|Y] applies to lists not to strings.
I'm completely confused, and blocked in every direction.
As I showed you my procedural 'parseP' does the job and for the same price returns a tree ready for evaluation. I expected the julog-prolog to be even simpler, the clauses describing the context-free grammar of the simple formulas in a form very similar to BNF. The only 'magic' would in this case reside in the 'using Julog' directive and the final query.
So I think it's better for me to give up now.
Thank you in any case for your help.
Regards.
Gilles

[ztangent]

Apologies for not replying to this until almost a year later! I think I didn't fully understand your last comment when I first read it, and I still don't quite understand it now.

FWIW, I'm quite sure that you can write a parser for the language you want in Julog, it just won't be very efficient or natural to do -- the way I would probably do it is first convert a Julia string to a (Julia) list of Chars, and then use the to_const_list helper function to convert the Julia list to a Julog list:

Julog.jl/src/utils.jl

Lines 126 to 128 in 01367bc

	"Convert a vector of Julia objects to a Julog list of constants."
	to_const_list(v::Vector) =
	foldr((i, j) -> Compound(:cons, [Const(i), j]), v; init=Compound(:cend, []))

By providing that as a query, you can probably use something like the clauses you've already written to parse the input!

If you're looking for other approaches to parsing first-order formulas in Julia, you might want to check out ParserCombinator.jl -- it's probably faster since it's specialized for parsing specifically.

I'll be marking this as closed unless it turns out there's anything here related to a bug in Julog -- thanks for your interest!