Решетка поглощения

редактировать
Рис. 1: Немодульная подрешетка N 5 в решетке подчинения

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

Содержание

  • 1 Определение
  • 2 свойства
  • 3 'Подрешетка' линейных членов
  • 4 Происхождение
  • 5 ссылки

Определение

Термин т 1 называется подводить слагаемое т 2, если подстановка σ такая, что σ применяется к т 1 урожайности т 2. В этом случае t 1 также называется более общим, чем t 2, а t 2 называется более конкретным, чем t 1 или экземпляром t 1.

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

  • считать два члена равными, если они различаются только именами переменных,
  • добавить искусственный минимальный элемент Ω ( сверхуказанный термин), который считается более конкретным, чем любой другой термин.

Эта решетка называется решеткой включения. Два члена называются объединяемыми, если их пересечение отличается от Ω.

Свойства

Рис. 2: Часть решетки включения, показывающая, что члены f ( a, x), f ( x, x) и f ( x, c) попарно унифицируемы, но не одновременно. ( Е опущено для краткости.)

Присоединиться и операция встречается в этой решетке называется антиунификациями и унификация, соответственно. Переменная x и искусственный элемент Ω - это верхний и нижний элементы решетки соответственно. Каждый основной член, то есть каждый член без переменных, является атомом решетки. Решетка имеет бесконечные нисходящие цепи, например x, g ( x), g ( g ( x)), g ( g ( g ( x))),..., но не бесконечные восходящие.

Если f - двоичный функциональный символ, g - унарный функциональный символ, а x и y обозначают переменные, то термины f ( x, y), f ( g ( x), y), f ( g ( x), g ( y)), f ( x, x) и f ( g ( x), g ( x)) образуют минимальную немодулярную решетку N 5 (см. рис. 1); его внешний вид препятствует тому, чтобы решетка подчинения была модульной, а следовательно, и распределительной.

Совокупность сроков, унифицированных с данным термином, не обязательно должна быть закрыта в отношении соответствия; Рис. 2 показан контрпример.

Обозначая Gnd ( t) множество всех основных экземпляров терма t, выполняются следующие свойства:

  • t равно объединению всех членов Gnd ( t) по модулю переименования,
  • t 1 является экземпляром t 2 тогда и только тогда, когда Gnd ( t 1) является подмножеством Gnd ( t 2),
  • члены с одинаковым набором наземных экземпляров равны по модулю переименования,
  • если t - пересечение t 1 и t 2, то Gnd ( t) - пересечение Gnd ( t 1) и Gnd ( t 2),
  • если t является объединением t 1 и t 2, то Gnd ( t) включает объединение Gnd ( t 1) и Gnd ( t 2).

«Подрешетка» линейных членов

Рис. 5. Дистрибутивная подрешетка линейных членов
Рис. 4: M 3 построен из линейных членов
Рис. 3: N 5 построен из линейных членов

Набор линейных членов, то есть терминов без нескольких вхождений переменной, является подмножеством решетки включения и сам по себе является решеткой. Эта решетка также включает N 5 и минимальную недистрибутивную решетку M 3 в качестве подрешеток (см. Рис. 3 и рис. 4) и, следовательно, не является модулярной, не говоря уже о дистрибутивной.

Операция meet всегда дает тот же результат в решетке всех членов, что и в решетке линейных членов. Операция соединения в решетке всех членов всегда дает экземпляр соединения в решетке линейных членов; например, (основные) члены f ( a, a) и f ( b, b) имеют соединение f ( x, x) и f ( x, y) в решетке всех терминов и в решетке линейных членов, соответственно. Поскольку операции соединения в общем не согласуются, решетка линейных членов не является собственно подрешеткой решетки всех терминов.

Соединение и встреча двух собственных линейных членов, т. Е. Их анти-объединение и объединение, соответствует пересечению и объединению их множеств путей, соответственно. Следовательно, любая подрешетка решетки линейных термов, не содержащая Ω, изоморфна решетке множеств и, следовательно, дистрибутивна (см. Рис. 5).

Происхождение

По-видимому, решетка подчинения была впервые исследована Гордоном Д. Плоткиным в 1970 году.

Ссылки

Последняя правка сделана 2024-01-11 03:10:57
Содержание доступно по лицензии CC BY-SA 3.0 (если не указано иное).
Обратная связь: support@alphapedia.ru
Соглашение
О проекте