Понимание списков в лямбда-прологе

Question

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

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 _.

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

Answer 1

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

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

Answer 2

В Прологе (как 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]].