Вычислимая модель математики

[alex55555]

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

Собственно пока вижу одно ограничение - время. Просто нужно выделить много времени, но никто не выделяет. В том числе на неопределяемые понятия (которые, видимо, можно задать в виде аксиом). Или я ошибаюсь? Кто-нибудь может подсказать?

[Someone]

alex55555 в сообщении #1376044 писал(а):

Просто нужно выделить много времени

Бесконечно много. И памяти.

[alex55555]

Someone в сообщении #1376237 писал(а):

Бесконечно много. И памяти.

Имелась в виду обычная оцифровка знаний. Изложение доказательства не в свободной форме, но в виде набора правил, следуя которым программа подтверждает выполнимость означенной ими логической цепочки. Никакой магии, никакого ИИ. Просто единый и проверяемый компьютером формат утверждений и теорем.

Отличие от общепринятого - устраняются неоднозначности и исправляется масса мелких ошибок. Ну и возможно крупных.

[Sender]

В принципе, эта идея не нова и когда-то получила выражение в виде QED manifesto.

[alex55555]

Sender в сообщении #1376266 писал(а):

В принципе, эта идея не нова и когда-то получила выражение в виде QED manifesto.

Спасибо, интересно.

Правда результат:

Цитата:

The project seems to have died in 1996, never having produced more than discussions and plans.

Не впечатляет. Ну и по причинам они тоже ссылаются на:

Цитата:

Very few people are working on formalization of mathematics.

То есть на то самое время, которое просто не выделили.

Так же в частностях ссылаются на недоработанность инструментов:

Цитата:

the paper finds that the major contenders, Mizar, HOL, and Coq, have serious shortcomings in their abilities to express mathematics.

Но здесь всё же проблема людская - надо в рамках существующих инструментов выразить то, что выражается произвольным образом. Да, ограничения мешают, но принципиально-то ничего не запрещают.

[arseniiv]

Есть много таких проектов, и везде мало (хотя с какой точки зрения?) людей, вот ещё Metamath например до кучи, но это всё соломинки большого снопа, наверняка кто-то собирает полный список где-нибудь. Присоединяйтесь к одному из них, например.

[alex55555]

arseniiv в сообщении #1376368 писал(а):

Есть много таких проектов, и везде мало (хотя с какой точки зрения?) людей, вот ещё Metamath например до кучи, но это всё соломинки большого снопа, наверняка кто-то собирает полный список где-нибудь. Присоединяйтесь к одному из них, например.

Частной инициативой тут не поможешь. Хотя для обучения, возможно, часть систем использовать можно. Но здесь опять встаёт приличная проблема выбора - нужно учить языки и средства каждой из подобных систем, что бы потом понять, а что же в них реально есть. Довольно долгое занятие. Но если пройти этот путь, то да, потом можно уже своё там "конспектировать", просто что бы по быстрому вспомнить, найти. Но опять же становится важным, как там реализован поиск. В целом разношерстность и отсутствие стандарта всё убивает. Жалко, что нет единого подхода.

[arseniiv]

Потому что люди не договорились, что нужно, а что не нужно, что более полезно иметь, и каких следствий этого иметь непозволительно. Может быть, договорятся, ну хотя бы в этом можете помочь. Конечно, тогда придётся изучать даже больше, чем нужно чтобы пользоваться какой-то одной из систем — ведь их придётся сравнивать, а ещё иметь представление о гипотетически возможных…

[alex55555]

arseniiv в сообщении #1376460 писал(а):

ведь их придётся сравнивать, а ещё иметь представление о гипотетически возможных…

А вы, кстати, не имеете представления о их наборе языков? Я поверхностно смотрел одну из систем, обнаружил функциональный язык программирования, притянутый к задаче формализации знаний. Много специфичного пришлось добавить и чистота функционального подхода куда-то делась. Подумалось про пролог, мне кажется он здесь весьма удобен (да и вообще очень прост, даже в сравнении с функциональными языками), но в математике он, видимо, не прижился, а жаль.

[arseniiv]

alex55555 в сообщении #1376495 писал(а):

А вы, кстати, не имеете представления о их наборе языков?

Поверхностно знаю Metamath, наверно можно сказать. Ну там подход, конечно, разительно отличается от систем, основанных на мощных теориях типов: это почти общего вида система переписывания строк, но которая умеет говорить о метапеременных (таких переменных, вместо которых предполагается подставлять предметные переменные) и ограничениях на подстановку вместо этих переменных, а всё остальное лежит на формализующих, в частности однозначность чтения языковых конструкций. Одной из целей Metamath было сделать саму программу (или только проверяющее выводы ядро? точно не знаю) простой и маленькой, потому например строки, а не алгебра термов, и потому явные подстановки и никакого понятия в самой программе о связанных вхождениях переменных.

