Как добавить приоритет оператора в грамматику жаворонка для FOL с равенством?

Как изменить эту грамматику, чтобы она соответствовала скобкам, которые находятся дальше?

?wff: compound_wff
?compound_wff: biconditional_wff
?biconditional_wff: conditional_wff (SPACE? BICONDITIONAL_SYMBOL SPACE? biconditional_wff)*
?conditional_wff: disjunctive_wff (SPACE? CONDITIONAL_SYMBOL SPACE? conditional_wff)*
?disjunctive_wff: conjunctive_wff (SPACE? DISJUNCTION_SYMBOL SPACE? disjunctive_wff)*
?conjunctive_wff: negated_wff (SPACE? CONJUNCTION_SYMBOL SPACE? conjunctive_wff)*
?negated_wff: (NEGATION_SYMBOL SPACE)* atomic_wff
?atomic_wff: predicate
           | term EQUAL_TO term
           | quantified_wff* LEFT_PARENTHESIS SPACE? wff SPACE? RIGHT_PARENTHESIS
?term: function
    | NAME
    | VARIABLE
?predicate: PREDICATE_NAME [LEFT_PARENTHESIS term (COMMA term)* RIGHT_PARENTHESIS]
?function: FUNCTION_NAME LEFT_PARENTHESIS term (COMMA SPACE? term)* RIGHT_PARENTHESIS
?quantified_wff: curly_quantifiers | quantifiers
?curly_quantifiers: quantifier_symbol LEFT_CURLY_BRACE VARIABLE (COMMA SPACE? VARIABLE)* RIGHT_CURLY_BRACE SPACE?
?quantifiers: quantifier_symbol SPACE? VARIABLE (COMMA SPACE? VARIABLE)* SPACE?

SPACE: /\s+/
COMMA: ","
EQUAL_TO: "="
LEFT_PARENTHESIS: "("
RIGHT_PARENTHESIS: ")"
LEFT_CURLY_BRACE: "{"
RIGHT_CURLY_BRACE: "}"
quantifier_symbol: UNIVERSAL_QUANTIFIER_SYMBOL | EXISTENTIAL_QUANTIFIER_SYMBOL
UNIVERSAL_QUANTIFIER_SYMBOL: "\\forall" | "∀"
EXISTENTIAL_QUANTIFIER_SYMBOL: "\\exists" | "∃"
NAME: /[a-t]/ | /[a-t]_[1-9]\d*/
VARIABLE: /[u-z]/ | /[u-z]_[1-9]\d*/
PREDICATE_NAME: /[A-HJ-Z]/ | /[A-HJ-Z]_[1-9]\d*/
FUNCTION_NAME: /[a-z]/ | /[a-z]_[1-9]\d*/
NEGATION_SYMBOL: "\\neg" | "\\lnot" | "¬"
CONJUNCTION_SYMBOL: "\\wedge" | "\\land" | "∧"
DISJUNCTION_SYMBOL: "\\vee" | "\\lor" | "∨"
CONDITIONAL_SYMBOL: "\\rightarrow" | "\\Rightarrow" | "\\Longrightarrow" | "\\implies" | "→" | "⇒"
BICONDITIONAL_SYMBOL: "\\leftrightarrow" | "\\iff" | "↔" | "⇔"

Я пытаюсь разобрать это, используя свою грамматику:

Что в LaTeX:

\exists{x} \forall{y} (P(f(x, y)) \vee \forall{z}(V(z) \iff \neg R(a) \wedge B(a)))

Я последовал примеру калькулятора и изменил свою исходную грамматику, чтобы добавить приоритет оператора, что привело к этому. Но он больше не принимает входную строку.

Я получаю эту ошибку:

lark.exceptions.UnexpectedCharacters: No terminal matches '\' in the current parser context, at line 1 col 35

