制約を設定する

数学と理論計算機科学において、集合制約とは項の集合間の方程式または不等式である。数値間の方程式系（不等式）と同様に、集合制約系を解く方法が研究されている。異なるアプローチでは、集合上の異なる演算子（「∪」、「∩」、「\」、関数適用など）^{[注 1]}と、集合式間の異なる（不）等式関係（「=」、「⊆」、「⊈」など）が認められる。

集合制約のシステムは、基底項の（特に無限の）集合を記述するのに役立ちます。^{[注 2]} これらは、プログラム解析、抽象解釈、および型推論で発生します。

各正規木文法は、その最小解が文法の木言語に対応するように、集合包含のシステムに体系的に変換できます。

例えば、文法（終端記号と非終端記号はそれぞれ小文字と大文字の頭文字で示される）と規則

集合包含システム（定数と変数はそれぞれ小文字と大文字の頭文字で示される）に変換されます。

このシステムには、最小限の解があります。つまり、「L ( N )」は、上記のツリー文法の非終端記号Nに対応するツリー言語を表します。

システムの最大解は自明であり、すべての項の集合をすべての変数に割り当てます。

• Aiken, A. (1995). セット制約: 結果、アプリケーション、および将来の方向性 (技術レポート). バークレー大学。
• Aiken, A., Kozen, D., Vardi, M., Wimmers, EL (1993 年 5 月)。セット制約の複雑性 (技術レポート)。コーネル大学コンピュータサイエンス学部。93–1352。{{cite tech report}}: CS1 maint: multiple names: authors list (link)
• Aiken, A., Kozen, D., Vardi, M., Wimmers, EL (1994). 「セット制約の複雑性」。Computer Science Logic'93 . LNCS. Vol. 832. Springer. pp. 1–17.{{cite book}}: CS1 maint: multiple names: authors list (link)
• Aiken, A., Wimmers, EL (1992)。「集合制約のシステムの解決 (拡張要約)」。第 7 回 IEEE コンピュータ サイエンスにおける論理シンポジウム。pp. 329–340。{{cite book}}: CS1 maint: multiple names: authors list (link)
• Bachmair, Leo, Ganzinger, Harald, Waldmann, Uwe (1992).セット制約はモナディッククラスです(技術レポート). Max-Planck-Institut für Informatik. p. 13. CiteSeerX  10.1.1.32.3739 . MPI-I-92-240.{{cite tech report}}: CS1 maint: multiple names: authors list (link)
• Bachmair, Leo, Ganzinger, Harald, Waldmann, Uwe (1993)。「セット制約はモナディッククラスです」。第 8 回 IEEE コンピュータサイエンスにおけるロジックシンポジウム。pp. 75–83。{{cite book}}: CS1 maint: multiple names: authors list (link)
• Charatonik, W. (1994 年 9 月)。「いくつかの等式理論における集合制約」。計算論理における制約に関する第 1 回国際会議 (CCL) 会議議事録。LNCS。第 845 巻。Springer。pp. 304–319。
• Charatonik, Witold; Podelski, Andreas (2002). 「交差を伴う制約のセット」.情報と計算. 179 (2): 213–229. doi : 10.1006/inco.2001.2952 .
• Charatonik, W., Podelski, A. (1998). Tobias Nipkow (編).共定値集合制約. LNCS 1379. Springer-Verlag. pp. 211–225.{{cite book}}: CS1 maint: multiple names: authors list (link)
• Charatonik, W., Talbot, J.-M. (2002). Tison, S. (編). Atomic Set Constraints with Projection . LNCS 2378. Springer. pp. 311–325.{{cite book}}: CS1 maint: multiple names: authors list (link)
• Gilleron, R.、Tison, S.、Tommasi, M. (1993)。「ツリーオートマトンを使用したセット制約システムの解決」。第 10 回コンピュータサイエンスの理論的側面に関する年次シンポジウム。LNCS。第 665 巻。Springer。pp. 505–514。{{cite book}}: CS1 maint: multiple names: authors list (link)
• Heintze, N., Jaffar, J. (1990)。「セット制約のクラスの決定手順 (拡張要約)」。第 5 回 IEEE コンピュータ サイエンスの論理に関するシンポジウム。pp. 42–51。{{cite book}}: CS1 maint: multiple names: authors list (link)
• Heintze, N., Jaffar, J. (1991 年 2 月)。セット制約のクラスの決定手順(技術レポート)。カーネギーメロン大学コンピュータサイエンス学部。{{cite tech report}}: CS1 maint: multiple names: authors list (link)
• Kozen, D. (1993). 「セット制約の論理的側面」(PDF) . Computer Science Logic'93 . LNCS. Vol. 832. pp. 175–188.
• Kozen, D. (1994). 「セット制約とロジックプログラミング」CCL . LNCS. Vol. 845.
• Dexter Kozen (1998). 「セット制約とロジックプログラミング」.情報と計算. 142 : 2–25. doi : 10.1006/inco.1997.2694 .
• Uribe, TE (1992)。「セット制約を使用したソートされた統一」。Proc . CADE–11。LNCS。第 607 巻。pp. 163–177。

• Aiken, A., Kozen, D., Wimmers, EL (1993 年 6 月)。負の制約を持つ集合制約システムの決定可能性 (技術レポート)。コーネル大学コンピュータ サイエンス学部。93–1362。{{cite tech report}}: CS1 maint: multiple names: authors list (link)
• Charatonik, W.、Pacholski, L. (1994 年 7 月)。「等式による負集合制約」。第 9 回 IEEE コンピュータ サイエンスにおける論理シンポジウム。pp. 128–136。{{cite book}}: CS1 maint: multiple names: authors list (link)
• R. Gilleron、S. Tison、M. Tommasi (1993)。「否定サブセット関係を持つセット制約システムの解決」。第 34 回コンピュータ サイエンスの基礎に関するシンポジウムの議事録。372 ～ 380 ページ。
• Gilleron, R., Tison, S., Tommasi, M. (1993).否定されたサブセット関係を持つセット制約システムの解決(技術レポート). Laboratoire d'Informatique Fondamentale de Lille. IT 247.{{cite tech report}}: CS1 maint: multiple names: authors list (link)
• Stefansson, K. (1993 年 8 月)。負の制約を持つ集合制約システムは NEXPTIME 完全です(技術レポート)。コーネル大学コンピュータ サイエンス学部。93–1380。
• Stefansson, K. (1994)。「負の制約を持つ集合制約システムは NEXPTIME 完全である」。第 9 回 IEEE コンピュータ サイエンスの論理に関するシンポジウム。pp. 137–141。