С прологом есть проблемы, как понимаю, потому что механизм вывода слабоват, и влиять на него достаточно высокоуровневым образом трудно. Чем он специфически к формализации математики может лучше подходить кроме этого механизма, неясно.

[alex55555]

arseniiv в сообщении #1376570 писал(а):

Поверхностно знаю Metamath, наверно можно сказать. Ну там подход, конечно, разительно отличается от систем, основанных на мощных теориях типов: это почти общего вида система переписывания строк, но которая умеет говорить о метапеременных (таких переменных, вместо которых предполагается подставлять предметные переменные) и ограничениях на подстановку вместо этих переменных, а всё остальное лежит на формализующих, в частности однозначность чтения языковых конструкций.

А какая может быть неоднозначность, если языковые конструкции интерпретирует компьютер? Или модель исполнения там замороченная и её сложно понять, а на этом основании вылазят недопонимания, трактуемые как неоднозначность восприятия?

arseniiv в сообщении #1376570 писал(а):

Одной из целей Metamath было сделать саму программу (или только проверяющее выводы ядро? точно не знаю) простой и маленькой, потому например строки, а не алгебра термов, и потому явные подстановки и никакого понятия в самой программе о связанных вхождениях переменных.

Простота модели исполнения очень нужна, она позволяет людям с меньшим опытом полноценно использовать систему. Но вот тогда про неоднозначность выше непонятно.

arseniiv в сообщении #1376570 писал(а):

С прологом есть проблемы, как понимаю, потому что механизм вывода слабоват, и влиять на него достаточно высокоуровневым образом трудно. Чем он специфически к формализации математики может лучше подходить кроме этого механизма, неясно.

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

Вообще в прологе очень просто задаются аксиомы. Так же доказательство методом сравнения результатов применения теорем с очевидными случаями выглядят не сложнее аксиом. А вот когда надо в общем случае для всех возможных значений переменной доказать истинность теоремы, тогда нужно привлекать либо много кода, либо вводить новые конструкции, как это и делается как минимум в тех системах, где используется расширенный функциональный язык.

Пролог, как и metamath, на уровне языка оперирует подстановками (при чём в расширенном виде - унификации), плюс имеет базовый механизм вывода. И по простоте доступен школьникам класса с 5-6-го (если не забивать им мозги логикой предикатов и т.д.). Поэтому мне он кажется интересным в этом плане.

[arseniiv]

alex55555 в сообщении #1376621 писал(а):

А какая может быть неоднозначность, если языковые конструкции интерпретирует компьютер?

Когда мы вводим много обозначений, может оказаться, что две разные конструкции реализуются одной и той же строкой; Metamath позволяет обозначениям выглядеть решительно как угодно (чтобы позволить бо́льшую человекочитаемость), но при этом не усложняет программу кодом для проверки однозначности чтения, так что можно по недосмотру устроить себе проблему каким-то набором определений.

Банальный пример. Пусть мы вводим формулу-конъюнкцию с обозначением $\varphi\wedge\psi$, где $\varphi,\psi$ — формулы. Тогда то, что строка $\varphi\wedge\chi\wedge\psi$ — формула, мы можем показать неединственным образом (двумя), т. е. у неё неоднозначное чтение. Чтобы такого не было, в обычных курсах матлогики и в Metamath формула-конъюнкция записывается с обязательными скобками: $(\varphi\wedge\psi)$, тогда вместо первой двусмысленной строки мы можем получить однозначные или $((\varphi\wedge\chi)\wedge\psi)$, или $(\varphi\wedge(\chi\wedge\psi))$. Чтобы скобки можно было писать пореже, нужен более сложный подход.

-- Вс фев 17, 2019 19:26:04 --

alex55555 в сообщении #1376621 писал(а):

Или модель исполнения там замороченная и её сложно понять

Там нет никакой модели исполнения, основная часть программы это просто чекер, плюс там функции для удобной работы с доказательствами (их внутренняя форма оптимизирована для проверки и неудобна для чтения).

-- Вс фев 17, 2019 19:28:00 --

alex55555 в сообщении #1376621 писал(а):

