Комментарии 5
Молодец! СНГ! Пишите еще!
Спасибо за статью, не знал о таком интересном инструменте. У меня давно есть вопросы, возможно, у вас есть ответы. Подобные языки для доказательства теорем очень напоминают правила построения грамматик. Кто-то как-то исследовал взаимосвязь грамматических правил и доказательство теорем? И, более широкий вопрос: кто-то исследовал грамматики для построения описания научных правил и законов?
Подобные языки для доказательства теорем очень напоминают правила построения грамматик.
Да, связь есть.
Терминология
«Языки для доказательств» называются «proof assistant».
Каждый из них основан на некоторой системе типов (Coq основан на CoC — calculus of constructions, что обусловило «петушиность» названия) и предоставляет некоторую обвязку в виде тактик, синтаксического сахара и прочих вещей, без которых повесится хочется.
В этом сообщении я не провожу различий между синтаксисом и грамматикой.
С одной стороны, система типов — это как бы грамматика на стероидах. Если грамматика выделяет из множества всех слов над алфавитом язык — подмножество слов, которые являются «синтаксически/грамматически правильными», — то типизация выделяет из этого языка те, которые к тому же являются «правильно-типизированными». Неформальная иллюстрация:
любой текст =[синтаксис]=> читаемый текст =[типизация]=> осмысленный текст
При этом правила типизации могут быть более выразительными за счёт того, что на этом этапе текст уже прошел синтаксический разбор и представим в виде AST со всеми особенностями и гарантиями используемой грамматики. Грубо говоря, это как переход работы со строка на bash к работе с объектами в PowerShell.
С другой стороны, процесс доказательства соответствия текста и системе типов, и грамматике называется выводом. В частности, если рассмотреть язык, в котором грамматика тривиальная (регулярка: .*), а система типов имеет конечное число типов, то такая система типов будет сама работать как грамматика, в которой типы выполняют роль нетерминальных символов. (Правда, надо ещё кое-какие ограничения наложить на вид правил вывода, чтобы получить точное соответствие порождающим грамматикам)
В качестве отправной точки можно посмотреть работы Барендрегта по Pure/Generalized Type Systems.
Кто-то как-то исследовал взаимосвязь грамматических правил и доказательство теорем?
Я не знаю работ именно по этому вопросу. Смежные привёл выше.
На всякий случай уточню, что системы типов — частный случай логических систем (некоторые считают, что справедливо и обратное), а вывод типов и доказательства теорем — это одно и то же в этих системах. Поэтому можно почитать любую литературу по теории типов: Girard et al. «Proofs and Types», Geuvers «Introduction to Type Theory» и прочие.
кто-то исследовал грамматики для построения описания научных правил и законов?
Не знаю. Идея формально описать естественно-научные теории и типизировать их лежит на поверхности. Не думаю, что никто этим не занимался.
лично моё мнение
С практической точки зрения интересны только те формализмы, которые позволят оперировать естественными для физики вещами, вроде «утверждение выполняется в лабораторных условиях / с интересующей точностью» при том, что не считается нужным или возможным точно проговаривать, в чём именно состоят лабораторные условия и какова в цифрах интересующая точность.
P.S. Только увидел презентацию Родина «Структурализм у Гильберта и Бурбаки», цитата оттуда:
Аксиоматический метод в исполнении Бурбаки существенно отличается от аксиоматического метода Гильберта. Патрик Суппес в контексте попытки использования аксиоматического метода в физике назвал бурбакистскую версию аксиоматического метод семантическим.
Странным образом дискуссия о различии между синтаксическим и семантическим вариантами аксиоматического метода мало затронула философию математики. Сами Бурбаки, по всей очевидности, просто не придавали значения таким логическим и философским тонкостям.
Контекст цитаты: обсуждение множества неизоморфных групп, изучаемых Лагранжем. То есть, это не совсем про наш вопрос, но слова те же :)
Общественность в лице меня ожидает продолжения)
CAP, Coq и Евклид