Кадр 1:85 — Почему накапливается conj2 из disj2?
В 85 есть:
(run* (x y)
(teacupo x)
(teacupo y))
который расширяется в:
(run* (x y)
(disj 2
(== 'tea x)
(== 'cup x))
(disj 2
(== 'tea y)
(== 'cup y)))
Так как жеconj2накапливать результаты, чтобы((tea tea) (tea cup) (cup tea) (cup cup))? Я не думаю, что это было объяснено должным образом в книге.
2 ответа
Кадр 1-53 гласит:
Значение
(run* q (conj2 (≡ 'corn q) (≡ 'meal q)))является().Для того, чтобы добиться успеха и
(≡ 'meal q)оба должны преуспеть. Первая цель удается, связываяcornс. Вторая цель не может тогда [выделено мной — wn] ассоциироватьсяmealс, сqуже не [выделено мной — wn] свежо.
Это означает, что в бинарной конъюнкции знания о состоянии ассоциации переменных и значений должны передаваться от первой цели ко второй. Таким образом, «выполнение» второй цели наступает после первой, в отличие отdisj2который «запускает» их независимо, «параллельно».
Это также означает, что код вполне правдоподобен.(run* (q p) (conj2 (≡ 'corn q) (≡ 'meal p)))иметь(corn meal)как его значение, потому чтоp"все еще" свеж даже после гола(≡ 'corn q)был выполнен". Это, собственно, и видно на кадрах 1-67 и 1-68 .
Таким образомconj2 «накапливает» знания об ассоциациях переменных и значений от своей первой цели до следующей, также известной как подстановка .
Но тогда что, если первой целью конъюнкции является дизъюнкция, производящая более одного значения?
Первый соответствующий кадр — это 1-77 , который показывает, что каждый из них должен быть передан второму по очереди, при этом собирая каждый результат. Но на самом деле он не обсуждает этот важный момент там .
Таким образом, схематически((a OR b), c) == ((a, c) OR (b, c))(письмо,дляAND), и аналогично(a, (b OR c)) == ((a, b) OR (a, c)), и поэтому
(a OR b) , (c OR d)
==
(a, (c OR d)) OR (b, (c OR d))
==
(a, c) OR (a, d) OR (b, c) OR (b, d)
что аналогично чтению следующей матрицы построчно:
c d
-------------
a | a,c a,d
b | b,c b,d
-------------
Другими словами,
(run* q
(conj2 (≡ 'corn q) (≡ 'meal q))) => ()
(run* q
(conj2 (≡ 'corn q) (≡ 'corn q))) => (corn)
(run* q
(disj2 (≡ 'corn q) (≡ 'meal q))) => (corn meal)
(run* (q p)
(conj2 (≡ 'corn q) (≡ 'meal p))) => ((corn meal))
(run* (q p)
(conj2
(≡ 'butter p)
(disj2 (≡ 'corn q) (≡ 'meal q)))) => ((corn butter) (meal butter))
(run* (q p)
(conj2
(disj2 (≡ 'corn q) (≡ 'meal q))
(≡ 'butter p))) => ((corn butter) (meal butter))
(run* (q p)
(conj2
(disj2 (≡ 'corn q) (≡ 'meal q))
(disj2 (≡ 'butter p) (≡ 'bread p))))
=> ((corn butter) (corn bread)
(meal butter) (meal bread))
Первая цель в соединении инстанцирует , вторая - инстанцирует , аrun (x y)говорит сообщить об обоих.
Оба и создаются, потому что отличаются от , поэтому они независимы друг от друга.
Это можно смоделировать в рамках парадигмы комбинирования потоков решений , как в этом моем ответе (эквивалентно модели книги без логических переменных), как этот псевдокод:
(1.) — это решение, замена, запись(name,value)пары. Он расширяется за счет унификации:
(var ≡ val) s = [[(x,v)] ++: s] // IF (x,_) NOT IN s , OR
| = [s] // IF (x,u) IN s AND u=v , OR
| = [] // OTHERWISE.
(все операторы любят
++:(«добавлять», также известное как «mplus»),
||:("или" он же "disj2 "),
>>:(«проталкивание», также известное как «привязка»), («и», также известное как «conj2 »), и т. д. определены в связанном ответе. Синтаксис представляет собой бесплатно лицензированное «приложение с каррированием путем сопоставления», аналогичное Haskell).
Замена представляет наши знания до сих пор. Объединение(x ≡ TEA), скажем, является целью — процедурой, которая при заданной замене производит поток новых замен (здесь — одну или ни одной), дополненный новым знанием, котороеx ≡ TEA (мы используем имена, написанные заглавными буквами, в качестве автоматически заключенных в кавычки символов) .
Увеличение замены предполагает возможный отказ от несовместимых значений.
Результатом является список, содержащий либо одну допустимую, возможно, расширенную замену, либо пустой список, не содержащий ни одной, что означает(x,v)был несовместим сs. Это выражает представление о том, что значение логической переменной, однажды установленное, не может измениться (за исключением возврата).
(2.) Дизъюнкция включает в себя применение целей по отдельности и передачу всех результирующих действительных решений (замен) вместе:
teacup° x = x ≡ TEA ||: x ≡ CUP
-- thus,
teacup° x s = (x ≡ TEA ||: x ≡ CUP) s
= (x ≡ TEA) s ++: (x ≡ CUP) s
(3.) Конъюнкцией каждое решение первой цели проходит через вторую:
(teacup° x &&: teacup° y) [] -- the initial substitution is empty
= teacup° x [] >>: teacup° y
= ( (x ≡ TEA ||: x ≡ CUP) [] ) >>: teacup° y
= ( (x ≡ TEA) [] ++: (x ≡ CUP) [] ) >>: teacup° y
= ( [[(x,TEA)]] ++: [[(x,CUP)]] ) >>: teacup° y
= [[(x,TEA)] , [(x,CUP)]] >>: teacup° y
= teacup° y [(x,TEA)] ++: teacup° y [(x,CUP)] ++: []
= (y ≡ TEA ||: y ≡ CUP) [(x,TEA)] ++:
(y ≡ TEA ||: y ≡ CUP) [(x,CUP)]
= (y ≡ TEA)[(x,TEA)] ++: (y ≡ CUP) [(x,TEA)] ++:
(y ≡ TEA) [(x,CUP)] ++: (y ≡ CUP) [(x,CUP)]
= [[(y,TEA),(x,TEA)]] ++: [[(y,CUP),(x,TEA)]] ++:
[[(y,TEA),(x,CUP)]] ++: [[(y,CUP),(x,CUP)]]
= [[(y,TEA),(x,TEA)] , [(y,CUP),(x,TEA)] ,
[(y,TEA),(x,CUP)] , [(y,CUP),(x,CUP)]]
Всего четыре решения, четыре замены, удовлетворяющие целиteacup° x &&: teacup° y, были произведены.
Соединение&&:двух целей будет для каждого из решений, полученных первой целью, собрать все решения, полученные второй целью, которые согласуются с решением, полученным второй целью. Здесь, посколькуxиyявляются двумя отдельными переменными, каждое новое решение не сталкивается со старым, другими словами, ни одно из решений не отвергается.
(4.) Если бы мы использовали одну и ту же переменную дважды, их взаимодействие означало бы, что мы должны отказаться от несовместимых подстановок:
(teacup° x &&: teacup° x) [] -- the initial substitution is empty
= teacup° x [] >>: teacup° x
= ( (x ≡ TEA ||: x ≡ CUP) [] ) >>: teacup° x
= ( (x ≡ TEA) [] ++: (x ≡ CUP) [] ) >>: teacup° x
= ( [[(x,TEA)]] ++: [[(x,CUP)]] ) >>: teacup° x
= [[(x,TEA)] , [(x,CUP)]] >>: teacup° x
= teacup° x [(x,TEA)] ++: teacup° x [(x,CUP)] ++: []
= (x ≡ TEA ||: x ≡ CUP) [(x,TEA)] ++:
(x ≡ TEA ||: x ≡ CUP) [(x,CUP)]
= (x ≡ TEA)[(x,TEA)] ++: (x ≡ CUP) [(x,TEA)] ++:
(x ≡ TEA) [(x,CUP)] ++: (x ≡ CUP) [(x,CUP)]
= [[(x,TEA)]] ++: [] ++: [] ++: [[(x,CUP)]]
= [[(x,TEA)] , [(x,CUP)]]
Здесь создаются два решения, потому что одна и та же логическая переменная не может одновременно содержать два разных значения, поэтому, например,(x ≡ CUP) [(x,TEA)]решает как[], пустой список, не содержащий решений, тем самым отклоняя попытку присвоения(x,CUP)когда(x,TEA)уже присутствует.
(5.)(run* (x y) (teacup° x) (teacup° y))более-менее похоже
[[]] >>: (teacup° x &&: teacup° y) >>: report [x, y]
==
(teacup° x &&: teacup° y) [] >>: report [x, y]
==
[[(y,TEA),(x,TEA)], [(y,CUP),(x,TEA)],
[(y,TEA),(x,CUP)], [(y,CUP),(x,CUP)]] >>: report [x, y]
==
report [x, y] [(y,TEA),(x,TEA)] ++:
report [x, y] [(y,CUP),(x,TEA)] ++:
report [x, y] [(y,TEA),(x,CUP)] ++:
report [x, y] [(y,CUP),(x,CUP)]
==
[ (TEA,TEA), (TEA,CUP), (CUP,TEA), (CUP,CUP) ]
для надлежащим образом определенногоreport <vars>цель.
(6.) Иrun* (x) (teacup° x) (teacup° x))более-менее похоже
[[]] >>: (teacup° x &&: teacup° x) >>: report [x]
==
(teacup° x &&: teacup° x) [] >>: report [x]
==
[[(x,TEA)], [(x,CUP)]] >>: report [x]
==
report [x] [(x,TEA)] ++: report [x] [(x,CUP)]
==
[ TEA, CUP ]