Решетка подчинения

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

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

Определение

t терм 1 _{включает} Говорят, что в себя терм t _{2 ,} если существует замена σ такая, что σ, примененная к t _{1 ,} дает t ₂ . В этом случае t ₁ также называется более общим, чем t ₂ , а t ₂ называется более конкретным, чем t ₁ , или экземпляром t ₁ .

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

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

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

Характеристики

Рис. 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 ₅ (см. рис. 1); его появление не позволяет решетке включений быть модульной и, следовательно, дистрибутивной .

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

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

• t равно объединению всех членов Gnd( t ), переименование по модулю,
• t ₁ является экземпляром t ₂ тогда и только тогда, когда Gnd( t ₁ ) ⊆ Gnd( t ₂ ),
• термины с одинаковым набором основных экземпляров равны по модулю переименования,
• если t является пересечением t1 _t1 и t2 _Gnd , то Gnd( ) = Gnd( ) _∩ ( t2 _t ),
• если t объединением t1 _t и t2 _{∪ Gnd} , то Gnd( ) ⊇ Gnd( t1 ₎ ( t2 _{является} ).

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

Рис. 5: Дистрибутивная подрешетка линейных термов

Рис. 4: М 3 построено из линейных членов

Рис. 3: N 5 построен из линейных членов

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

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

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

Источник

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