В математической логике неинтерпретируемая функция [ 1] или символ функции [2] — это функция, которая не имеет других свойств, кроме своего имени и n-арной формы. Символы функций используются вместе с константами и переменными для формирования терминов .
Теорию неинтерпретируемых функций иногда называют свободной теорией , поскольку она свободно генерируется, и, таким образом, свободным объектом , или пустой теорией , поскольку она имеет пустое множество предложений (по аналогии с исходной алгеброй ). Теории с непустым множеством уравнений известны как эквациональные теории . Проблема выполнимости для свободных теорий решается синтаксической унификацией ; алгоритмы для последней используются интерпретаторами для различных компьютерных языков, таких как Пролог . Синтаксическая унификация также используется в алгоритмах для проблемы выполнимости для некоторых других эквациональных теорий, см. Унификация (компьютерная наука) .
В качестве примера неинтерпретируемых функций для SMT-LIB , если эти входные данные подаются решателю SMT :
(declare-fun f (Int) Int)(утверждаем (= (f 10) 1))
решатель SMT вернет "Эти входные данные выполнимы". Это происходит, потому что f
это неинтерпретируемая функция (т. е. все, что известно о ней, f
это ее сигнатура ), поэтому возможно, что f(10) = 1
. Но, применяя входные данные ниже:
(declare-fun f (Int) Int)(утверждаем (= (f 10) 1))(утверждаем (= (f 10) 42))
решатель SMT вернет «Этот ввод невыполним». Это происходит потому , что f
, будучи функцией, она никогда не может возвращать разные значения для одного и того же ввода.
Проблема принятия решений для свободных теорий особенно важна, поскольку с ее помощью можно сократить множество теорий. [3]
Свободные теории можно решить путем поиска общих подвыражений для формирования замыкания конгруэнции . [ необходимо разъяснение ] Решатели включают решатели выполнимости по модулю теорий .