Простота модели исполнения очень нужна, она позволяет людям с меньшим опытом полноценно использовать систему.

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

[arseniiv]

alex55555 в сообщении #1376621 писал(а):

Все компьютерные языки сводимы к тьюринг-машине, поэтому в плане "слабоват" вопрос скорее философский.

Разумеется, я не на таком уровне говорил. (Кроме того это ваше утверждение в точном смысле некорректно.) Если предполагается, что у пролога есть какие-то свойства, которых нет у других языков, полезные для использования его в формальных математических корпусах, то я считаю, что это не так. Системы с большей выразительностью позволяют и более гуманную запись, и больше инструментов в конструировании вывода (так чтобы некоторые можно было получать даже полностью автоматически).

alex55555 в сообщении #1376621 писал(а):

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

Вопрос на деле стоит как бы не совсем такой.

alex55555 в сообщении #1376621 писал(а):

Вообще в прологе очень просто задаются аксиомы. Так же доказательство методом сравнения результатов применения теорем с очевидными случаями выглядят не сложнее аксиом. А вот когда надо в общем случае для всех возможных значений переменной доказать истинность теоремы, тогда нужно привлекать либо много кода, либо вводить новые конструкции, как это и делается как минимум в тех системах, где используется расширенный функциональный язык.

Вы просто не пробовали на прологе формализовать достаточно интересные вещи. Вот хватаните ZFC например. По-моему, ничего не получится.

Кроме того, как я уже написал, он не позволяет проверять доказательства (ну если только на нём не написать чекер, который и будет проверять, а не пролог), он позволяет только «выводить», и недостаточно мощно, ну потому что конечно же иначе он бы не мог это делать автоматически.

alex55555 в сообщении #1376621 писал(а):

Пролог, как и metamath, на уровне языка оперирует подстановками

К слову, те подстановки, которые упоминались выше, это не подстановки самой программы, а т. н. explicit substitution, чисто синтаксические конструкции, определённые конкретно для того корпуса, но которые можно не вводить для своего.

[alex55555]

arseniiv в сообщении #1376636 писал(а):

Там нет никакой модели исполнения, основная часть программы это просто чекер, плюс там функции для удобной работы с доказательствами (их внутренняя форма оптимизирована для проверки и неудобна для чтения).

Если есть исполнение, есть и модель. Например SQL не задаёт строго набор действий, но реляционная модель от этого никуда не девается, а выполняемый набор действий обязан ей не противоречить. Правда на практике в модель вводятся дополнения, но они обычно ещё дальше от декларативного смысла и ближе к исполнению. То есть даже если в metаmath есть только декларативный язык задания неких математических структур, то обработка этих структур всё же исходит из каких-то правил, увязанных с декларативным языком. Непосредственно проверка после подстановки может выполняться разными способами, но вот отказаться от подстановки вряд ли возможно, а это как раз модель исполнения, хоть и не детализированная до операций более низкого уровня.

arseniiv в сообщении #1376636 писал(а):

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

Да, это важно, но всё же второстепенно. Ведь разработка программы это удел достаточно квалифицированных в области её применения людей. Так какой-нибудь айфон может использовать даже ребёнок дошкольного возраста, а вот писать программы для него дошкольник вряд ли сможет. То есть когда более квалифицированные специалисты занимаются специализированной (узкой) проблемой, то с точки зрения эффективности решения проблем пользователей это сразу снимает массу вопросов, поскольку квалификация предполагается достаточной для решения подобных проблем. Другое дело, когда программу хотят менять сами пользователи. Тогда им нужно становиться программистами. Их жизнь облегчают разного рода DSL и прочие костыли, но суть не меняется - программу всё равно надо уметь писать. Ну и если есть умение, значит есть специалист с достаточной квалификацией, способный разобраться в корректности или некорректности работы программы. Плюс если бы математики сами взялись за изучение алгоритма работы программы автоматического вывода, то банально количество глаз, нацеленных на относительно скромный объём кода, очень сильно помогло бы отлову множества ошибок.

-- 17.02.2019, 22:47 --

arseniiv в сообщении #1376663 писал(а):

Кроме того это ваше утверждение в точном смысле некорректно

Не учтена многопоточность? Ввод-вывод?

arseniiv в сообщении #1376663 писал(а):

Системы с большей выразительностью позволяют и более гуманную запись, и больше инструментов в конструировании вывода (так чтобы некоторые можно было получать даже полностью автоматически).

А каким способом достигается большая выразительность?

