Логика для вычислимых функций
-
Основы логики вычислимых функций (LCF)
- LCF — это инструмент для доказательства теорем, разработанный в Стэнфорде и Эдинбурге в 1970-х годах.
- Основан на теоретических принципах Даны Скотт и использует язык программирования ML.
-
Механизм и преимущества
- Теоремы представлены в виде специального типа данных «theorem».
- ML гарантирует вывод теорем с использованием только правил, заданных типом данных theorem.
- Программы на ML могут быть сложными, но достоверность теорем не зависит от их сложности.
-
Недостатки и последующие реализации
- Надежность вычислений расширена благодаря формальной верификации компилятора ML.
- Эффективность процедур доказательства требует тщательного анализа корректности.
- Отражение может быть более эффективным для доказательства правильности функций.
-
Влияния и рекомендации
- Cambridge LCF упростила логику, позволив использовать полные функции.
- HOL, HOL Light и Isabelle proof assistant поддерживают различные логики, включая Isabelle/LCF.
- Статья является заглушкой и призывает к расширению для Википедии.