2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему На страницу 1, 2, 3, 4, 5 ... 7  След.
 
 Формализация математических текстов
Сообщение01.08.2020, 09:15 


01/08/20
67
Формализация математических текстов

Известно, что математический текст представляет собой формулу. Здесь рассматриваются средства, позволяющие записать такую формулу.

1. Логическая структура

К стандартным логическим символам добавляются $\rfloor$ (пусть) и $\vdash$ (тогда).


Запись ($\mathrm{Th}. 2 \mid  x\mapsto a$) означает ссылку на формулировку теоремы 2, в которой параметр $x$ заменяется параметром $a$.

Часть доказательства, заключённая в скобки $(_{asd} \,\,\,    _{asd}) $, проводится методом "от противного".


2. Буквы и аббревиатуры

Предположим, что в тексте часто упоминаются математические объекты одного типа (например, кольца). В этом случае зарезервируем для обозначения таких объектов букву (например, $R$). На протяжении всего текста эта буква будет обозначать объект данного типа. При необходимости ввести несколько объектов данного типа можно воспользоваться той же буквой с индексами. Запись $r \in R$ автоматически будет расшифровываться как "$r$ - элемент кольца", а запись $R_1 \sqsubset  R_2$ - как "$R_1$ - подкольцо кольца $R_2$".

Для того чтобы обозначить класс объектов, применяются аббревиатуры. Класс колец можно обозначить $RNG$, класс групп - $GRP$, класс коммутативных объектов - $COM$.
Тогда класс абелевых (коммутативных) групп можно обозначить $COM.GRP$, а запись $g \in G  \in COM.GRP$ будет расшифровываться как "$g$ является элементом абелевой группы $G$".
Если класс объектов образует категорию, то аббревиатуру класса следует подчеркнуть. Например, $\underline{COM.RNG}$ - категория коммутативных колец.
Зарезервировав для понятия "простой", аббревиатуру $PRM$, получим обозначения для множества простых чисел - $PRM.\mathbb{Z}$ и для множества простых идеалов данного кольца - $PRM.IDL(R)$. Если буква $I$ обозначает идеал, то запись $I \in PRM$ означает, что $I$ - простой идеал.

Запись $f : A {\rightarrow}_{hme} B$ означает, что $f$ - гомеоморфизм ($hme$).

Списки букв и аббревиатур размещаются в указателе обозначений.

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

Изложение с дополнениями в виде pdf-файла в хранилище Google Диск.
https://drive.google.com/file/d/1wp3-Fb ... 6ur8-/view

Исправленная версия заметки (добавлена ссылка на монографию С.И. Адяна, где используются схожие обозначения):
https://drive.google.com/file/d/1TuzXeX ... pFpzY/view

Практическая реализация предлагаемого способа в виде конспектов конкретных математических текстов в виде pdf-файлов доступна по следующим ссылкам:

Конспект книги В.Г. Каца и П. Чена "Квантовый анализ".
https://drive.google.com/file/d/13qJvqZ ... PDV0C/view

Конспект §§1-11 главы 1 книги Ю.И. Манина "Введение в теорию схем и квантовые группы".
https://drive.google.com/file/d/1eD98R2 ... mQRvN/view

 Профиль  
                  
 
 Posted automatically
Сообщение01.08.2020, 10:19 


20/03/14
12041
 i  Тема перемещена из форума «Дискуссионные темы (М)» в форум «Карантин»
по следующим причинам:

- просьба предельно четко сформулировать предмет темы,
- касательно внешних ссылок см п. 5 правил форума topic3476.html
- (краткие инструкции по набору формул: «Краткий FAQ по тегу [math]» и видеоролик Как записывать формулы);


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

 Профиль  
                  
 
 Posted automatically
Сообщение01.08.2020, 12:11 


20/03/14
12041
 i  Тема перемещена из форума «Карантин» в форум «Дискуссионные темы (М)»
Причина переноса: пока сюда.

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение20.08.2020, 12:58 
Заслуженный участник
Аватара пользователя


21/12/05
5903
Новосибирск
Alexandr Gavrichenko в сообщении #1476790 писал(а):
Практическая реализация предлагаемого способа в виде конспектов конкретных математических текстов в виде pdf-файлов доступна по следующим ссылкам:

Для шпаргалок годится - проверено на себе.

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение20.08.2020, 15:13 


10/04/12
704
А чем это лучше чем Coq?

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение23.08.2020, 09:44 


