Сопоставление с образцом с ассоциативными и коммутативными операторами

Question

Сопоставление с образцом (как, например, в Прологе, языках семейства ML и различных оболочках экспертной системы) обычно выполняется путем сопоставления запроса с элементом данных по элементу в строгом порядке.

В таких областях, как автоматическое доказательство теоремоднако необходимо учитывать, что некоторые операторы являются ассоциативными и коммутативными.Предположим, у нас есть данные

A or B or C

и запрос

C or $X

Если следовать синтаксису поверхности, это не совпадает, но логически оно должно совпадать с $X, связанным с A or B, потому что1011 * является ассоциативным и коммутативным.

Существует ли какая-либо существующая система на любом языке, которая делает подобные вещи?

Answer 1

Ассоциативно-коммутативное сопоставление с образцом существует с 1981 и ранее , и до сих пор остается актуальной темой сегодня .

Есть много систем, которые реализуют эту идею и делают ее полезной; это означает, что вы можете избежать записи сложных сопоставлений с образцом, если для сопоставления с образцом можно использовать ассоциативность или коммутативность. Да, это может быть дорого; Лучше, чтобы сопоставитель шаблонов делал это автоматически, чем плохо.

Вы можете увидеть пример в системе переписывания для алгебры и простого исчисления , реализованной с использованием нашей системы преобразования программ. В этом примере обрабатываемый символьный язык определяется правилами грамматики, и те правила, которые имеют свойства A-C, помечаются. Перезаписи на деревьях, полученные в результате синтаксического анализа символьного языка, автоматически расширяются для соответствия.

Answer 2

В переписывающем устройстве maude реализовано ассоциативное и коммутативное сопоставление с образцом.

http://maude.cs.uiuc.edu/

Answer 3

Я никогда не сталкивался с такой вещью, и у меня был более подробный взгляд.

Есть веская вычислительная причина для того, чтобы не реализовывать это по умолчанию - нужно по существу генерировать все комбинации входных данных перед сопоставлением с образцом, или вам нужно сгенерировать полную сумму совпадений для всех предложений соответствия.

Я подозреваю, что обычным способом реализации этого было бы просто написать оба шаблона (в двоичном случае), то есть иметь шаблоны для C or $X и $X or C.

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

Между прочим, я подозреваю, что операция, которую вы в основном хотите, это разделение шаблонов объединения на множествах, например ::11011*

foo (Or ({C} disjointUnion {X})) = ...

Единственная среда программирования, которую я видел, которая имеет дело с множествами в любой детали, - это Изабель / HOL, и я до сих пор не уверен, что вы можете создавать сопоставления с образцами по ним.

РЕДАКТИРОВАТЬ: Похоже, что функциональность function Изабель (а не fun) позволит вам определять сложные неконструктивные шаблоны, за исключением того, что вы должны доказать, что они используются последовательно, и вы не можете использовать код генератор больше.

РЕДАКТИРОВАТЬ 2: Способ, которым я реализовал аналогичную функциональность по n коммутативным, ассоциативным и транзитивным операторам, был следующим:

Мои термины имели форму A | B | C | D, тогда как запросы имели форму B | C | $X, где $X было разрешено совпадать с нолем или более. Я предварительно отсортировал их с помощью лексографического упорядочения, чтобы переменные всегда встречались в последней позиции.

Сначала вы создаете все парные совпадения, игнорируя переменные на данный момент и записывая те, которые соответствуют вашим правилам.

{ (B,B), (C,C)  }

Если вы рассматриваете это как двудольный граф, то, по сути, вы решаете проблему идеальный брак . Существуют быстрые алгоритмы для их нахождения.

Предполагая, что вы найдете его, вы собираете все, что не отображается в левой части вашего отношения (в этом примере A и D), и помещаете их в переменную $X и ваш матч завершен. Очевидно, что здесь вы можете потерпеть неудачу на любом этапе, но это в основном произойдет, если в RHS нет свободной переменной или если в LHS существует конструктор, который ничем не соответствует (что не позволяет вам найти идеальное соответствие).

Извините, если это немного запутано. Прошло много времени с тех пор, как я написал этот код, но я надеюсь, что это поможет вам, даже немного!

Для справки, это может не быть хорошим подходом во всех случаях. У меня были очень сложные понятия «совпадение» на подтермах (то есть не простое равенство), и поэтому построение множеств или чего-либо еще не работало бы. Возможно, это сработает и в вашем случае, и вы сможете напрямую вычислять непересекающиеся союзы.