Описание тега unification

Unification, in computer science and logic, is an algorithmic process by which one attempts to solve the satisfiability problem. The goal of unification is to find a substitution which demonstrates that two seemingly different terms are in fact either identical or just equal.
2 ответа

Поиск всех объединений в прологе

Я написал свой первый простой код в PROLOG: is_beginning([], _). is_beginning([FirstLetterB|RestWordB], [FirstLetterW|RestWordW]) :- FirstLetterB == FirstLetterW, is_beginning(RestWordB, RestWordW). Он предназначен для определения, равен ли первый а…
10 дек '12 в 10:10
1 ответ

Ошибка типа в функции Haskell

Я написал функцию Haskell следующим образом: shift :: Subst a -> Subst a shift (S s) = [(x, (subst s' d)) | (x,d) <- s] where s' = [(x,d) | (x,d) <- s, null (vars d)] С типом данных вроде data Subst a = S [(String,a)] Я объявил subst как su…
10 ноя '12 в 00:34
2 ответа

Ручной вывод типа для `f1 x xs = (filter . (<)) X xs`

Я хочу вручную получить тип: f1 x xs = (filter . (&lt;)) x xs Первый раз мы видим x, так: x :: t1 затем (&lt;) имеет этот тип: (&lt;) :: Ord a1 =&gt; a1 -&gt; a1 -&gt; Bool Мы можем только сказать (&lt; x) если следующие типы могут быть объединены: …
27 апр '14 в 18:37
1 ответ

Логика первого порядка цепочки прямого движения (унификация)

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

Пользовательский синтаксис структуры данных в Прологе

В Прологе [H|T] это список, который начинается с H и где остальные элементы находятся в списке T (внутренне представлен с '.'(H, '.'(…))). Можно ли определить новый синтаксис подобным образом? Например, можно ли определить, что [T~H] это список, кот…
1 ответ

Вручную получим тип `zipWith . uncurry`

Я пытаюсь вывести тип zipWith . uncurry zipWith . uncurry = (.) zipWith uncurry - конкатенация как функция (.) :: (b1 -&gt; c1) -&gt; (a1 -&gt; b1) -&gt; a1 -&gt; c1 zipWith :: (a2 -&gt; b2 -&gt; c2) -&gt; [a2] -&gt; [b2] -&gt; [c2] uncurry :: (a3 -…
03 май '14 в 00:43
2 ответа

Предикат участника

Когда вы звоните member(Item, List) с неослабленным списком Prolog объединяет и возвращает список, содержащий элемент. Я хочу правило, которое возвращает true/false и не пытается объединиться. Есть ли такое правило?
05 янв '14 в 15:59
1 ответ

Пролог одинарная кавычка (') унификация

Я пытаюсь объединить переменную X с '*' (включая кавычки, в общей сложности 3-символьную строку), что я делаю, это простой X='*'., но в результате X имеет значение *, Если я пойду на X=''*''.результат X=''*'', Я запутался, как я могу достичь '*'?
26 апр '15 в 00:05
1 ответ

Объединение двигателя не работает на Laravel

Когда я использую ключи унификации для совместного использования в инфраструктуре laravel, я получаю эту ошибку статус: 403 и информация: запрещено в ответ. Спасибо
06 авг '17 в 18:55
1 ответ

Подключение к выводу трассы объединения пролога

Я пытаюсь исследовать выполнимость проекта по созданию языка вывода пользовательских типов на нетипизированном языке. (Сам язык не важен, но это PHP). Моя первая идея - запустить унификацию типов на этом. Я немного программировал на Haskell, так что…
29 мар '13 в 23:28
4 ответа

Пролог, доступ к конкретному члену списка?

Может кто-нибудь сказать мне, как получить доступ к конкретному члену списка в прологе? Скажем, например, мне нужен доступ к 3-му или 4-му элементу списка, переданного в правило?
17 окт '12 в 16:55
2 ответа

GHC отклоняет код монады ST как неспособный объединить переменные типа?

Я написал следующую функцию: (.&gt;=.) :: Num a =&gt; STRef s a -&gt; a -&gt; Bool r .&gt;=. x = runST $ do v &lt;- readSTRef r return $ v &gt;= x но когда я попытался скомпилировать, я получил следующую ошибку: Could not deduce (s ~ s1) from the co…
04 ноя '11 в 09:21
2 ответа

Идрис - Невозможно оценить применение функции по типу

Я получаю проблему, когда у меня есть значение с типом fun a, с fun быть функцией и a значение, которое не вычисляется при проверке типов и выдает ошибку объединения, когда я заставляю его быть результатом применения этой функции. Конкретная ошибка …
22 дек '15 в 05:52
2 ответа

Удаление всех членов списка без объединения в прологе

Возможный дубликат: Пролог удалить: не удаляет все элементы, которые объединяются с элементом В Прологе, если вы напишите это: delete([(1,1),(1,2),(1,1),(3,4)],(1,_),L). результат будет: L = [ (1, 2), (3, 4)]. Что является нормальным, потому что пер…
11 ноя '11 в 22:18
1 ответ

Почему это выражение не унифицировано?

Я определил следующую базу знаний: leaf(_). tree(X) :- leaf(X). и ожидал запрос: leaf(X) = tree(X). возвращать true .потому что любой лист должен по определению быть деревом. К сожалению, активация трассировки не дает никаких полезных результатов. В…
02 дек '18 в 15:26
1 ответ

Подстановка в логике первого порядка

Я должен сказать, объединяют ли следующие пары выражений. Это задача: f(g(a, X), g(X, b)) = f(g(a, b, c, d)) Я знаю, что при заданном наборе выражений подстановка является унификатором для этого набора, если все условия набора являются одинаковыми с…
13 дек '18 в 10:24
2 ответа

Казалось бы, ненужный случай в алгоритме унификации в SICP

Я пытаюсь понять алгоритм объединения, описанный в SICP здесь В частности, в процедуре "extend-if-возможный" есть проверка (первое место, помеченное звездочкой "*"), которая проверяет, является ли правое выражение "выражение" переменной, которая уже…
04 авг '09 в 19:56
2 ответа

Почему SWI-Prolog объединяет строку в кавычках и без кавычек (без пробелов) в одно правило?

Предположим, у меня есть следующие правила: unify('test', 'this is a test'). run :- write('Enter something: '), read(X), unify(X, Y), write('The answer is '), write(Y). И тогда я запускаю это следующим образом: ?- ['unify.pl']. % unify.pl compiled 0…
04 ноя '10 в 20:18
1 ответ

Пролог - объяснение шагов трассировки на английском языке

plays(alice, leadguitar). plays(noah, drums). plays(mike, leadguitar). plays(mike, drums). plays(katie, baseguitar). plays(drew, leadguitar). plays(drew, baseguitar). duetwith(Person1,Person2):- plays(Person1,L), plays(Person2,L), Person1 \= Person2…
25 ноя '18 в 18:18
2 ответа

Странность объединения в экземпляре класса типов

Допустим, у меня есть следующий (глупый) класс: class BlindMap m where mapB :: m a -&gt; m b Я мог бы предоставить следующее [] пример: instance BlindMap [] where mapB = map id Тип RHS является [a] -&gt; [a] который должен объединиться с [a] -&gt; […