Открыть список
Как стать автором
Обновить

Комментарии 22

Не часто можно встретить Prolog. Одно из мест, где он и сейчас используется — написание правил для обработки запросов на изменения (changes) и сливания кода (merge) в системе контроля версий и обсуждения кода Gerrit.
А какие там могут быть правила?
Примеры, скопированные из документации:
Make change submittable if commit author is «John Doe»
Make change submittable if commit message starts with «Fix „
Make change submittable only if Code-Review+2 is given by a non author
1+1=2 Code-Review
Make change submittable if all comments have been resolved
Make change submittable if it is a pure revert

Кстати, отличный пример rule-based модели

Всегда озадачивало почему библиотека алгоритма бэктракинга с api эмитирующим запись правил prolog не входят в стандартные библиотеки ни java ни .net. Т.е. я понимаю что в задачах общих языков программирования применения будет не много, но чисто с рекламными и образовательными целями включить такую библиотеку казалось бы должно быть выгодно. Но нет. Подозреваю что есть какие-то подводные камни которые не заметны с первого взгляда. Если знаете почему то поделитесь.

Мне кажется всё дело в том, что для многих это не слишком привычная для многих парадигма моделирования — но в LP сообществе эта тема очень популярна, то есть ASP и IDP — умеют интегрироваться с Prolog и вызывать его, если нужно.


Мы в одной из своих задач (не упомянутой здесь) использовали


https://labix.org/python-constraint

Библиотека для решения простых задач на ограничения прямо внутри Python, я думаю был бы реальный спрос и хорошие use-cases — и библиотеки напишут.

В Clojure есть стандартная библиотека core.logic, которая реализует miniKanren.
Про ProbProlog есть, а про Fuzzy Prolog будет?
И в чём принципиальная разница между Probability Logic и Fuzzy Logic?

Скорее имеет смысл сравнивать Problog с Weighted Logic аля Markov Logic — у каждой формулы есть вес, но для весов не выполняются аксиомы вероятности и их нельзя нормально проинтерпретировать. Т.е. мы выяснили, что лучшая формула подходящая под данные — это


a & b --> c

с весом 42, а следом за ним другая формула с весом 33 — это много или мало? Не слишком ясно.


Вот тут много полезных ссылок:
https://www.quora.com/What-are-the-hot-topics-in-machine-learning-and-fuzzy-logic-together

Fuzzy Logic проще в реализации и требует существенно меньше вычислений, но дадека от реальности, так как не умеет учитывать вклад нескольких не самых вероятных событий и взаимное влияние событий.
Возможно, это мечта ленивого наивного программиста, но: что мешает использовать LP в авто-генерации готового кода? Например, на Java или хотя бы его тестирование(или верификация).
А можно пример, как именно?
Эм… ну это я Вас хотел спросить, бывает ли такое )

Возможно будет коряво, но представляю себе это так:
Например допустим, я написал свою СУБД (со своими блэкджеками и ш алгоритмами) и мне нужно верифицировать, будет ли соблюдаться гарантированная изолированность транзакций. Во всех комбинациях возможных запросов SQL с учетом параллельного асинхронного их выполнения. Я просто “скармливаю” этот код системе верификации и она выдает ответ – да, транзакции всегда будут изолированными при любых запросах или наоборот – нет не будут, из за такого то участка в коде.

С автогенерацией кода на основе логической модели – сложнее, но я где то слышал, что в узких областях экспериментировали с этим.
Я не уверен, что вот это выполнимо:
> Во всех комбинациях возможных запросов SQL
Скорее нужно в runtime требовать выполнения этого условия и проверять его, чем тестировать на всех возможных запросах.

> С автогенерацией кода на основе логической модели – сложнее, но я где то слышал, что в узких областях экспериментировали с этим.

Да, я об этом напишу в следующих статьях — по сути Sketching for ASP, как раз из этих идей и вырос.
Чтобы гарантировать правильность сколько-нибудь сложной программы, ее нужно писать одновременно с доказательством. Доказать _уже_ написанную (без оглядки на способ доказательства) программу на языке общего назначения (скажем, Java), как правило, нереально.
Доказать _уже_ написанную (без оглядки на способ доказательства) программу на языке общего назначения (скажем, Java), как правило, нереально.

Вот я и мел в виду. Что почему бы средствами ASP например, парсить такие программы на языке общего назначения и создавая логическую модель — автоматически доказывать ее корректность. Например, отвечая на вопросы — при каких наборах входных параметров программа будет падать в необрабатываемые исключения (деление на ноль допустим).
Если бы это было возможно в общем виде, мы бы получили ответы на все математические вопросы.

Например, программа останавливается, когда, перебирая все тройки чисел, находит контр-пример к великой теореме Ферма. Если ASP докажет, что программа зависает — теорема доказана.

Или решать диофантовы уравнения можно так: если вход является решением, пусть программа падает. Вопрос к ASP — при каком входе программа падает.

Или подбирать ключи к шифрам, или…
В общем виде — разумеется невозможно. Там еще Теорема Гёделя нам рукой машет. Но, ведь значительное количество программ содержат очень простую арифметику, там нет ни каких полиномов с большими степенями…
Со знаниями математика можно понять, программа простая и легко доказуемая, или она сводится к решению новой, никем не решённой задачи.

Но как это запрограммировать? Может ли алгоритм в общем случае понять, простая задача тут или сложная. Если сложная, какие для неё известны методы решения.

очень простую арифметику, там нет ни каких полиномов с большими степенями
Как и в примере программы, проверяющей великую теорему Ферма.
Еще вопрос: а сиситемы проверки доказательств и логическое программирование как-то связаны? ведутся ли работы или уже предел достигут?
Вообще хотелось бы статью на хабре о системах проверки доказательств.
Это один из подходов: многие Proof Assistant, например Isabelle, используют внутри вариант логического программирования. Идеи там очень сильно перекликаются с Прологом, насколько мне известно.

Есть и другие, завязанные на функциональное программирование (в том числе Haskell).

> Вообще хотелось бы статью на хабре о системах проверки доказательств.
Я бы тоже её с радостью почитал :)
Только полноправные пользователи могут оставлять комментарии. Войдите, пожалуйста.