\exists{x} \forall{y} (P(f(x, y)) \vee \forall{z}(V(z) \iff \neg R(a) \wed
                                  ^
Expected one of: 
    * RIGHT_PARENTHESIS

В идеале я хочу заставить требовать круглые скобки везде, где это возможно, за исключением случаев перед отрицательным atomic_wff без круглых скобок. Это делается для того, чтобы гарантировать создание только одного дерева синтаксического анализа даже при явной настройке неоднозначности. Как решить эту проблему?

Изменить 1

Я хочу уточнить, что приоритет операторов для одних и тех же операторов должен быть правоассоциативным. Итак, P(a) ∧ Q(a) ∧ R(a) разрешится как P(a) ∧ (Q(a) ∧ R(a))

Редактировать 2

Я упростил отладку грамматики жаворонка, используя соответствующие терминалы. Теперь он анализирует длинное латексное уравнение, но по-прежнему неоднозначен для более простых входных данных, таких как P(a) ∧ Q(a) ∧ R(a), который создает два дерева синтаксического анализа. Я до сих пор не знаю, что я делаю неправильно. Грамматика выполняет правильную рекурсию и по-прежнему не может создать ни одного дерева синтаксического анализа.

Редактировать 3

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

?wff: compound_wff
compound_wff: biconditional_wff
biconditional_wff: conditional_wff (SPACE? BICONDITIONAL_SYMBOL SPACE? conditional_wff)*
conditional_wff: disjunctive_wff (SPACE? CONDITIONAL_SYMBOL SPACE? disjunctive_wff)*
disjunctive_wff: conjunctive_wff (SPACE? DISJUNCTION_SYMBOL SPACE? conjunctive_wff)*
conjunctive_wff: negated_wff (SPACE? CONJUNCTION_SYMBOL SPACE? negated_wff)*
negated_wff: (NEGATION_SYMBOL SPACE?)* atomic_wff
atomic_wff: predicate
          | term EQUAL_TO term
          | quantified_wff* LEFT_PARENTHESIS SPACE? wff SPACE? RIGHT_PARENTHESIS
term: function
    | NAME
    | VARIABLE
predicate: PREDICATE_NAME [LEFT_PARENTHESIS term (COMMA term)* RIGHT_PARENTHESIS]
function: FUNCTION_NAME LEFT_PARENTHESIS term (COMMA term)* RIGHT_PARENTHESIS
quantified_wff: curly_quantifiers | quantifiers
curly_quantifiers: quantifier_symbol LEFT_CURLY_BRACE VARIABLE (COMMA SPACE? VARIABLE)* RIGHT_CURLY_BRACE SPACE?
quantifiers: quantifier_symbol SPACE? VARIABLE (COMMA SPACE? VARIABLE)* SPACE?

SPACE: /\s+/
COMMA: /,\s*/
EQUAL_TO: /\s*=\s*/
LEFT_PARENTHESIS: "("
RIGHT_PARENTHESIS: ")"
LEFT_CURLY_BRACE: "{"
RIGHT_CURLY_BRACE: "}"
quantifier_symbol: UNIVERSAL_QUANTIFIER_SYMBOL | EXISTENTIAL_QUANTIFIER_SYMBOL
UNIVERSAL_QUANTIFIER_SYMBOL: "\\forall" | "∀"
EXISTENTIAL_QUANTIFIER_SYMBOL: "\\exists" | "∃"
NAME: /[a-t]/ | /[a-t]_[1-9]\d*/
VARIABLE: /[u-z]/ | /[u-z]_[1-9]\d*/
PREDICATE_NAME: /[A-HJ-Z]/ | /[A-HJ-Z]_[1-9]\d*/
FUNCTION_NAME: /[a-z]/ | /[a-z]_[1-9]\d*/
NEGATION_SYMBOL: "\\neg" | "\\lnot" | "¬"
CONJUNCTION_SYMBOL: "\\wedge" | "\\land" | "∧"
DISJUNCTION_SYMBOL: "\\vee" | "\\lor" | "∨"
CONDITIONAL_SYMBOL: "\\rightarrow" | "\\Rightarrow" | "\\Longrightarrow" | "\\implies" | "→" | "⇒"
BICONDITIONAL_SYMBOL: "\\leftrightarrow" | "\\iff" | "↔" | "⇔"

%ignore SPACE
%ignore COMMA
%ignore LEFT_CURLY_BRACE
%ignore RIGHT_CURLY_BRACE

Таким образом, невозможно создать одно дерево синтаксического анализа для ¬P(a) ∧ Q(b).

Вам действительно не хватает правой скобки в вашем выражении (P(f(x, y))

gimix 20.11.2022 14:15

Нет я не. Первая скобка перед P должна соответствовать последней скобке во всей формуле.

daegontaven 20.11.2022 23:48

Вы говорите: «Я хочу заставить требовать круглые скобки везде, где это возможно, за исключением случая перед отрицательным atomic_wff без круглых скобок». Но ваш пример wff включает ... ⟺¬R(a)∧B(a), где правым оператором является союз ¬R(a)∧B(a), написанный без круглых скобок. Так что это? Скобки необязательны, и двусмысленность разрешается, потому что имеет более низкий приоритет, чем ? Или нужны скобки и пример wff неверный?

rici 21.11.2022 18:16

Я спрашиваю, потому что у меня есть грамматика, которая требует круглых скобок в соответствии с запросом, но она отклоняет ваш пример именно потому, что нужные круглые скобки отсутствуют. Я опубликую это, как только вы уточните.

rici 21.11.2022 18:17

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

daegontaven 21.11.2022 20:37

@rici Я добавил разъяснение выше в комментарии.

daegontaven 22.11.2022 14:57

@daegontaven: Извините, я не видел этот комментарий раньше. Иногда @ необходимы. При всем уважении, я не думаю, что "правильный ассоциативный ряд для всех связок" - хорошая идея. Это будет анализировать P∨Q⟺P∧R как P∨(Q⟺(P∧R)), что почти наверняка не является предполагаемой интерпретацией. Если вы имеете в виду, что связки правильно ассоциативны сами с собой, это нормально (и нормально, я думаю), но он не примет P∨Q⟺P∧R без скобок, устраняющих неоднозначность (P∨Q)⟺(P∧R), поэтому ваш пример ввода не анализируется. Можно много говорить об общих правилах приоритета :-) Но ваш выбор.

rici 22.11.2022 17:07

Для дальнейшего использования, пожалуйста, отредактируйте свои разъяснения в своем вопросе. Комментарии здесь эфемерны.

rici 22.11.2022 17:08

@rici Да, я хочу правильной ассоциативности, но с таким приоритетом операторов, чтобы отрицание было выше конъюнкции, а не дизъюнкции, а не условного, а не биусловного. Таким образом, P∨Q⟺P∧R будет автоматически разрешаться как (P∨Q)⟺(P∧R), поскольку ∧ и ∨ имеют более высокий приоритет, чем ⟺.

daegontaven 22.11.2022 19:02

@rici Я добавил уточнение к вопросу.

daegontaven 24.11.2022 17:40
14 Задание: Типы данных и структуры данных Python для DevOps
14 Задание: Типы данных и структуры данных Python для DevOps
проверить тип данных используемой переменной, мы можем просто написать: your_variable=100
Python PyPDF2 - запись метаданных PDF
Python PyPDF2 - запись метаданных PDF
Python скрипт, который будет записывать метаданные в PDF файл, для этого мы будем использовать PDF ридер из библиотеки PyPDF2 . PyPDF2 - это...
Переменные, типы данных и операторы в Python
Переменные, типы данных и операторы в Python
В Python переменные используются как место для хранения значений. Пример переменной формы:
Почему Python - идеальный выбор для проекта AI и ML
Почему Python - идеальный выбор для проекта AI и ML
Блог, которым поделился Harikrishna Kundariya в нашем сообществе Developer Nation Community.
Как автоматически добавлять котировки в заголовки запросов с помощью PyCharm
Как автоматически добавлять котировки в заголовки запросов с помощью PyCharm
Как автоматически добавлять котировки в заголовки запросов с помощью PyCharm
Анализ продукта магазина на Tokopedia
Анализ продукта магазина на Tokopedia
Tokopedia - это место, где продавцы могут продавать свои товары. Товар должен быть размещен на витрине, чтобы покупателям было легче найти товар...
1
10
167
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

Проблема заключалась в том, что каждое правило wff не соответствовало предшествующему правилу в его частях. Так:

?biconditional_wff: conditional_wff (SPACE? BICONDITIONAL_SYMBOL SPACE? biconditional_wff)*

Следует изменить на:

?biconditional_wff: conditional_wff (SPACE? BICONDITIONAL_SYMBOL SPACE? conditional_wff)*

Решение этой проблемы состоит в том, чтобы иметь такую ​​грамматику:

?wff: compound_wff
compound_wff: biconditional_wff
biconditional_wff: conditional_wff (SPACE? BICONDITIONAL_SYMBOL SPACE? conditional_wff)*
conditional_wff: disjunctive_wff (SPACE? CONDITIONAL_SYMBOL SPACE? disjunctive_wff)*
disjunctive_wff: conjunctive_wff (SPACE? DISJUNCTION_SYMBOL SPACE? conjunctive_wff)*
conjunctive_wff: negated_wff (SPACE? CONJUNCTION_SYMBOL SPACE? negated_wff)*
negated_wff: (NEGATION_SYMBOL SPACE?)* atomic_wff
atomic_wff: predicate
          | term EQUAL_TO term
          | quantified_wff* LEFT_PARENTHESIS SPACE? wff SPACE? RIGHT_PARENTHESIS
term: function
    | NAME
    | VARIABLE
predicate: PREDICATE_NAME [LEFT_PARENTHESIS term (COMMA term)* RIGHT_PARENTHESIS]
function: FUNCTION_NAME LEFT_PARENTHESIS term (COMMA term)* RIGHT_PARENTHESIS
quantified_wff: curly_quantifiers | quantifiers
curly_quantifiers: quantifier_symbol LEFT_CURLY_BRACE VARIABLE (COMMA SPACE? VARIABLE)* RIGHT_CURLY_BRACE SPACE?
quantifiers: quantifier_symbol SPACE? VARIABLE (COMMA SPACE? VARIABLE)* SPACE?

SPACE: /\s+/
COMMA: /,\s*/
EQUAL_TO: /\s*=\s*/
LEFT_PARENTHESIS: "("
RIGHT_PARENTHESIS: ")"
LEFT_CURLY_BRACE: "{"
RIGHT_CURLY_BRACE: "}"
quantifier_symbol: UNIVERSAL_QUANTIFIER_SYMBOL | EXISTENTIAL_QUANTIFIER_SYMBOL
UNIVERSAL_QUANTIFIER_SYMBOL: "\\forall" | "∀"
EXISTENTIAL_QUANTIFIER_SYMBOL: "\\exists" | "∃"
NAME: /[a-t]/ | /[a-t]_[1-9]\d*/
VARIABLE: /[u-z]/ | /[u-z]_[1-9]\d*/
PREDICATE_NAME: /[A-HJ-Z]/ | /[A-HJ-Z]_[1-9]\d*/
FUNCTION_NAME: /[a-z]/ | /[a-z]_[1-9]\d*/
NEGATION_SYMBOL: "\\neg" | "\\lnot" | "¬"
CONJUNCTION_SYMBOL: "\\wedge" | "\\land" | "∧"
DISJUNCTION_SYMBOL: "\\vee" | "\\lor" | "∨"
CONDITIONAL_SYMBOL: "\\rightarrow" | "\\Rightarrow" | "\\Longrightarrow" | "\\implies" | "→" | "⇒"
BICONDITIONAL_SYMBOL: "\\leftrightarrow" | "\\iff" | "↔" | "⇔"

Также удалите директивы %ignore.

%ignore SPACE
%ignore COMMA
%ignore LEFT_CURLY_BRACE
%ignore RIGHT_CURLY_BRACE

Другие вопросы по теме