解釈されない関数

数理論理学において、未解釈関数^[1]または関数記号^{[2]とは、関数の名前と}n項形式以外の特性を持たない関数のことである。関数記号は、定数や変数とともに項を形成するために使用される。

解釈されない関数の理論は、自由に生成されるため自由オブジェクトであるため自由理論と呼ばれることもあります。または、空の文の集合を持つ理論であるため空理論と呼ばれることもあります(初期代数に類似)。空でない方程式の集合を持つ理論は、方程式理論として知られています。自由理論の充足可能性問題は、統語的統一によって解決されます。後者のアルゴリズムは、Prologなどのさまざまなコンピュータ言語のインタープリタで使用されます。統語的統一は、他の特定の方程式理論の充足可能性問題のアルゴリズムでも使用されます。統一 (コンピュータサイエンス)を参照してください。

例

SMT-LIBの解釈されない関数の例として、この入力がSMT ソルバーに与えられた場合:

(宣言-fun f (Int) Int)
((= (f 10) 1) を主張する)

SMT ソルバーは「この入力は満足可能です」を返します。これは、fが解釈されない関数 (つまり、fそのシグネチャのみがわかっている) であるため、である可能性がありますf(10) = 1。ただし、以下の入力を適用すると、

(宣言-fun f (Int) Int)
((= (f 10) 1) を主張する)
((= (f 10) 42) を主張する)

SMT ソルバーは「この入力は満たされません」を返します。これはf、関数であるが同じ入力に対して異なる値を返すことができないために発生します。

自由理論の決定問題は、多くの理論をそれによって還元できるため、特に重要である。^[3]

自由理論は、合同閉包を形成する共通の部分式を検索することによって解くことができます。^[^{説明が必要}^]ソルバーには、理論を法とする充足可能性ソルバーが含まれます。

^ Bryant, Randal E.; Lahiri, Shuvendu K.; Seshia, Sanjit A. (2002). 「ラムダ式と非解釈関数によるカウンタ演算ロジックを使用したシステムのモデリングと検証」(PDF)。コンピュータ支援検証。コンピュータサイエンスの講義ノート。第 2404 巻。pp . 78–92。doi :10.1007/3-540-45657-0_7。ISBN 978-3-540-43997-4. S2CID 9471360。
^ バーダー、フランツ、ニプコウ、トビアス(1999)。用語の書き換えとその他。ケンブリッジ大学出版局。p. 34。ISBN 978-0-521-77920-3。
^ de Moura, Leonardo; Bjørner, Nikolaj (2009). 形式手法: 基礎と応用: 第 12 回ブラジル形式手法シンポジウム、SBMF 2009、ブラジル、グラマド、2009 年 8 月 19 ～ 21 日: 改訂された選定論文(PDF) 。ベルリン: Springer。ISBN 978-3-642-10452-7。