Representation and generation of terms

[rzach]

So for the interactive mode (issue #14 ) I need to represent formulas of a logic in some way that allows me to do the following:

• If F is a formula, find an assignment of values to the variables in it that makes it take a certain value (or check if a given assignment has a certain value, or find the value for a given assignment).
• If F is a formula, determine if it is a tautology.
• Test if F is a legal formula of a given logic, and generate via backtracking all formulas of that logic.

I started by representing formulas as Prolog terms, with variables being Prolog variables. Then I can do things like isValue(and(neg(X),X), t) to find the values for X where ~X & X is true. But I'm running into trouble when trying to generate all formulas. Prolog's depth-first search on backtracking is a problem, but also the fact that logical variables = Prolog variables. Is there a way to define isFormula(X) so that on backtracking X will take values, e.g., X, neg(X), and(X,X), and(X,Y), and(neg(X),X), etc? Or is the thing to do to make formulas be represented as ground terms of some form (e.g., representing variables as numbers or var(n) or something? Then finding or testing for values is harder -- you'd have to explicitly represent assignments (say as a list [1-t, 2-f]). But a breadth-first search/generation of formulas is easier, perhaps.

There is an efficiency hurdle I can already see: if we want to generate formulas breadth first, we probably have to do it by limiting the depth or length of the term and at the same time limiting the indices of the variables we allow. And we should do this in such a way that as the size of the formula increases we don't re-generate formulas we already considered.

[gsalzer]

I think the problem may rather be the number of terms growing exponentially with depth. Below is a sample code that will generate all terms of a certain depth for the operators specified by isOp(Function,Arity). isTerm(N, T, Vs) will generate all terms of depth N, with Vs being the variables occurring in T. By partitioning Vs and unifying the variables in each partition you can generate different versions of T differing in which leafs contain identical variables. You could also remove the Vs arguments and collect the variables afterwards by traversing T.

findall(T, isTerm(I,T,Vs), Ts), length(Ts,N) yields: I=0: N=2 I=1: N=6 I=2: N=66 I=3: N=5478 I=4: Stack limit (1.0Gb) exceeded

isOp(c,0).
isOp(f,1).
isOp(g,2).

% T is a term of depth N, with variables Vs.
isTerm(N, T, Vs) :-
    length(D, N),
    isTermEq(D, T, Vs, []).

% isTermEq(D, T, Vs, Vs0)
% T is a term of depth length(D), with variables Vs-Vs0
isTermEq([], T, [T|Vs], Vs) :-
    var(T).
isTermEq([], T, Vs, Vs) :-
    isOp(T,0).
isTermEq([_|D], T, Vs, Vs0) :-
    isOp(F, N), N > 0,
    functor(T, F, N),
    T =.. [_|Ts],
    isTermEq_l(D, Ts, Vs, Vs0).

% isTermEq_l(D, Ts, Vs, Vs0)
% Ts is a list of terms, where at least one has depth length(D),
% with variables Vs-Vs0
isTermEq_l(D, [T|Ts], Vs, Vs0) :-
    isTermEq(D, T, Vs, Vs1),
    isTermLe_l(D, Ts, Vs1, Vs0).
isTermEq_l(D, [T|Ts], Vs, Vs0) :-
    D = [_|D1],
    isTermLe(D1, T, Vs, Vs1),
    isTermEq_l(D, Ts, Vs1, Vs0).

% isTermLe(D, T, Vs, Vs0)
% T is a term with signature FNs of depth length(D) or less,
% with variables Vs-Vs0
isTermLe(_D, T, [T|Vs], Vs) :-
    var(T).
isTermLe(_D, T, Vs, Vs) :-
    isOp(T,0).
isTermLe([_|D], T, Vs, Vs0) :-
    isOp(F, N), N > 0,
    functor(T, F, N),
    T =.. [_|Ts],
    isTermLe_l(D, Ts, Vs, Vs0).

% Ts is a list of terms with signature FNs of depth length(D) or less,
% with variables Vs-Vs0
isTermLe_l(_D, [], Vs, Vs).
isTermLe_l(D, [T|Ts], Vs, Vs0) :-
    isTermLe(D, T, Vs, Vs1),
    isTermLe_l(D, Ts, Vs1, Vs0).

[rzach]

Ah cool, thanks. So you think the way to go is to make Prolog variables be propositional variables rather than introduce special atoms or ground terms v-n and then do everything semantical with assignments? (Thinking of potentially making this work with multseq where variables are atoms a, b, c, ...).

[gsalzer]

So you think the way to go is to make Prolog variables be propositional variables rather than introduce ...

I'm not sure about that. I had this decisions several times, and in the beginning, it seems elegant to use Prolog variables, but it has some drawbacks, as you cannot distinguish easily between variables on the Prolog and logic level. I think I remember a colleague, whom I consider to be the Prolog expert at TUW, advocating to use special terms to represent variables on the object level, and not to use Prolog variables.

[rzach]

Alright if Uli (?) says so then let's do that. I made an attempt in the interactive branch yesterday. Could use what you did to generate not actual formulas but "skeletons" and then take a formula to be something where each (Prolog) variable is a member of [v-1,v2,..length(Vs)]?

[gsalzer]

Yes, Uli ...

[rzach]

(I coded something that generates all formulas of length (not depth) N which worked but gave a "not sufficiently instantiated" error after it got all of them. Can your thing be changed to generate by length not depth so it explodes later?)

[gsalzer]

In isTerm, in the lines for variables and constant, you can adjust whether variables and constants contribute to the length of a term. The code below assigns the length 1 to both types of terms. If you replace [_|S], S by S, S, then the length will be taken to be 0.

isOp(c,0).
isOp(f,1).
isOp(g,2).

% T is a term of size N, with variables Vs.
isTerm(T, N, Vs) :-
    length(S, N),
    isTerm(T, S, [], Vs, []).

% isTerm(T, S, S0, Vs, Vs0)
% T is a term of size S-S0, with variables Vs-Vs0
isTerm(T, [_|S], S, [T|Vs], Vs) :-
    var(T).
isTerm(T, [_|S], S0, Vs, Vs0) :-
    isOp(F, N),
    functor(T, F, N),
    T =.. [_|Ts],
    isTerm_l(Ts, S, S0, Vs, Vs0).

% isTerm_l(Ts, S, S0, Vs, Vs0)
% Ts is a list of terms with total size S-S0 and variables Vs-Vs0
isTerm_l([], S, S, Vs, Vs).
isTerm_l([T|Ts], S, S0, Vs, Vs0) :-
    isTerm(T, S, S1, Vs, Vs1),
    isTerm_l(Ts, S1, S0, Vs1, Vs0).

[rzach]

Awesome; I've included this in ml_interactive and it works well to generate all formulas of a logic by length.