01/08/20
67
bot в сообщении #1479968 писал(а):
Для шпаргалок годится - проверено на себе.

Объём текста уменьшается ориентировочно на 30%.

mustitz в сообщении #1479986 писал(а):
А чем это лучше чем Coq?

Здесь предлагается однотипный способ записи разнообразных терминов на основе обозначения математического понятия, такого же как обращение к элементу записи в языках программирования (например, Паскаль).
Судя по статье в Википедии https://ru.wikipedia.org/wiki/Coq (с Coq я не знаком) элементы этого способа есть в Coq, поскольку Peano.plus и Peano.mult означают пеановские сложение и умножение.
Я рассмотрел возможность сделать такую запись повсеместно применяемой в обычном тексте (книге, статье), а не только в языке программирования. Тогда открывается возможность сделать математический текст машинно распознаваемым.
В моей работе собственно автоматическое доказательство теорем не рассматривается.

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

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение24.08.2020, 22:44 
Заслуженный участник
Аватара пользователя


28/04/14
968
спб
Alexandr Gavrichenko в сообщении #1476790 писал(а):
Известно, что математический текст представляет собой формулу

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

Для людей это не подходит. Для компьютеров - есть более основательные подходы.

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение25.08.2020, 09:27 


01/08/20
67
demolishka в сообщении #1480609 писал(а):
Тут тоже новые закорючки придумывать будем?

Почему бы и нет. В настоящем же виде
Alexandr Gavrichenko в сообщении #1480349 писал(а):
список обозначений, исторические и идейные замечания
записываются на естественном языке. Формализации подлежат формулировки определений и теорем и доказательства.
Вводя аббревиатуру для неизвестного понятия $XYZ$, можно формализованно записывать и некоторые наводящие соображения в виде вопросов.

Запись $$SPC(R) \in IRD.TOP.SPACE \Leftrightarrow NPT(R) \in XYZ$$ эквивалентна вопросу: как охарактеризовать нильрадикал кольца с неприводимым спектром?

Ответ: $$XYZ = PRM.IDL(R)$$ (нильрадикал прост).

demolishka в сообщении #1480609 писал(а):
Для людей это не подходит.

Это с непривычки.
Никто же не пишет сейчас "неизвестная величина, умноженная на себя", а пишут формулу $x^2$.
И все понимают это потому, что в школе проходили запись формул.
А в младших классах эти закорючки выглядели "для людей не подходящими".

Здесь же предлагается заменить фразу "каждый простой идеал содержится в максимальном идеале" формулой
$$\forall I \in PRM \quad \exists I' \in MAX \quad (I \subset I' \subset R)$$
Таких формул в школе никто не изучал, поэтому они непонятны.
Допускаю, что такая запись не всем придётся по вкусу, но её плюс в том, что уменьшается число разночтений.

demolishka в сообщении #1480609 писал(а):
Для компьютеров - есть более основательные подходы.

Как раз формула воспринимается и человеком, и компьютером.

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение25.08.2020, 16:31 
Заслуженный участник
Аватара пользователя


28/04/14
968
спб
Alexandr Gavrichenko в сообщении #1480631 писал(а):
Это с непривычки.

Дело не в привычке, а в неэффективности. Вы просто сокращаете английские слова и требуете некоторой однозначной записи высказываний.
Alexandr Gavrichenko в сообщении #1480631 писал(а):
её плюс в том, что уменьшается число разночтений.

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

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение25.08.2020, 17:07 


01/08/20
67
demolishka в сообщении #1480680 писал(а):
плюс только для "левополушарных математиков"

Да. Формула может иметь несколько разных интерпретаций, и "понимание" - это выбор одной из этих интерпретаций.
Когда решают уравнения, то производят алгебраические преобразования, не придавая им специального смысла.
Почему бы целевой аудитории моей работы и не быть "левополушарными математиками"?
У кого-то понимание основано на изображении. Им данная формализация будет неудобна.

demolishka в сообщении #1480680 писал(а):
распознавать формулы подобно компьютеру

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

demolishka в сообщении #1480680 писал(а):
неэффективности

Ещё раз: запись "неизвестная величина, умноженная на себя" неэффективна в том смысле, что никто ей не пользуется. Так что есть уровень, на котором формализация общепринята.

demolishka в сообщении #1480680 писал(а):
Вы просто сокращаете английские слова