arseniiv в сообщении #1376663 писал(а):

Вы просто не пробовали на прологе формализовать достаточно интересные вещи. Вот хватаните ZFC например. По-моему, ничего не получится.

Получится. Системы автоматического вывода написаны на ещё более низкоуровневых языках. В этом смысле получится хоть на чём. Вопрос только в соотношении затрат при том или ином подходе. Сразу писать на прологе, включая на нём же некие расширения, или писать по сути те же самые расширения на низкоуровневом языке и далее уже использовать их оторвано от исходного языка.

arseniiv в сообщении #1376663 писал(а):

Кроме того, как я уже написал, он не позволяет проверять доказательства (ну если только на нём не написать чекер, который и будет проверять, а не пролог), он позволяет только «выводить», и недостаточно мощно, ну потому что конечно же иначе он бы не мог это делать автоматически.

Да, напрямую доказательства общего вида непонятно как сделать. Видимо только через некую промежуточную сущность, вводящую дополнительную логику в модель исполнения.

[arseniiv]

alex55555 в сообщении #1376716 писал(а):

Если есть исполнение, есть и модель.

Какое, например, исполнение, если взять чекер выводов исчисления высказываний?

alex55555 в сообщении #1376716 писал(а):

То есть даже если в metаmath есть только декларативный язык задания неких математических структур, то обработка этих структур всё же исходит из каких-то правил, увязанных с декларативным языком. Непосредственно проверка после подстановки может выполняться разными способами, но вот отказаться от подстановки вряд ли возможно, а это как раз модель исполнения, хоть и не детализированная до операций более низкого уровня.

Вы понимаете «модель исполнения», вероятно, широковато. Вообще, конечно, как раз то, как выглядят выводы во внутреннем формате Metamath, можно считать программами на конкатенативном языке, но придание им семантики будет сильно зависеть от того, какие же аксиомы / правила вывода определены, потому что именно это (для Metamath — не более и не менее, никаких примитивных правил вывода там нет, мы определяем всё) задаёт, из чего такие «программы» состоят и какие из них корректны. В любом случае это слегка иррелевантно вопросу о полезности того или иного подхода.

alex55555 в сообщении #1376716 писал(а):

Да, это важно, но всё же второстепенно. Ведь разработка программы это удел достаточно квалифицированных в области её применения людей.

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

alex55555 в сообщении #1376716 писал(а):

Плюс если бы математики сами взялись за изучение алгоритма работы программы автоматического вывода, то банально количество глаз, нацеленных на относительно скромный объём кода, очень сильно помогло бы отлову множества ошибок.

Так вот же именно!

alex55555 в сообщении #1376716 писал(а):

Не учтена многопоточность? Ввод-вывод?

Не все формальные языки, имеющие хоть какое-то отношение к компьютеру, являются языками программирования; не все языки программирования тьюринг-полны и «тьюринг-реализуемы» (то есть они могут быть и слабее, и сильнее машины Тьюринга, хотя вторые будут представлять в основном академический интерес; что не помешает их друг в друга например компилировать, хоть выполнять программы на них будет и нельзя).

alex55555 в сообщении #1376716 писал(а):

А каким способом достигается большая выразительность?

Разными. Ну как вот языки программирования позволяют писать выражения по-человечески и при этом не писать лишних скобок? Грамматики, парсинг с приоритетами, такие штуки. Всё это усложняет код. А если использовать библиотеку, придётся и её код проверять.

alex55555 в сообщении #1376716 писал(а):

Системы автоматического вывода написаны на ещё более низкоуровневых языках.

Погодите, не путайте системы автоматического вывода и системы автоматической проверки, в обсуждаемом случае необходимо только второе.

Ладно, допустим вы говорите, что можно на прологе написать некий встроенный DSL и уже вместе с ним напасть на ZFC (а конкретно уметь представлять её аксиомы, выводы в ней и проверять эти выводы на корректность). Давайте. Можно взять ZF, и даже её кусок, только чур оставить хотя бы одну схему аксиом и включить аксиому бесконечности. Возьмётесь?

alex55555 в сообщении #1376716 писал(а):

Да, напрямую доказательства общего вида непонятно как сделать. Видимо только через некую промежуточную сущность, вводящую дополнительную логику в модель исполнения.

Ну вот, видимо не возьмётесь, потому что даже нет идей. Боюсь, в недостаточно динамическом прологе это вообще будет невозможно, ну или условно говоря поверх пролога будет написан целиком новый язык, что не годится.