Handmath, аматорська математика - своїми руками, сторінка 4
Що таке алгебра?
Нехай - дійсне векторний простір. тобто виконані наступні аксіоми (, - дійсні числа):
Елементи вже можна складати. Тепер нехай на можна задати множення так, щоб були виконані наступні аксіоми:
Ми не вимагає від множення, взагалі кажучи, ні асоціативності, ні тим більше коммутативности або будь-яких інших властивостей. Власне, все: при виконанні наведених вище умов, - алгебра.
композиційна алгебра
Нехай до того ж - евклідів, тобто на ньому задано деякий скалярний твір, причому
Це скалярний твір породжує норму. Алгебра є композиційною. якщо.
Одиниця - вона і в Африці одиниця, тільки ми, щоб уникнути путініци, будемо обозначаеть її, тому що ми будемо вибирати цей елемент в якості першого базисного вектора. Від одиниці потрібно тільки, щоб. Оскільки алгебра є композиційною, ми отримуємо, що
тобто одиниця свідомо унормована. Це не єдине цікаве властивість дійсних композиційних алгебр з одиницею.
подільники нуля
У дійсних композиційних алгебрах їх немає! І правда,
сполучення
Сполучення можна задати наступною формулою
тобто поєднання дійсно інволютивно. Більш того
Порядковий розбір нашого hello world
Отже, ми успішно встановили Міцар і перевірили нашу першу статтю. Але, власне, а що в нашій статті написано?
Власне текст статті повинен начитатися зі слова begin. Якщо ми приберемо його, то отримаємо помилку «213:« begin »missing». Кількість слів begin в статті може бути будь-яким - його можна поставити хоч після кожного рядка або кілька разів поспіль: на коректність це ніяк не вплине.
Тепер, завдяки підсвічуванню ми можемо помітити, що слова в статті можна розділити на деякі групи: ті, які підсвічені так само, як environ і begin (це рівно ще одне слово reserve) і слова for, or, not, implies. Останні слова - це логічні зв'язки «або», «не» і символ імплікації, логічного слідства (). Тут потрібно сказати, що все, що стосується обчислення предикатів, Міцар розуміє без яких би то не було додаткових пояснень.
Останні три рядки показують весь арсенал базових відносин =, <> і in (тобто) і їх властивостей: а саме, що <> є антонім для = (перший рядок) і що ставлення in асиметрично (друга і третя рядки). Ніяких інших базових відносин в МІЦАР немає.
Спробуємо трохи змінити статтю
Додамо тавтології, які формулюють основні властивості рівності (рефлексивність, симетричність і транзитивність):
hello = hello;
hello = world iff world = hello;
hello = world world = Mizar implies hello = Mizar;
Після запуску перевірки отримаємо помилку «143: No implicit qualification» поруч зі словом Mizar. Дійсно, ця змінна не була описана. Якщо її додати в секцію reserve, то все стане добре. iff - це прийняте в англомовній літературі скорочення виразу «тоді і тільки тоді, коли», а - звичайний знак для логічного «і». Додамо тепер ще три рядки і подивимося, що буде
hello = world Mizar in hello implies Mizar in world;
hello = world implies (Mizar in hello iff Mizar in world);
(Mizar in hello iff Mizar in world) implies hello = world;
Перші дві проходять перевірку, а на третій виникає помилка. Це здається дивним, тому що другий рядок стверджує, що якщо два безлічі рівні, то будь-який елемент належить одному з них тоді і тільки тоді, коли він належить і іншому. Звернення цього твердження вже не є за замовчуванням очевидним для Мицара, тому що вимагає того, щоб відносини in і = були якось пов'язані один з одним. За замовчуванням ж in - це просто асиметричне відношення, яке, можливо, з рівністю ніяк і не пов'язано. Про те, як потрібно формувати секцію environ, щоб зв'язати їх, слід написати окремий пост.
Що робити далі?
Корисні посилання
Ще у Мицара є вікі. на якому особливо корисна класифікація статей за розділами математики, розпочата Марко Ріккарді (монтіньозо, Італія).
Formalized Mathematics
Що таке Міцар
Міцар - це ще і формальний мову, на якому можна записувати докази, зручні для автоматичної перевірки, але також доступні для прочитання людиною. Опис цієї мови заслуговує окремого поста.
І нарешті, Міцар - це те, чим я останнім часом цікавлюся і чому присвячую цю замітку, підсумком якої має стати Hello World на МІЦАР.
Як встановити Міцар
За не зовсім зрозумілих причин, Міцар не є Open Source проектом (координатори проекту базуються переважно в Польщі і бояться, що Міцар «вкрадуть»; можливо, наші брати-слов'яни знають, чого побоюватися), проте дистрибутиви доступні для вільного скачування і використання в будь-яких некомерційних цілях.
1. Завантажити Emacs (Міцар працює і без нього. З ним він просто робиться зовнішній вигляд і зручні.)
2. Розпакувати вміст завантаженого в корінь на C: \
4. Погодитися з програмою установки і дозволити їй звалити Міцар в C: \ mizar
5. Додати змінну середовища MIZFILES = C: \ mizar
6. Скопіювати файл mizar.emacs з папки C: \ mizar в корінь C: \
Під Linux або MacOS потрібно вибрати відповідний дистрибутив Міцар. а Emacs в Linux вже буває встановлений, і не мені розповідати линуксоидов, як його налаштовувати.
Mizar Mode for Emacs
Спеціальний режим для роботи з файлами Мицара був розроблений Джозефом Урбаном з Неймегена (Нідерланди) і зараз входить в стандартний дистрибутив системи. Насправді він є практично єдиною працюючою «IDE» для користувачів Міцар. Якщо Ви не знаєте, як працювати з Emacs, то спробуйте пройти стандартний вступний курс - він зручний, швидкий і зрозумілий, Emacs сам його Вам запропонує. Якщо не хочете - користуйтеся стрілками на клавіатурі, мишкою для виділення і пунктами меню для копіювання / вставки (так як ніяких Crtl + C / Ctrl + V в Emacs для цих цілей немає - там трохи інша логіка).
Hello, World!
Перед запуском Emacs підготуйте де-небудь поруч дві директорії: text і dict, в яких будуть розташовуватися файли нашого hello world. Отже, запускаємо щось на зразок C: \ emacs-23.2 \ bin \ runemacs.exe і створюємо новий файл hello.miz в директорії text (директорія dict нам знадобиться тільки для порядку - в неї нічого зберігати не потрібно). Потім скопіюйте наступний текст в Emacs, переконайтеся, що текст круто підсвітити, потім виберіть пункт меню Mizar-> Indenting-> Indent bufer, переконати, що текст якось вирівнявся, після чого натисніть Ctrl-C Enter (або через меню Mizar-> Run Mizar).
environ
begin
reserve hello, world for set;
hello = world or hello <> world;
not hello in hello;
hello in world implies not world in hello;
Вступ до магістратури увінчалося успіхом. Це завдання було першою на іспиті і, мабуть, найлегшою. У ній все просто до очевидності. Четверная група Клейна - це нециклічного група з чотирьох елементів, ізоморфна. Нетривіальні рівності її таблиці множення:
Легко бачити, що будь-яка перестановка елементів не змінює цієї таблиці множення в цілому - група переходить в себе (тобто здійснює деякий гомоморфізм, до того ж все перестановки оборотні, тому це гомоморфізм, який є біекція, тобто ізоморфізм, та до того ж це ще ізоморфізм групи в себе, тобто автоморфизм). При автоморфізм нейтральний елемент завжди повинен переходити в себе, тому ніяких інших автоморфізмів бути не може. (Симетрична група перестановок трьох елементів) і є шукана група автоморфізмів.