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

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

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

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

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

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

Операция join и meet в этой решетке называются антиобъединением и объединением соответственно. Переменная 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 , справедливы следующие свойства: ^[2]

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

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

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

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

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