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

Установить ограничения, полученные из абстрактная интерпретация из Collatz алгоритм

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

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

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

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

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

Boolграмм	→ ложный
Boolграмм	→ истинный
BListграмм	→ ноль
BListграмм	→ минусы(Boolграмм,BListграмм)
BList1грамм	→ минусы(истинный,BListграмм)
BList1грамм	→ минусы(ложный,BList1грамм)

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

BoolS	⊇ ложный
BoolS	⊇ истинный
BListS	⊇ ноль
BListS	⊇ минусы(BoolS,BListS)
BList1S	⊇ минусы(истинный,BListS)
BList1S	⊇ минусы(ложный,BList1S)

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

BoolS	= L(Boolграмм)	= { ложный, истинный }
BListS	= L(BListграмм)	= { ноль, минусы(ложный,ноль), минусы(истинный,ноль), минусы(ложный,минусы(ложный,ноль)), ... }
BList1S	= L(BList1грамм)	= { ноль, минусы(истинный,ноль), минусы(истинный,минусы(ложный,ноль)),... }

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

Литература

• Айкен, А. (1995). Установите ограничения: результаты, приложения и будущие направления (Технический отчет). Univ. Беркли.
• Aiken, A., Kozen, D., Vardi, M., Wimmers, E.L. (Май 1993 г.). Сложность установленных ограничений (Технический отчет). Департамент компьютерных наук Корнельского университета. 93–1352.
• Aiken, A., Kozen, D., Vardi, M., Wimmers, E.L. (1994). «Сложность установки ограничений». Логика информатики'93. LNCS. 832. Springer. С. 1–17.
• Эйкен, А., Виммерс, Э. (1992). «Решение систем заданных ограничений (расширенная аннотация)». Седьмой ежегодный симпозиум IEEE по логике в компьютерных науках. С. 329–340.
• Бахмар, Лео, Ганцингер, Харальд, Вальдманн, Уве (1992). Ограничения набора - это монадический класс (Технический отчет). Max-Planck-Institut für Informatik. п. 13. CiteSeerX  10.1.1.32.3739. МПИ-И-92-240.
• Бахмар, Лео, Ганцингер, Харальд, Вальдманн, Уве (1993). «Ограничения множества - это монадический класс». Восьмой ежегодный симпозиум IEEE по логике в компьютерных науках. С. 75–83.
• Чаратоник, В. (сентябрь 1994 г.). «Установить ограничения в некоторых эквациональных теориях». Proc. 1-й Int. Конф. по ограничениям в вычислительной логике (CCL). LNCS. 845. Springer. С. 304–319.
• Чаратоник, Витольд; Подельски, Андреас (2002). «Установить ограничения с пересечением». Информация и вычисления. 179 (2): 213–229. Дои:10.1006 / inco.2001.2952.
• Чаратоник, В., Подельски, А. (1998). Тобиас Нипков (ред.). Коопределенные ограничения множества. LNCS 1379. Springer-Verlag. С. 211–225.
• Charatonik, W., Talbot, J.-M. (2002). Тисон, С. (ред.). Ограничения атомарного множества с проекцией. LNCS 2378. Springer. С. 311–325.
• Гиллерон, Р., Тисон, С., Томмази, М. (1993). «Решение систем заданных ограничений с использованием древовидных автоматов». 10-й ежегодный симпозиум по теоретическим аспектам информатики. LNCS. 665. Springer. С. 505–514.
• Хайнце, Н., Джаффар, Дж. (1990). «Процедура принятия решения для класса установленных ограничений (расширенная аннотация)». Пятый ежегодный симпозиум IEEE по логике в компьютерных науках. С. 42–51.
• Хайнце, Н., Джаффар, Дж. (Февраль 1991 г.). Процедура принятия решения для класса установленных ограничений (Технический отчет). Школа компьютерных наук Университета Карнеги-Меллона.
• Козен, Д. (1993). «Логические аспекты ограничений множества» (PDF). Логика информатики'93. LNCS. 832. С. 175–188.
• Козен, Д. (1994). «Задать ограничения и логическое программирование». CCL. LNCS. 845.
• Декстер Козен (1998). «Задать ограничения и логическое программирование». Информация и вычисления. 142: 2–25. Дои:10.1006 / inco.1997.2694.
• Урибе, Т. (1992). «Сортированное объединение с использованием заданных ограничений». Proc. CADE – 11. LNCS. 607. С. 163–177.

Литература по отрицательным ограничениям

• Айкен, А., Козен, Д., Виммерс, Э.Л. (Июнь 1993 г.). Разрешимость систем заданных ограничений с отрицательными ограничениями. (Технический отчет). Департамент компьютерных наук Корнельского университета. 93–1362.
• Чаратоник В., Пачольски Л. (июль 1994 г.). «Ограничения отрицательного множества с равенством». Девятый ежегодный симпозиум IEEE по логике в компьютерных науках. С. 128–136.
• Р. Гиллерон; С. Тисон; М. Томмази (1993). «Решение систем множественных ограничений с отрицательными отношениями подмножества». Материалы 34-го симп. по основам информатики. С. 372–380.
• Гиллерон, Р., Тисон, С., Томмази, М. (1993). Решение систем множественных ограничений с отрицательными отношениями подмножеств (Технический отчет). Laboratoire d'Informatique Fondamentale de Lille. Елизавета 247.
• Стефанссон, К. (август 1993 г.). Системы заданных ограничений с отрицательными ограничениями завершены NEXPTIME (Технический отчет). Департамент компьютерных наук Корнельского университета. 93–1380.
• Стефанссон, К. (1994). "Системы заданных ограничений с отрицательными ограничениями завершаются NEXPTIME". Девятый ежегодный симпозиум IEEE по логике в компьютерных науках. С. 137–141.

Примечания

1. Если ж является п-арная функция символа, допускаемая в члене, то "ж(E₁,...,E_п) "- выражение множества, обозначающее множество { ж(т₁,...,т_п) : т₁∈E₁ и и т_п∈E_п }, куда E₁,...,E_п являются заданными выражениями по очереди.
2. Это похоже на описание, например, а Рациональное число как решение уравнения а⋅Икс + б = 0, причем целое число коэффициенты а, б.