Блог

Я использую Teyjus для программирования в лямбда-прологе. У меня есть этот простой генератор списков:

 type islist int -> list X -> o.

islist N nil
       :- N >= 0.
islist N (H::T)
       :- N >= 0,
          M is N - 1,
          islist M T.
  

Мне нужно создать предикат, который возвращает список, состоящий из всех списков, сгенерированных islist в пределах определенной границы.

Я думал продолжить цикл, управляемый сбоем. На данный момент я могу печатать только списки, созданные с помощью следующего кода:

 type loop   int -> o.

loop N
     :- islist N L,
        term_to_string L STR,
        print STR,
        print "n",
        fail.
loop _.
  

Что мне нужно, так это собирать эти списки, а не печатать их (поэтому мне нужно что-то вроде понимания списка).
Как я могу это сделать?

Если вы работаете в Prolog, вы можете использовать встроенные операторы setof или bagof для выполнения такой коллекции. Они недоступны в лямбда-прологе. Setof — это естественный вид оператора «более высокого порядка», но теория доказательств, лежащая в основе лямбда-пролога (и его двоюродных братьев по линейной логике), не предусматривает такой функции. Это можно было бы реализовать, например, в Teyjus, но это не было приоритетом.

Для решения проблемы требуется некоторая постоянная память, которая сохраняет свое состояние при сбоях. В Прологе можно использовать базу данных предложений assert / retract. В Teyjus доступно только сохранение файловой системы. Таким образом, печать в файл из цикла, управляемого сбоем, а затем считывание ответов в виде списка, по-видимому, является единственным способом сделать это в текущей реализации Teyjus.

В Прологе (Scryer, SICStus, SWI одинаково):

 ?- numlist(0,4,Ns), maplist(length,Ls,Ns).
   Ns = [0,1,2,3,4], Ls = [[],[_A],[_B,_C],[_D,_E,_F],[_G,_H,_I,_J]].