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

[alex55555]

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

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

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

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

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

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

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

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

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

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

Конечно, код должен быть доступен, как минимум в виде псевдо-алгоритма, той самой модели исполнения. А лучше в полном виде, что бы была возможность выявить ошибки в реализации общего алгоритма.

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

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

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

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

То есть просто следование модели представления данных, привычной пользователям. Правильно? Но что мешает следовать такой модели на прологе? Исключаем при этом общие для всех проблемы отсутствия математических символов на клавиатуре. Да, иногда будут лишние скобки, но разве это так критично?

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

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

На основе систем проверки делают системы вывода, и наоборот.

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

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

Напасть можно на что угодно, но проблема всё равно останется прежней. Есть аксиомы и доказанные теоремы, далее следуют правила вывода, применение которых к аксиомам и теоремам позволяет строить новые теоремы. Собственно формализация аксиом и доказанных теорем на прологе тривиальна - обычное правило. А вот применение к таким правилам пролога правил вывода (не равно правилам пролога) есть то самое место, где встречается сложность. В системах автоматического вывода правила вывода встроены в систему на низком уровне, реализованы на том языке, на котором писалась система. В прологе так же придётся эти правила реализовывать, поэтому от, как вы выразились, "будет написан целиком новый язык", не уйти, но вопрос в сложности такого подхода - меньше эта сложность, чем стандартный подход с реализацией правил вывода на низкоуровневом языке или больше. Оценку сложности дать сложно (каламбурнее - лучше запоминается :) ). Точная оценка может быть после реализации, но реализация здесь нетривиальная и требует прилично времени. Ну а потом уже можно хоть ZFC, хоть всю математику "вводить".

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

В общем вы так смело возложили на меня обязанность "сделать конфетку", но я вам пытаюсь показать, что объём работы будет немаленький.

[Someone]

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

То есть проверка для конечной структуры возможна простым перебором, а для бесконечности - ну в общем очевидно.

Господь с Вами! Какие "бесконечные структуры"? Все теоремы теории множеств и их доказательства — конечные тексты, определяемые чисто синтаксически. Аксиом, правда, бесконечное множество, но они порождаются простыми синтаксическими схемами (можно написать перечисляющий алгоритм). Так что никаких "бесконечных структур" в программе рассматривать не потребуется, нужны только манипуляции с конечными строками.

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

[пианист]

Вот, товарищ примерно таким чем-то занят:
https://arxiv.org/search/math?searchtyp ... les%2C+T+C

[arseniiv]

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

Нельзя брать только часть (чекер).

Почему нельзя?

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

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

Тогда у вас для разных вещей «модель» значит существенно разное. И вы так и не показали, что введение этого понятия вообще для чего-то полезно.

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

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

Я начинаю терять нить; в каком смысле мы задаём? В MM, в произвольной системе формализации математики, в идеале?

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

Конечно, код должен быть доступен, как минимум в виде псевдо-алгоритма, той самой модели исполнения. А лучше в полном виде, что бы была возможность выявить ошибки в реализации общего алгоритма.

Именно что никаких «псевдо-алгоритмов» (что это такое вообще? есть псевдокод, есть алгоритм), выполняется-то конкретный код, а не идеи, которыми руководствовались при его описании. А как документировать систему пользователю, который не заинтересован смотреть код, вещь вообще отдельная.

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

То есть просто следование модели представления данных, привычной пользователям. Правильно?

Это слишком общие слова.

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

Но что мешает следовать такой модели на прологе? Исключаем при этом общие для всех проблемы отсутствия математических символов на клавиатуре. Да, иногда будут лишние скобки, но разве это так критично?

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

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

На основе систем проверки делают системы вывода, и наоборот.

Это тоже общие слова, притом для текущего обсуждения непозволительно общие. Если вы всю дорогу собирались оставаться на уровне «кто-то когда-то непонятно зачем гипотетически может сделать», то так бы и сказали, но я ждал чего-то посущественнее.

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

Оценку сложности дать сложно

Ну и толку-то от болтовни всей. А я тут в конкретное устройство MM зачем-то полез — и, спрашивается, для кого? (Это риторический вопрос.)

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

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

То есть вы даже не в курсе, что такое аксиома бесконечности в ZF, шикарно.

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

В общем вы так смело возложили на меня обязанность "сделать конфетку", но я вам пытаюсь показать, что объём работы будет немаленький.

А я вам пытался показать, что вы надели смотря на пролог розовые очки.

Ладно, может на этот диван присядет поболтать ни о чём кто-то другой, а я ухожу.

[alex55555]

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

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

То есть проверка для конечной структуры возможна простым перебором, а для бесконечности - ну в общем очевидно.

Господь с Вами! Какие "бесконечные структуры"?

Ну вот простой пример:

append([e|es1],es2,[e|es3]):-append(es1,es2,es3).
append([],es,es).

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

Я это не с целью что-то там оспорить говорю, но мне самому интересно - как будет лучше, правильнее, эффективнее, потому что бесконечность и компьютер я не совмещал.

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

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

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

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

[Someone]

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

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

Я согласен с arseniiv: Вы не понимаете, о чём пишете. В математике нет доказательств, которые ссылаются сами на себя прямо или косвенно. Такая ситуация называется "порочным кругом" и запрещена.

Ещё раз повторяю: в ZFC (да и вообще в математике, за исключением, может быть, каких-то "бесконечных логик", о которых я краем уха что-то слышал, но никогда с ними не встречался; чего только люди не придумают…) все теоремы и все доказательства являются конечными текстами. "Доказательство", которое никогда не заканчивается — не доказательство.

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