Расширение шаблона спецификации на основе LINQ для реализации включения

Существует множество реализаций шаблона составной спецификации на основе LINQ. Я не видел ни одного, который использовал бы субсумпшн.

Есть ли такие примеры, которые были задокументированы (блоги и т. д.) или опубликованы как открытый исходный код? У меня есть идея и доказательство концепции того, как это может работать, если ExpressionVisitor переводит каждую спецификацию в каноническую логическую форму (CNF/DNF), но я обеспокоен тем, что это слишком сложно. Есть ли способ лучше?


linq linq-expressions boolean-logic boolean-expression specification-pattern
person smartcaveman    schedule 04.12.2012    source источник
comment
Вы имели в виду условное предложение where в Linq?   -  person Frank Myat Thu    schedule 10.12.2012

Ответы (1)


arrow_upward
2
arrow_downward

Меня беспокоит, что это слишком сложно. Есть ли способ лучше?

Короткий ответ: "Нет, не существует" 1

Длинный ответ: «слишком сложный» отражает суть проблемы: это NP-сложно. Вот короткое неофициальное доказательство, основанное на том факте, что проблема выполнимости является NP-полной. :

  • Предположим, что у вас есть две логические формулы, A и B.
  • Вам нужно проверить, подразумевает ли A B или, что то же самое, ¬A | B для всех назначений переменных, от которых зависят A и B. Другими словами, вам нужно доказательство того, что F = ¬A | B является тавтологией.
  • Предположим, что тест на тавтологию можно выполнить за полиномиальное время
  • Рассмотрим ¬F, обратную F. F выполнимо тогда и только тогда, когда ¬F не является тавтологией
  • Используйте гипотетический полиномиальный алгоритм, чтобы проверить, является ли ¬F тавтологией.
  • Ответ на вопрос «является ли F выполнимым» является обратным ответу на вопрос «является ли ¬F тавтологией».
  • Следовательно, существование полиномиального средства проверки тавтологии будет означать, что проблема выполнимости находится в P и что P=NP.

Конечно, тот факт, что проблема является NP-трудной, не означает, что не будет решений для практических случаев: на самом деле ваш подход с преобразованием к канонической форме может дать хорошие результаты во многих реальных ситуациях. Однако отсутствие заведомо «хорошего» алгоритма часто препятствует активной разработке практических решений2.

1 С обязательной оговоркой "если не P=NP".

2 Если только не подойдет "достаточно хорошее" решение, что вполне может иметь место для вашей проблемы, если вы допускаете "ложноотрицательные результаты".

person Sergey Kalinichenko    schedule 11.12.2012
comment
+1, Вопрос: вы используете тавтологию в формально-логическом смысле слова или в CS есть похожее, но по-другому квалифицированное определение? Насколько я понимаю, предложение тавтологично, если оно может быть получено из пустого множества предложений SC. Это не будет адекватным описанием того, что я пытаюсь доказать, потому что у меня также есть обширная база знаний/база данных, из которой можно извлечь. С другой стороны, проблема сложная, но раньше она была эффективно решена. Прямо сейчас я изучаю Prolog, Euler и Microsoft Solver Foundation. - person smartcaveman; 13.12.2012
comment
@smartcaveman Я использую тавтологию в формально-логическом смысле этого слова: чтобы доказать, что выражение A включает в себя B, вам нужно показать, что A => B всегда верно, то есть может быть получено из пустого набора предпосылок. Единственная причина, по которой я упомянул об этом, заключалась в том, чтобы добраться до проблемы выполнимости, которая, как известно, является NP-полной. Обратите внимание, что только A => B должно быть тавтологией; отдельные выражения A и B могут быть и во всех нетривиальных случаях будут основываться на непустых наборах предпосылок. Чем больше этот набор, тем сложнее доказать отнесение B к A. - person Sergey Kalinichenko; 13.12.2012
comment
так что у меня была другая идея, как решить эту проблему более практически - все еще работая над этим. Вместо чистого переписывания я мог бы создать модель квадрата оппозиции для каждого предиката и потребовать, чтобы все мои предикаты были в силлогистической форме. Кажется, что это может уменьшить сложность, потому что контент будет нормализован, а не формальное представление - поскольку мой домен является бизнес-приложением, я думаю, что оно может быть достаточно выразительным. Есть предположения? - person smartcaveman; 14.12.2012
comment
@smartcaveman Изменение представления не изменит фундаментальной сложности проблемы. Даже если вы нормализуете все до 3-CNF, вы все еще находитесь в пространстве NP. По сути, вы строите средство доказательства теорем первого порядка — это непросто, если только вы существенно не ограничите свои предикаты. Разрешение ложных отрицательных результатов в некоторых крайних случаях может быть еще одним компромиссом, если ваше приложение может это допустить. - person Sergey Kalinichenko; 14.12.2012
comment
Можете ли вы подробнее рассказать о том, что вы имели в виду: разрешить ложные отрицания для крайних случаев или дать мне ссылку на где-нибудь, где обсуждается этот вариант? - person smartcaveman; 28.12.2012
comment
@smartcaveman Я имел в виду попробовать символический подход, когда два дерева выражений проверяются на изоморфизм подграфов. Поскольку деревья представляют собой плоские графы, вы можете использовать линейное время. алгоритм поиска соответствия. К сожалению, обнаружение таких совпадений наложило бы чрезмерные ограничения на представление ваших выражений. В результате можно будет построить пару выражений, содержащих совпадение, но символьный алгоритм его не найдет. - person Sergey Kalinichenko; 28.12.2012
comment
@smartcaveman Например, упрощенный символический подход не найдет соответствия между ¬B & ¬C и A | ¬(B | C), потому что он не знает о законах ДеМоргана. Конечно, вы можете внести множество улучшений, чтобы исключить такие простые случаи, как этот, но вы не сможете охватить их все. - person Sergey Kalinichenko; 28.12.2012
comment
спасибо, что прояснили это - теперь я понимаю, что вы имеете в виду по поводу ложноотрицательных результатов. Однако я не думаю, что согласен на такой компромисс. Я бы не считал законы ДеМоргана крайним случаем ... ошибаюсь ли я, думая, что лексическое сравнение символов выражений, отсортированных по алфавиту в CNF, охватит все случаи? - person smartcaveman; 29.12.2012
comment
@smartcaveman Если оба выражения являются CNF, вам больше не нужны законы ДеМоргана. Вам даже не нужно сортировать, просто запустите алгоритм изоморфизма подграфов на двух деревьях выражений. Добраться до CNF будет сложно, если вы выберете этот подход. - person Sergey Kalinichenko; 29.12.2012