Кто по-английски читает (математические книжки, это проще), лучший текст Pertti Lounesto "Clifford algebras and spinors" (есть на libgen.rs, но нужен VPN)
Я довольно много пробовал всего и моё мнение - пока хорошего пруфчекера нет. И перспективней всех Metamath, если бы там удалось решить проблемы с подстановкой (в Metamath есть только простая подстановка, не заботящаяся о переименовании связанных переменных в случае коллизий, поэтому формализовать логику с кванторами или лямбда-исчисление приходится крайне нестандартными способами). Проблемы эти математические, не программистские.
Написал сложное доказательство, в котором естественно возникают зависимые типы (некоторый тип данных естественным образом делится на "слои", индексированные натуральными числами). Итого, есть типы B и A n, где n:nat. Хочу доказать, что B есть сумма всех A n. Строю функции
foo (n:nat) (a: A n) : B
rang (b:B) : nat
bar (b:B) : A (rang b)
Доказываю
forall (b:B), foo (rang b) (bar b) = b
forall (n:nat) (a: A n), rang (foo n a) = n
Но когда выписываю теорему
forall (n:nat) (a: A n), bar (foo n a) = a
получаю
"The term bar (foo n a) has type A (rang (foo n a)) while it is expected to have type A n".
Спрашиваю на форуме, отвечают -- надо присобачить тип равенства. Прикидываю, как его присобачить, понимаю, что доказательство (и без того сложное) станет сложнее в два раза, бросаю Coq нафиг. Хотя, сделан Coq хорошо, это я такой хитроумный.
В первой половине 80-х учил Фортран, Алгол и Пи-эль 1. Однако, диплом писал уже на функциональном языке ГАРФ, придуманном в ВИНИТИ Ильёй Ханаановичем Шмаиным. Вот какой-то документ по ГАРФ (в формате doc), но не уверен, можно ли по нему что-то понять.
Учил в своё время Lua, очень добрый и приятный язык, сделано в Бразилии. Но когда попробовал на нём рисовать, там есть только OpenGL2, а OpenGL3 уже нет. Потому что в OpenGL3 есть команды с двойными указателями ** и даже LuaJIT не может их понять (с одной звёздочкой может, в Lua вообще нет указателей, но LuaJIT позволяет вставлять в Lua кусочки кода на C). А так, гораздо приятнее, чем Питон и Яваскрипт. Lua, кстати, придумана (она женского рода, Lua значит "Луна") на год раньше Яваскрипта. В былые времена несколько раз слышал от разработчиков на Яваскрипт "как хорошо было бы, если бы сразу выбрали Lua вместо Яваскрипт!" Яваскрипт был сделан на коленке за два дня (как рассказывал его разработчик), что поначалу очень чувствовалось (сейчас его, кажется, доработали)
Кусочек кода на языке Factor. Определяет функцию <value>, которая при каждом запуске выдаёт новое натуральное число. В скобках что-то вроде типа (из ничего получается одно значение, в Factor функция может выдавать несколько значений, которые кладутся в стек, оттуда же берутся аргументы).
Вот интересно, все остальные книжки Бурбаков вполне нормальные. Полезли не в своё дело (среди них не было специалистов по матлогике и основаниям математики)
Шеннон был жонглёр-любитель. Жонглёр он был плохой (дошёл до четырёх предметов), но силён в теории. Придумал способ записи жонглёрских трюков, которым с тех пор пользуются все жонглёры
Идея там простая (но жонглёры обычно не понимают, учат наизусть). Запись 531 означает, что первый брошенный мяч пробудет в полёте 5 тактов, второй 3 такта, третий один такт. Руки обычно бросают попеременно (левая-правая, левая-правая). Если три шарика назвать A,B,C, последовательность бросков выглядит так
ABCCBAABCCBA
Первым броском левая рука выбрасывает мячик A высоко, он вернётся через пять тактов (в правую руку). Вторым броском правая рука выбрасывает мячик B не так высоко, он вернётся через три такта. Третьим броском левая рука низко перекидывает мячик C в правую, это занимает один такт. Четвёртым броском правая рука выбрасывает мячик C на пять тактов и дальше 531531531. Если число нечётное, мячик вернётся в другую руку, если чётное - в ту же самую. Для одновременных бросков двумя руками есть специальная запись.
Читаю и думаю "Смогу ли я так делать?" С одной стороны, я способен к сложной математике. С другой, птичьи языки не запоминаю. Впечатление, что для хакера важней не ум, а хорошая память и усердие.
Альтернатива какого рода? ЖЖ хорош, чтобы поговорить. Кое-где там оживлённые места (например, в блоге ivanov-petrov). Если хотите поговорить, лучше ЖЖ ничего нет. Если же выкладывать фото и получать лайки, тогда другое дело.
Пизельда!
По ссылке "Илья Слуцкер" какой-то Илья Суцкевер.
Кто по-английски читает (математические книжки, это проще), лучший текст Pertti Lounesto "Clifford algebras and spinors" (есть на libgen.rs, но нужен VPN)
Я довольно много пробовал всего и моё мнение - пока хорошего пруфчекера нет. И перспективней всех Metamath, если бы там удалось решить проблемы с подстановкой (в Metamath есть только простая подстановка, не заботящаяся о переименовании связанных переменных в случае коллизий, поэтому формализовать логику с кванторами или лямбда-исчисление приходится крайне нестандартными способами). Проблемы эти математические, не программистские.
Спасибо, я туда ходил.
Что самое прекрасное - Бабаи 1950 года рождения. В возрасте 65 лет он это открыл!
А вот знает ли кто-нибудь , этот способ записи алгоритмов (после слов "Шифрование:" и "Расшифровка:") - это что такое? Чем это набирают?
Написал сложное доказательство, в котором естественно возникают зависимые типы (некоторый тип данных естественным образом делится на "слои", индексированные натуральными числами). Итого, есть типы B и A n, где n:nat. Хочу доказать, что B есть сумма всех A n. Строю функции
foo (n:nat) (a: A n) : Brang (b:B) : natbar (b:B) : A (rang b)Доказываю
forall (b:B), foo (rang b) (bar b) = bforall (n:nat) (a: A n), rang (foo n a) = nНо когда выписываю теорему
forall (n:nat) (a: A n), bar (foo n a) = aполучаю
"The term
bar (foo n a)has typeA (rang (foo n a))while it is expected to have typeA n".Спрашиваю на форуме, отвечают -- надо присобачить тип равенства. Прикидываю, как его присобачить, понимаю, что доказательство (и без того сложное) станет сложнее в два раза, бросаю Coq нафиг. Хотя, сделан Coq хорошо, это я такой хитроумный.
Кто хочет программировать машину Тьюринга, вот здесь есть она
https://www2.cs.duke.edu/csed/jflap/
Неправда, Чёрч был научруком Клини.
В первой половине 80-х учил Фортран, Алгол и Пи-эль 1. Однако, диплом писал уже на функциональном языке ГАРФ, придуманном в ВИНИТИ Ильёй Ханаановичем Шмаиным. Вот какой-то документ по ГАРФ (в формате doc), но не уверен, можно ли по нему что-то понять.
https://www.mediafire.com/file/h303jm3czojl17x/GARF-1_ed%2526comm_VB_Jan06.DOC/file
Учил в своё время Lua, очень добрый и приятный язык, сделано в Бразилии. Но когда попробовал на нём рисовать, там есть только OpenGL2, а OpenGL3 уже нет. Потому что в OpenGL3 есть команды с двойными указателями ** и даже LuaJIT не может их понять (с одной звёздочкой может, в Lua вообще нет указателей, но LuaJIT позволяет вставлять в Lua кусочки кода на C). А так, гораздо приятнее, чем Питон и Яваскрипт. Lua, кстати, придумана (она женского рода, Lua значит "Луна") на год раньше Яваскрипта. В былые времена несколько раз слышал от разработчиков на Яваскрипт "как хорошо было бы, если бы сразу выбрали Lua вместо Яваскрипт!" Яваскрипт был сделан на коленке за два дня (как рассказывал его разработчик), что поначалу очень чувствовалось (сейчас его, кажется, доработали)
Пестов, кажется, обиделся (никто не оценил), на письма с вопросами не отвечает. А мне нравится!
: <value> ( -- value ) \ <value> counter ;
Кусочек кода на языке Factor. Определяет функцию <value>, которая при каждом запуске выдаёт новое натуральное число. В скобках что-то вроде типа (из ничего получается одно значение, в Factor функция может выдавать несколько значений, которые кладутся в стек, оттуда же берутся аргументы).
Вот интересно, все остальные книжки Бурбаков вполне нормальные. Полезли не в своё дело (среди них не было специалистов по матлогике и основаниям математики)
Шеннон был жонглёр-любитель. Жонглёр он был плохой (дошёл до четырёх предметов), но силён в теории. Придумал способ записи жонглёрских трюков, которым с тех пор пользуются все жонглёры
https://ogo-spb.ru/index.php/siteswaps
Идея там простая (но жонглёры обычно не понимают, учат наизусть). Запись 531 означает, что первый брошенный мяч пробудет в полёте 5 тактов, второй 3 такта, третий один такт. Руки обычно бросают попеременно (левая-правая, левая-правая). Если три шарика назвать A,B,C, последовательность бросков выглядит так
ABCCBAABCCBA
Первым броском левая рука выбрасывает мячик A высоко, он вернётся через пять тактов (в правую руку). Вторым броском правая рука выбрасывает мячик B не так высоко, он вернётся через три такта. Третьим броском левая рука низко перекидывает мячик C в правую, это занимает один такт. Четвёртым броском правая рука выбрасывает мячик C на пять тактов и дальше 531531531. Если число нечётное, мячик вернётся в другую руку, если чётное - в ту же самую. Для одновременных бросков двумя руками есть специальная запись.
Читаю и думаю "Смогу ли я так делать?" С одной стороны, я способен к сложной математике. С другой, птичьи языки не запоминаю. Впечатление, что для хакера важней не ум, а хорошая память и усердие.
Ну, всё сразу не могу, но знакомые математики сейчас собираются на сайте
https://mathstodon.xyz/about
Альтернатива какого рода? ЖЖ хорош, чтобы поговорить. Кое-где там оживлённые места (например, в блоге ivanov-petrov). Если хотите поговорить, лучше ЖЖ ничего нет. Если же выкладывать фото и получать лайки, тогда другое дело.
А что стало с Гавриловым?