В математической логике неинтерпретируемая функция [1] или символ функции [2] — это функция, которая не имеет никакого другого свойства, кроме своего имени и n-арной формы. Функциональные символы используются вместе с константами и переменными для формирования термов .
Теорию неинтерпретируемых функций также иногда называют свободной теорией , поскольку она свободно порождается и, таким образом, является свободным объектом , или пустой теорией , являющейся теорией , имеющей пустой набор предложений (по аналогии с исходной алгеброй ). Теории с непустым набором уравнений известны как эквациональные теории . Проблема выполнимости свободных теорий решается путем синтаксической унификации ; алгоритмы для последнего используются интерпретаторами различных компьютерных языков, например Пролога . Синтаксическая унификация также используется в алгоритмах решения проблемы выполнимости некоторых других эквациональных теорий, см. Унификация (информатика) .
В качестве примера неинтерпретируемых функций для 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]
Свободные теории могут быть решены путем поиска общих подвыражений для формирования конгруэнтного замыкания . [ нужны разъяснения ] Решатели включают в себя решатели теорий выполнимости по модулю .