Conversation
TonitaN
suggested changes
Nov 25, 2024
BaldiSlayer
changed the title
Collaborator
Author
|
*только заметил, что после переименования ветки pr закрылся |
TonitaN
suggested changes
Jan 1, 2025
TonitaN
left a comment
TonitaN
left a comment
There was a problem hiding this comment.
На всякий случай предупреждаю, что других ревью сегодня не будет!
TonitaN
reviewed
Jan 20, 2025
TonitaN
left a comment
TonitaN
left a comment
There was a problem hiding this comment.
Тут всё хорошо, просто уточняю последние штрихи.
| author: Евдокимов Никита | ||
| id: 249 | ||
| questions: | ||
| - 'Какой вывод о завершаемости системы переписывания термов можно сделать, если не получается применить порядок Кнута-Бендикса или подобрать числовую функцию? |
There was a problem hiding this comment.
*или подобрать монотонные функции, убывающие при переписывании
| questions: | ||
| - 'Какой вывод о завершаемости системы переписывания термов можно сделать, если не получается применить порядок Кнута-Бендикса или подобрать числовую функцию? | ||
| ' | ||
| - answer: 'Для нетеровой системы переписывания термов свойства конфлюэнтности и локальной конфлюэнтности эквивалентны. То есть если система не имеет бесконечных цепочек переписывания и конфлюэнтна (локально-конфлюэнтна) => также локально-конфлюэнтна (конфлюэнтна). Система переписывания термов называется локально-конфлюэнтной, если для любых термов t_1, t_2, t_3 таких, что t_1 -> t_2 и t_1 -> t_3, найдется терм t_4, для которого выполяется t_2 ->* t_4 и t_3 ->* t_4 |
There was a problem hiding this comment.
ну, в одну сторону эта эквивалентность тривиальна, достаточно написать только в другую (локальная -> глобальная конфлюэнтность)
There was a problem hiding this comment.
И хотелось бы хотя бы один пример локально конфлюэнтной системы.
| - answer: 'Определим расширение подстановки σ | ||
| [x, σ] = xσ; | ||
| Для термов вида f(t_1, ..., t_n) результат подстановки определяется как f_A([t_1, σ], ..., [t_n, σ]), где f_A — интерпретация функции f в алгебре A. | ||
| Система переписывания термов {l_i → r_i} совместна с фундированной монотонной алгеброй A, если для всех i и любых подстановок σ выполняется [l_i, σ] > [r_i, σ], что означает, что значение левой части правила l_i строго больше значения правой части r_i после применения одной и той же подстановки. |
| questions: | ||
| - 'Что означает совместность системы переписывания термов с фундированной монотонной алгеброй и какое условие при этом выполняется? | ||
| ' | ||
| - answer: 'Фундированная монотонная алгебра над множеством функциональных символов F — это фундированное множество ⟨A, >⟩ такое, что для каждого функционального символа f ∈ F существует функция F_A: A^n → A, строго монотонная по каждому из аргументов |
| questions: | ||
| - 'Полная система переписывания термов | ||
| ' | ||
| - answer: 'Система переписывания термов называется нетеровой, если не существует бесконечной цепочки редукций t_1 -> t_2 -> t_3 -> ... . |
There was a problem hiding this comment.
Объяснить ещё, как это связано с нётеровыми порядками (мне видится, что через замыкание отношения переписываемости).
| questions: | ||
| - 'Отношение редукции и порядок редукции | ||
| ' | ||
| - answer: 'Система переписывания термов называется конфлюэнтной, если для любых термов t_1, t_2, t_3, таких что t_1 переписывается (->*) в t_2 и t_1 ->* в t_3, найдется терм t_4, для которого справедливо, что t_2 ->* в t_4 и t_3 ->* в t_4. |
| questions: | ||
| - 'Что такое сопоставление с образцом в системах переписывания термов? | ||
| ' | ||
| - answer: 'Пусть s_1 -> t_1 - два правила переписывания, которые без потери общности не имеют общих переменных, то есть V(s_1) и V(s_2) не имеют пересечений. Пусть u - некоторое такое вхождение терма в s_1, что терм s_1/u не является переменной и унифицируем с s_2. Тогда пара термов σ(s_1[u <- t_2]) и σ(t_1), где σ - наиболее общий унификатор s_1/u и s_2, называется критической парой, полученной в результате совмещения правил s_2 -> t_2 и s_1 -> t_1 |
There was a problem hiding this comment.
Кстати, в БЗ нет ничего про унификацию, а ссылки на унификацию есть. Может, добавить?
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.