How to identify valid bodies and convertible terms

Question

is_convertible_term(T) should be true, if T can be converted to a valid body (7.6.2 of ISO/IEC 13211-1). Thus:

?- is_convertible_term((A,B)).
   true.
?- is_convertible_term(A).
   true.
?- is_convertible_term(3.14).
   false.
?- is_convertible_term((a->b;c,!)).
   true.
?- is_convertible_term(\+1).
   true. % because (\+)/1 is a built-in predicate

This should be written in ISO Prolog and it should be as short as possible.

Additionally, is_body(T) should be true, if T is identical to the conversion to a valid body. With the help of it we could for example remove call wrappers (provided there is no interference with !/0 or a top level (->)/2).

?- is_body((a,X)).
   false.
?- is_body((a,call(X))). % this is the conversion of (a,X)
   true.

What I have tried so far, was to start with is_body/1 since it can only be true if is_convertible_term/1 is true. So

is_body(T) :-
   is_convertible_term(T),
   ... .   % <-- here I am stucked

(Just for the sake of completeness, we are considering here ISO Prolog only without any constraint extension, but predicates from the Prolog prologue are fine)

Answer 1

Very short solution.

is_convertible_term(T) :-
    catch((! ; T), error(type_error(callable,_),_), false).

is_body(T) :-
    \+ \+ (
        term_variables(T, Vs),
        append(Vs, _, [0|Vs]),
        is_convertible_term(T)
    ).

Answer 2

Here is my solution after reading an excerpt of 7.6.2 of the standard found in this related question.

is_convertible_term(T):- % I really don't use this procedure /1
  is_convertible_term(T, _).
  
is_convertible_term(T, G) :-
    (   var(T)
    ->  G=call(T)
    ;   member(T-G,
               [ (Arg1, Arg2)-(GArg1, GArg2),
                 (Arg1;Arg2)-(GArg1;GArg2),
                 (Arg1->Arg2)-(GArg1->GArg2),
                 (Arg1*->Arg2)-(GArg1*->GArg2)
               ])
    ->  maplist(is_convertible_term,
                [Arg1, Arg2],
                [GArg1, GArg2])
    ;   callable(T),
        G=T
    ).

is_body(T) :-
   is_convertible_term(T, G),
   T==G.

Sample runs:

?- is_convertible_term((A,B)).
true.

?- is_convertible_term(A).
true.

?- is_convertible_term(3.14).
false.

?- is_convertible_term((a->b;c,!)).
true.

?- is_convertible_term(\+1).
true.

?- is_body((a,X)).
false.

?- is_body((a,call(X))).
true.

?- is_convertible_term((a->B;c,!), G).
G = (a->call(B);c, !).

Answer 3

This solution counts the number of variable that needs substitution:

is_convertible_term(T) :-
    vcount(T, 0, _).

is_body(T) :-
    vcount(T, 0, 0).

vcount(T, S0, S) :-
    var(T), !,
    succ(S0, S).
vcount(T, S0, S) :-
    T =.. [N,T0,T1],
    member(N, [',',;,->]), !,
    vcount(T0, S0, S1),
    vcount(T1, S1, S).
vcount(T, S, S) :-
    functor(T, N, _),
    atom(N).

Answer 4

An alternative solution:

is_convertible_term(T) :-
    var(T), !.
is_convertible_term(T) :-
    T =.. [N,T0,T1],
    member(N, [',',;,->]), !,
    is_convertible_term(T0),
    is_convertible_term(T1).
is_convertible_term(T) :-
    functor(T, N, _),
    atom(N).

is_body(T) :-
    \+ \+ (
        term_variables(T, Vs),
        maplist(=(0), Vs),
        is_convertible_term(T)
    ).

Answer 5

Slightly smaller and faster:

is_convertible_term(T) :-
    var(T), !.
is_convertible_term(T) :-
    member(T, [(T0,T1),(T0;T1),(T0->T1)]), !,
    is_convertible_term(T0),
    is_convertible_term(T1).
is_convertible_term(T) :-
    callable(T).

is_body(T) :-
    \+ \+ (
        term_variables(T, Vs),
        append(Vs, [0], [_|Vs]),
        is_convertible_term(T)
    ).

Answer 6

One more definition:

:- dynamic('$body'/1).

is_convertible_term(T) :-
    catch(asserta(('$body'(T) :- T)), error(type_error(callable,_),_), false),
    retract(('$body'(T) :- _)), !.

% Alternative.
% is_body(T) :-
%     catch(asserta(('$body'(T) :- T)), error(type_error(callable,_),_), false),
%     clause('$body'(T), U),
%     retract(('$body'(T) :- U)), !,
%     T == U.
is_body(T) :-
    \+ \+ (
        term_variables(T, Vs),
        append(Vs, _, [0|Vs]),
        is_convertible_term(T)
    ).