Эти сокращения позволяют встраивать математические понятия в формулы.
Так, кстати, обозначают категории. Я рассмотрел дальнейшее развитие. Чтобы присвоить какому-то понятию аббревиатуру, оно не обязано представлять собой категорию. Далее рассматриваются структурированные наборы сокращений.
Кроме того, обозначение центрального понятия одной буквой применяется в энциклопедических статьях.
Здесь эти способы формализации приложены к математическому тексту.

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение25.08.2020, 18:02 
Заслуженный участник
Аватара пользователя


28/04/14
968
спб
Alexandr Gavrichenko в сообщении #1480687 писал(а):
Так что есть уровень, на котором формализация общепринята.

Уровень есть, только Вы его доводите до абсурда.

Alexandr Gavrichenko в сообщении #1480687 писал(а):
правополушарнику

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

Из Вашей посылки, что
Alexandr Gavrichenko в сообщении #1476790 писал(а):
математический текст представляет собой формулу

путь только в компьютерную проверку доказательств теорем. Либо это так и останется как Ваше личное развлечение.

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение25.08.2020, 18:15 


01/08/20
67
demolishka в сообщении #1480694 писал(а):
Вы его доводите до абсурда.

Большая часть рассуждений в тексте формальна. Не вижу абсурда в том, чтобы привести эти рассуждения к формуле.
demolishka в сообщении #1480694 писал(а):
путь только в компьютерную проверку доказательств теорем.

Скорей обучение компьютера математике.

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение25.08.2020, 18:38 


10/04/12
704
Alexandr Gavrichenko в сообщении #1480700 писал(а):
Большая часть рассуждений в тексте формальна. Не вижу абсурда в том, чтобы привести эти рассуждения к формуле.


Если нужна формальность, то я уже упоминал Coq. Нет никакой проблемы записать условие теоремы с использованием этого языка, там же провести формальное доказательство с проверкой. И приложить файл. Другой вопрос в том, насколько часто нам нужна именно формальность? И сколько разных непониманий возникает в случае неформального текста, который могла бы устранить формализация? Мне это не представляется большой проблемой. А значит нет мотивации переходить на предложенную нотацию, что очень ресурсоёмко: сколько в мире работающих математиков? Сколько им необходимо будет времени для того, чтобы ознакомиться с нотацией, наступить на все грабли, привыкнуть к ней? И в результате получить то же представление в мозгу, что и раньше. Аналогично можно предложить писать все научные работы на эсперанто.

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение26.08.2020, 06:47 


26/12/18
155
Формализация вроде Coq-а реално нужна для проверки доказательств только в очень редких и исключительных случаях, когда эти доказательства оказываются слишком громоздкими, хаотическими и с трудом обозримыми для экспертов: задача 4-ых красок, решение Т.Хейлсом гипотезы Кеплера и подобные плохо структурированные проблемы с большущим пространством перебора. Полная формализация чревата большими накладными расходами и серьёзными ошибками при интуитивной/содержательной интерпретации чужих мышлению формальных текстов. На мой взгляд, для подавляющего большинства работающих математиков и проблем такая формализация не стоит свеч и ненужно затормозила бы продуктивность.

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение26.08.2020, 08:49 


01/08/20
67
mustitz в сообщении #1480701 писал(а):
Сколько им необходимо будет времени для того, чтобы ознакомиться с нотацией, наступить на все грабли, привыкнуть к ней?

Этот вопрос так же уместен по отношению к Coq, как и к предложенной "нотации".
Можно ли научить компьютер (тот же Coq) воспринимать уже написанный текст?
То есть, Coq "читает" статью или книгу и автоматически добавляет содержащиеся в тексте теоремы в свой список лемм. Здесь формализация текста может оказаться полезной.

mustitz в сообщении #1480701 писал(а):
И в результате получить то же представление в мозгу, что и раньше.

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

Sycamore в сообщении #1480757 писал(а):
серьёзными ошибками при интуитивной/содержательной интерпретации чужих мышлению формальных текстов.

Остаётся возможность, что эта интерпретация будет не ошибочной, а альтернативной.


О передаче идей в формализованном тексте


Идеи передаются обычным (естественным) языком и никак не формализуются.

Конспект книги В. Г. Каца и П. Чена "Квантовый анализ", §7, Th.4
https://drive.google.com/file/d/13qJvqZ ... PDV0C/view
Доказательство содержит обращение к интуитивному представлению о выборе шаров и записывается естественным языком.

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 101 ]  На страницу 1, 2, 3, 4, 5 ... 7  След.

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group