Предложения в (лямбда)прологе, начинающиеся с разреза
Я читаю статью « Реализация теории типов в программировании логики с ограничениями высшего порядка », и на p7 я вижу следующий код лямбда-пролога:
% KAM-like rules in CPS style
whd1 (app M N) S Ks Kf :- !, Ks [] M [N|S].
whd1 (lam T F1) [N|NS] Ks Kf :- !, pi x \ val x T N NF => Ks [x] (F1 x) NS.
whd1 X S Ks Kf :- !, val X _ N NF, if (var NF) (whd_unwind N NF), Ks [] NF S.
whd1 X S Ks Kf :- Kf.
Меня смущает положение разреза
!в третьем пункте. Мое понимание сокращения состоит в том, что оно всегда завершается успешно, но предотвращает возврат после этого успеха и, в частности, приводит к игнорированию последующих предложений для одного и того же предиката. В частности, отсечение, которое идет первым в предложении, должно означать, что как только объединение заголовка с этим предложением будет успешным, все последующие предложения будут игнорироваться.
Имея это в виду, сокращения, которые начинаются с первого и второго предложений выше, имеют для меня смысл: они говорят, что если сокращаемый термин является
appили
lam, то к нему может применяться только одно правило. Но мне кажется, что заголовок третьего предложения является полностью общим — все аргументы являются отдельными переменными — поэтому он не может не унифицировать. Поэтому мне кажется, что разрез, с которого начинается третье предложение, всегда будет вызываться, и, следовательно, четвертое предложение никогда не будет достигнуто. Я ожидал, что третье предложение будет написано примерно так
whd1 X S Ks Kf :- val X _ N NF, !, if (var NF) (whd_unwind N NF), Ks [] NF S.
чтобы это применялось только к тому, что они называют «переменными, привязанными к val»; тогда разрез будет указывать, что если это такая переменная, применяется только это предложение, а если
Xне такая переменная, то мы могли бы вернуться и попробовать четвертое предложение.
Тем не менее, мое понимание вырезания очень зачаточное, поэтому я ожидаю, что что-то упускаю. Может кто-нибудь объяснить?