В программировании на логику, что такое ненест? - PullRequest
0 голосов
/ 17 ноября 2018

вопрос

Reasoned Schemer описывает, как использовать miniKanren, который похож на Prolog, но является библиотекой для Lisp-подобных языков. Книга «Первая заповедь» такова:

Для преобразования функции, значение которой является логическим в функцию, значение которой является целью, заменить cond с conde и unnest каждый вопрос и ответ Снимите ответ #t (или #f), заменив его на #s (или #u).

Они на самом деле не определяют unnesting, кроме как через несколько примерно эквивалентных примеров. Самым ясным является следующее: unnesting переносит вас от (list? (cdr l)) до

(fresh (d)
       (cdro l d)
       (listo d))

Я не понимаю, зачем нужно дурачиться. Например, для вышеуказанной цели, почему не достаточно tp написать (listo (cdr l))?

[1] Моя настройка мини-канрена в Racket

Как описано здесь , я запустил raco pkg install minikanren и затем определил несколько пропущенных кусочков.

[2] Некоторые определения функций вам могут не понадобиться

Вот определения listo и все, что он использует, за исключением вещей, определенных в библиотеке minikanren или в прелюдии Ракета.

(define listo
  (lambda (l)
    (conde
     ((nullo l) #s)
     ((pairo l)
      (fresh (d)
             (cdro l d)
             (listo d)))
     (else #u))))

(define nullo
  (lambda (x)
    (== x '())))

(define pairo
  (lambda (p)
    (fresh (a d)
           (conso a d p))))

(define cdro
  (lambda (p d)
    (fresh (a)
           (== (cons a d) p))))

(define conso
  (lambda (head tail result)
    (== (cons head tail) result)))

Ответы [ 3 ]

0 голосов
/ 19 ноября 2018

Отказ от ответственности, я не знаю схемы, и я нахожусь в 1/5 в этой книге.

Я думаю, что это необходимо, потому что функция, которую вы заменяете, часто имеет входную четность (количество принятых аргументов)ниже того, которым вы заменяете его.Вы что-то вроде рефакторинга функции, чтобы поместить выходные данные в переменную, которую вы передаете в нее, вместо того, чтобы возвращать ее как выходные данные.Почему вам нужно заменить каждую функцию логическим эквивалентом?Я не совсем уверен,

(Изменить Я прочитал контекст вашего примера больше ...), если мы возьмем пример, который вы привели, стандартная версия вызвала бы ошибку, если бы я передала не список, я думаю, который отличается от возврата отказа.Таким образом, если вы передаете что-то, что не является списком, вместо получения () из своего запуска, вы создаете исключение, которое отличается.Я понял еще одно отличие, и более важное.Ваш пример взят из определения listo, и listo не просто проверяет, может ли что-то быть списком.он может быть использован для создания бесконечного списка, если задана несвязанная переменная.Это происходит потому, что первый первый элемент в conde будет успешным, поэтому вы получите ().После того, как pairo l преуспеет в создании первого элемента (reified_1), а второй элемент возвращается к листу, этот внутренний лист сначала возвращает (), как и первый результат внешнего листо, поэтому вы получаете (reified_1. ()) Иэто может продолжаться бесконечно.Это работает, потому что у вас есть (cdro ld) с новым d, что позволяет d быть связанным с переменной, которая устанавливается рекурсивным вызовом listo.Вы не могли бы сделать это, не создав переменную d, выполнив unnesting.

Объясняя точку четности:

cdr(x) # get the rest elements of x
cdro(a x) # you "pass in" the equivalent to the output element of the first function into this logical version. 

Это означает, что если у вас есть b = cdr (cdr (x)), вынеобходимо создать переменную для хранения промежуточного значения, например:

fresh(a)
cdro(a, x)
fresh(b)
cdro(b, a)

Видите разницу / причину?Вы передаете свои выводы.Таким образом, вы не можете «вкладывать», где все находится внутри вложенного выражения, вам нужно разбить его на строки, чтобы было место для назначения новых переменных.

Почему так должно быть?Я размышлял, можно ли избежать большого количества ненужных сообщений, перегружая функции, основанные на четности.Нечто подобное я написал ниже (в python, предположим, что caro уже определено).Дело в том, что я думаю, что это бесполезно, потому что переменная, которую вы связываете с первым элементом списка, является новой, нигде не упоминаемой, поэтому не может быть полезной для применения каких-либо других ограничений.Задача состоит в том, чтобы вернуть наборы привязок, которые их удовлетворяют, но эти привязки должны быть на переменных, которые уже определены, или они бесполезны.

class UNDEF:
    pass

def cdronew(a, b=UNDEF):
    if b is UNDEF:
        # assume that we need to fresh a variable and use that for our output
        b = fresh('b')
        # not a typo in order, we're assuming we wanted the first val of the list
        # here is the problem, we'll bind b but noone outside this function knows about it so that binding is useless!
        return cdro(b, a)
    else:
        return cdro(a, b)
0 голосов
/ 03 декабря 2018

«Unnesting» предназначен для преобразования SSA , потому что это так, как это делает Prolog, потому что он не имеет оценки, и все изменения состояния и передача должны выполняться явно.

Форма SSAчто вы получаете ваш код, как после выполнения ограниченной формы CPS преобразования.Просто каждая промежуточная сущность делается явной и получает имя.

(let* ((c (+ (sqr x) (sqr y)) )
       (z (sqrt c)))
  ....

преобразуется в

(let*  ((a (sqr x))
        (b (sqr y))
        (c (+ a b))
        (z (sqrt c)))
  ....

Аналогично, когда вы пишете, код Lisp (list? (cdr l)) превращается в предикат

    ( L = [_ | D], 
      is_list( D ) )

в Прологе,что является целью

    (fresh (d)
       (cdro l d)    ; a relation "cdro" holds between `l` and `d`
       (listo  d))   ; a predicate listo holds for `d`

в миниКанрене.Зачем?Потому что (cdr l) - это Lisp функция, которая возвращает значение.Но в Прологе нет оценки, нет значений, возвращаемых неявно, а скорее они создаются явным образом с помощью предиката , отношения , путем «установки» логической переменной, котораяаргумент этого предиката.

0 голосов
/ 17 ноября 2018

термин un-nesting означает изменение иерархии структуры - или удаление скобок.

только что нашел книгу Разумный планировщик и связанный GitHub page , что также определяет его:

Процесс преобразования (car (cdr l)) в (cdro l v) и (caro v r) называется unnesting….Признать сходство между unnesting и [CPS].

...