Овеществленный call_with_time_limit / call_with_inference_limit

Я пытаюсь определить отношение callto_status(Goal, Status), которое всегда завершается успешно и объединяет Status в соответствии с результатом вызова Goal (другими словами, я хотел бы реализовать овеществленную версию call_with_inference_limit/3). В моей реализации используется SWI call_with_inference_limit/3, который имеет тот же интерфейс, что и call_with_time_limit/3 (что должно заставить его работать и в этом случае). Реализация call_with_..._limit не отступает, поэтому я подумал, что лучше не создавать впечатление сообщения о замене ответа на цель.

Я ввел вспомогательный предикат derivable_st для удобства чтения. Он обрабатывает случай успеха и тайм-аута, но в противном случае терпит неудачу.

% if Goal succeeds, succeed with Status = true,
% if Goal times out, succeed with Status = timeout
% if Goal fails, fail
derivable_st(Goal, Status) :-
    T = 10000,                               % set inference limit
%    copy_term(Goal, G),                    % work on a copy of Goal, we don't want to report an answer substitution
    call_with_inference_limit(G, T, R),     % actual call to set inference limit
    (  R == !
    -> Status = true                        % succeed deterministically, status = true
    ;  R == true
    -> Status = true                        % succeed non-deterministically, status = true
    ;  (  R == inference_limit_exceeded     % timeout
       -> (
              !,                            % make sure we do not backtrack after timeout
              Status = timeout              % status = timeout
          )
       ;  throw(unhandled_case)             % this should never happen
       )
    ).

Основной предикат охватывает derivable_st и обрабатывает случай сбоя и возможные исключения (если они есть). Мы могли бы захотеть выделить переполнения стека (которые случаются в случае слишком высоких пределов вывода), но сейчас мы просто сообщаем о любых исключениях.

% if Goal succeeds, succeed with Status = true,
% if Goal times out, succeed with Status = timeout
% if Goal fails, succeed with Status = false
% if Goal throws an error, succeed with Status = exception(The_Exception)
% Goal must be sufficiently instantiated for call(Goal) but will stay unchanged
callto_status(Goal, Status) :-
    catch((  derivable_st(Goal, S)            % try to derive Goal
          -> Status = S                       % in case of success / timeout, pass status on
          ;  Status = false                   % in case of failure, pass failure status on, but succeed
          ),
          Exception,
          Status = exception(Exception)       % wrap the exception into a status term
    ).

Предикат работает для некоторых простых тестов:

?- callto_reif( length(N,X), Status).
Status = true.

?- callto_reif( false, Status).
Status = false.

?- callto_reif( (length(N,X), false), Status).
Status = timeout.

Теперь мой вопрос немного расплывчатый: делает ли этот предикат то, что я заявляю? Видите ли вы какие-либо ошибки/точки улучшения? Я благодарен за любой вклад!

Изменить: как было предложено @false, закомментировано copy_term/2


prolog meta-predicate
person lambda.xy.x    schedule 13.02.2019    source источник
comment
Почему copy_term/2? Проблемы с ограничениями впереди   -  person false    schedule 13.02.2019
comment
Я хотел сохранить предикат как можно более чистым — если я удалю copy_term/2, первый запрос будет успешным с L=[], N=0, Status=true в качестве единственного решения, что вводит в заблуждение.   -  person lambda.xy.x    schedule 14.02.2019
comment
к вашему сведению   -  person false    schedule 01.10.2019

Ответы (1)


arrow_upward
1
arrow_downward

Это более короткое решение:

callto_status(Goal, Status) :-
    call_with_inference_limit(Goal, 10000, Status0),
    (Status0 = ! -> !, Status = true; Status = Status0).
callto_status(_, false).

Вот видите, как полезен оригинал! статус, чтобы избежать ненужной точки выбора:

?- callto_status(member(X,[1,2,3]), Y).
X = 1,
Y = true 
X = 2,
Y = true 
X = 3,
Y = true.

?- callto_status(fail, Y).
Y = false.

Конечно, вы также можете заменить Status0 = ! -> !, Status = true только на Status0 = ! -> Status = true. Тогда вы всегда будете получать оставшуюся точку выбора:

?- callto_status(member(X,[1,2,3]), Y).
X = 1,
Y = true 
X = 2,
Y = true 
X = 3,
Y = true 
Y = false.

Из вопроса непонятно, чего именно вы хотите.

person Mostowski Collapse    schedule 27.07.2019
comment
Спасибо, это решение довольно интересное, но разве я не получу Status = false, если решение для последней цели недетерминировано? Например, callto(member(1,[1,1,3]), false). завершится успешно, но очевидно, что запрос имеет результат. - person lambda.xy.x; 27.07.2019
comment
Возможно, для уточнения: callto_status(G,S) следует унифицировать S с true, если G имеет решения, унифицировать с false, если оно не является выводным, и унифицировать с timeout, если ни одно из них не может быть показано в течение T шагов. Предикат также должен иметь возможность возвращаться к решениям G, но оставляя S нетронутым. - person lambda.xy.x; 27.07.2019