Установить ограничение

В математике и теоретической информатике представляет ограничение набора собой уравнение или неравенство между наборами терминов .Подобно системам ( в ) уравнений между числами, изучаются методы решения систем заданных ограничений. Разные подходы допускают разные операторы (например, «∪», «∩», «\» и применение функций). ^{[примечание 1]} о множествах и различных отношениях (в) уравнениях (например, «=", «⊆» и «⊈») между выражениями множеств.

Системы ограничений множеств полезны для описания (в частности, бесконечных) множеств основных терминов . ^{[примечание 2]}Они возникают при анализе программ, абстрактной интерпретации и выводе типов .

Связь с обычными древовидными грамматиками

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

Например, грамматика (терминальные и нетерминальные символы, обозначаемые строчными и прописными инициалами соответственно) с правилами

Бул _Джи	→ ложь
Бул _Джи	→ правда
Список _G	→ ноль
Список _G	→ минусы ( Bool _G , BList _G )
BList1 _G	→ минусы ( правда , BList _G )
BList1 _G	→ минусы ( ложь , BList1 _G )

преобразуется в систему включения множеств (константы и переменные обозначаются строчными и прописными инициалами соответственно):

Бул _С	⊇ ложь
Бул _С	⊇ правда
Список _S	⊇ ноль
Список _S	⊇ минусы ( Bool _S , BList _S )
BList1 _S	⊇ минусы ( правда , BList _S )
BList1 _S	⊇ минусы ( ложь , BList1 _S )

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

Бул _С	= L ( бул _G )	= { ложь , правда }
Список _S	= L ( BList _G )	= { ноль , минусы ( ложь , ноль ), минусы ( истина , ноль ), минусы ( ложь , минусы ( ложь , ноль )), ... }
BList1 _S	= L ( BList1 _G )	= { ноль , минусы ( истина , ноль ), минусы ( истина , минусы ( ложь , ноль )),... }

Максимальное решение системы тривиально; он присваивает каждой переменной набор всех терминов.

Литература

Эйкен, А. (1995). Установите ограничения: результаты, применение и будущие направления (технический отчет). унив. Беркли.
Айкен А., Козен Д., Варди М., Виммерс Э.Л. (май 1993 г.). Сложность установленных ограничений (Технический отчет). Факультет компьютерных наук Корнелльского университета. 93–1352. {{cite tech report}}: CS1 maint: несколько имен: список авторов ( ссылка )
Айкен А., Козен Д., Варди М., Виммерс Э.Л. (1994). «Сложность установленных ограничений». Информатика Логика'93 . ЛНКС. Том. 832. Спрингер. стр. 1–17. {{cite book}}: CS1 maint: несколько имен: список авторов ( ссылка )
Айкен А., Виммерс Э.Л. (1992). «Решение систем множественных ограничений (расширенное резюме)». Седьмой ежегодный симпозиум IEEE по логике в информатике . стр. 329–340. {{cite book}}: CS1 maint: несколько имен: список авторов ( ссылка )
Бахмайр, Лео, Ганцингер, Харальд, Вальдманн, Уве (1992). Установить ограничения — это монадический класс (технический отчет). Институт компьютерных наук Макса Планка. п. 13. CiteSeerX 10.1.1.32.3739 . МПИ-И-92-240. {{cite tech report}}: CS1 maint: несколько имен: список авторов ( ссылка )
Бахмайр, Лео, Ганцингер, Харальд, Вальдманн, Уве (1993). «Ограничения установки — это монадический класс». Восьмой ежегодный симпозиум IEEE по логике в информатике . стр. 75–83. {{cite book}}: CS1 maint: несколько имен: список авторов ( ссылка )
Харатоник, В. (сентябрь 1994 г.). «Установите ограничения в некоторых эквациональных теориях». Учеб. 1-й Межд. Конф. по ограничениям в вычислительной логике (CCL) . ЛНКС. Том. 845. Спрингер. стр. 304–319.
Харатоник, Витольд; Подельски, Андреас (2002). «Установить ограничения с пересечением» . Информация и вычисления . 179 (2): 213–229. дои : 10.1006/inco.2001.2952 .
Харатоник В., Подельски А. (1998). Тобиас Нипков (ред.). Соопределенные ограничения набора . LNCS 1379. Шпрингер-Верлаг. стр. 211–225. {{cite book}}: CS1 maint: несколько имен: список авторов ( ссылка )
Харатоник В., Талбот Ж.-М. (2002). Тайсон, С. (ред.). Ограничения атомарного набора с проекцией . LNCS 2378. Спрингер. стр. 311–325. {{cite book}}: CS1 maint: несколько имен: список авторов ( ссылка )
Гиллерон Р., Тайсон С., Томмаси М. (1993). «Решение систем множественных ограничений с использованием древовидных автоматов». 10-й ежегодный симпозиум по теоретическим аспектам информатики . ЛНКС. Том. 665. Спрингер. стр. 505–514. {{cite book}}: CS1 maint: несколько имен: список авторов ( ссылка )
Хайнце Н., Джаффар Дж. (1990). «Процедура принятия решения для класса ограничений множества (расширенное резюме)». Пятый ежегодный симпозиум IEEE по логике в информатике . стр. 42–51. {{cite book}}: CS1 maint: несколько имен: список авторов ( ссылка )
Хайнце Н., Джаффар Дж. (февраль 1991 г.). Процедура принятия решения для класса установленных ограничений (технический отчет). Школа компьютерных наук Университета Карнеги-Меллон. {{cite tech report}}: CS1 maint: несколько имен: список авторов ( ссылка )
Козен, Д. (1993). «Логические аспекты ограничений набора» (PDF) . Информатика Логика'93 . ЛНКС. Том. 832. стр. 175–188.
Козен, Д. (1994). «Установка ограничений и логическое программирование». ККЛ . ЛНКС. Том. 845.
Декстер Козен (1998). «Установка ограничений и логическое программирование» . Информация и вычисления . 142 : 2–25. дои : 10.1006/inco.1997.2694 .
Урибе, Т.Е. (1992). «Сортированное объединение с использованием ограничений набора» . Учеб. КАД–11 . ЛНКС. Том. 607. стр. 163–177.

Литература о негативных ограничениях

Айкен А., Козен Д., Виммерс Э.Л. (июнь 1993 г.). Разрешимость систем заданных ограничений с отрицательными ограничениями (Технический отчет). Факультет компьютерных наук Корнелльского университета. 93–1362. {{cite tech report}}: CS1 maint: несколько имен: список авторов ( ссылка )
Харатоник В., Пачольски Л. (июль 1994 г.). «Отрицательные ограничения множества с равенством». Девятый ежегодный симпозиум IEEE по логике в информатике . стр. 128–136. {{cite book}}: CS1 maint: несколько имен: список авторов ( ссылка )
Р. Гиллерон; С. Тайсон; М. Томмаси (1993). «Решение систем ограничений множеств с отрицательными отношениями подмножеств». Материалы 34-го симпозиума. по основам информатики . стр. 372–380.
Гиллерон Р., Тайсон С., Томмаси М. (1993). Решение систем множественных ограничений с отрицательными связями подмножеств (Технический отчет). Лаборатория фундаментальной информатики Лилля. ИТ 247. {{cite tech report}}: CS1 maint: несколько имен: список авторов ( ссылка )
Стефанссон, К. (август 1993 г.). Системы множественных ограничений с отрицательными ограничениями являются NEXPTIME-Complete (Технический отчет). Факультет компьютерных наук Корнелльского университета. 93–1380.
Стефанссон, К. (1994). «Системы множественных ограничений с отрицательными ограничениями являются NEXPTIME-завершенными». Девятый ежегодный симпозиум IEEE по логике в информатике . стр. 137–141.

Примечания

^ Если f - n -арный функциональный символ, допущенный в термине, то " f ( E ₁ ,..., E _n )" - это выражение множества, обозначающее набор { f ( t ₁ ,..., t _n ) : t ₁ ∈ E ₁ и ... и t _n ∈ En _} , где E ₁ ,..., En _— поочередно заданные выражения.
^ Это похоже на описание, например, рационального числа как решения уравнения a ⋅ x + b = 0 с целыми коэффициентами a , b .

Эта математической логике статья, посвященная , незавершена . Вы можете помочь Википедии, расширив ее .

П ≟ НП

Эта теоретической информатикой, статья, связанная с незавершена . Вы можете помочь Википедии, расширив ее .

[1] Если f - n -арный функциональный символ, допущенный в термине, то " f ( E ₁ ,..., E _n )" - это выражение множества, обозначающее набор { f ( t ₁ ,..., t _n ) : t ₁ ∈ E ₁ и ... и t _n ∈ En _} , где E ₁ ,..., En _— поочередно заданные выражения.

[2] Это похоже на описание, например, рационального числа как решения уравнения a ⋅ x + b = 0 с целыми коэффициентами a , b .

[примечание 1]

[примечание 2]