Неинтерпретируемая функция

Тип функции в математической логике

В математической логике неинтерпретируемая функция [ ^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]

Свободные теории можно решить путем поиска общих подвыражений для формирования замыкания конгруэнции . ^{[ необходимо разъяснение ]} Решатели включают решатели выполнимости по модулю теорий .

Смотрите также

Примечания

Ссылки

^ Брайант, Рэндал Э.; Лахири, Шувенду К.; Сешиа, Санджит А. (2002). «Моделирование и проверка систем с использованием логики арифметики счетчика с лямбда-выражениями и неинтерпретируемыми функциями» (PDF) . Компьютерная проверка . Конспект лекций по информатике. Том 2404. С. 78– 92. doi :10.1007/3-540-45657-0_7. ISBN 978-3-540-43997-4. S2CID 9471360.
^ Баадер, Франц ; Нипков, Тобиас (1999). Переписывание терминов и все такое . Cambridge University Press. стр. 34. ISBN 978-0-521-77920-3.
^ де Моура, Леонардо; Бьёрнер, Николай (2009). Формальные методы: основы и приложения: 12-й Бразильский симпозиум по формальным методам, SBMF 2009, Грамаду, Бразилия, 19-21 августа 2009 г.: пересмотренные избранные статьи (PDF) . Берлин: Springer. ISBN 978-3-642-10452-7.

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

[1] Брайант, Рэндал Э.; Лахири, Шувенду К.; Сешиа, Санджит А. (2002). «Моделирование и проверка систем с использованием логики арифметики счетчика с лямбда-выражениями и неинтерпретируемыми функциями» (PDF) . Компьютерная проверка . Конспект лекций по информатике. Том 2404. С. 78– 92. doi :10.1007/3-540-45657-0_7. ISBN 978-3-540-43997-4. S2CID 9471360.

[2] Баадер, Франц ; Нипков, Тобиас (1999). Переписывание терминов и все такое . Cambridge University Press. стр. 34. ISBN 978-0-521-77920-3.

[3] де Моура, Леонардо; Бьёрнер, Николай (2009). Формальные методы: основы и приложения: 12-й Бразильский симпозиум по формальным методам, SBMF 2009, Грамаду, Бразилия, 19-21 августа 2009 г.: пересмотренные избранные статьи (PDF) . Берлин: Springer. ISBN 978-3-642-10452-7.