?

Log in

No account? Create an account
sober space
 
[Most Recent Entries] [Calendar View] [Friends]

Below are the 20 most recent journal entries recorded in Осман Бинеев's LiveJournal:

[ << Previous 20 ]
Wednesday, May 19th, 2032
4:04 pm
Sticky
О себе
Не френжу никого, без обид. Если кто мне интересен - читаю через фидридер.

Мой предыдущий журнал: algebraic_brain

Locations of Site Visitors



Некоторые замечания:

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

Все около-научные тексты в этом блоге являются дилетантскими.
Wednesday, March 21st, 2018
11:59 am
Увы, после вчерашних записей я понял, что социофобия по-прежнему держит меня в ежовых рукавицах. Придется делать опять перерывчик. А жаль, много новых идей.
Tuesday, March 20th, 2018
5:58 pm
ошибся здесь: не "имеющих предел коспанов", а просто коспанов. С каким-то другим ограничением, не соображу пока, но это сейчас не важно.
4:19 pm
Не встречал ли кто-нибудь в статьях такую штуковину: категория коспанов (cospan) в Read more...Collapse )
2:26 pm
Как я уже много раз говорил, Павел ghbdtn многому меня научил в алгебре, однако в последние пару лет перед тем, как мы прекратили общаться, я чувствовал, что его замечания отвлекают меня от моей цели. Но не мог это сформулировать. Сейчас могу:

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


Так я пытаюсь поступить с теорией вероятностей и сейчас у меня возникли интересные идеи как это сделать с гладкими многообразиями. И кстати, там тоже пучки, от пучков не избавиться.
2:03 pm
Отображение, сохраняющее расстояния, называется изометрией. А если оно изменяет их пропорционально, тогда как?
Saturday, June 24th, 2017
4:12 pm
Постоянное соревнование в злом остроумии, ерничестве, жестокой иронии есть несомненный признак интеллектуальной жизни русскоязычного общества. Это соревнование, вне зависимости от политической принадлежности соревнующегося унаследованное от Маркса, Ленина и других блестящих полемистов, в наше время наносит непоправимый вред доверию, а значит и совокупному интеллекту. И, похоже, никакая степень знакомства со священным текстами тут не помеха. Борьба с чем бы то ни было такими средствами ни к чему рационально хорошему не приведет.
Friday, March 17th, 2017
11:28 am
Для чего мне нужны зависимые типы. Ну частично для того, чтобы показать что алг. верификация в моем понимании достаточно мощная вещь чтобы включить в себя всякие новомодные сейчас штучки-дрючки. Которые безусловно в чём то интересны, но я их считаю идеологически неверными и некрасивыми, во всяком случае в их нынешних сферах применения.

Но главное это комбинаторика. У меня есть гипотеза что код idA содержит комбинаторные характеристики A и что их можно алгоритмически извлекать.
Thursday, March 16th, 2017
4:10 pm
Общая идея дальнейшего движения
Я хочу продвинуться к естественному появлению зависимых типов в бестиповой лямбде. Для этого планируется сделать следующее:

Если сопоставлять обычную лямбду без типов с моноидом, то хотелось бы перейти по аналогии к "кольцу".Read more...Collapse )

Напоминаю, что всё это чистый дилетантизм и сильно доверять этому не надо.
1:14 pm
Мои аксиомы описаны в чуть-чуть видоизмененном виде в этой лекции. Но я нашел как упростить формулировку чтобы там были только три операции: σx.y (в лекции ↑), λx.P (где λ.P≡λ0.P) и PQ. А вместо ρ(P) лучше ввести сразу предпорядок.
Wednesday, March 15th, 2017
2:27 pm
Захотелось твердую копию Барендрегта. Однако цена... Но наверное закажу.
Tuesday, March 14th, 2017
6:14 pm
Готово.

clayrat посоветовал мне всё-таки Purescript, но я уже успел начать в elm'е, поскольку нашел к тому моменту онлайновую песочницу. Read more...Collapse )
2:01 am
Формулировка то работающая, но при переносе в жж наделал конечно ошибок. Вроде всё поправил, но надёжнее было бы выложить в каком-то хаскеллоподобном виде. Кстати, давно хотел попробовать что-то вроде purescript или elm...
12:52 am
Окончательная формулировка
Проверенная, работающая в программной имлементации алгебраическая формулировка бестиповой лямбды. Сложновато, но кто знает, может я и придумаю как упростить.Read more...Collapse )
Monday, March 13th, 2017
4:28 pm
Получилось.
Я как-то сразу не догадался, что формулировку можно извлечь непосредственно из правильного рекурсивного кода, реализующего обычную редукцию с индексами де Брёйна. Т.е. вопрос не в том, можно ли представить бестиповую лямбду в виде алгебраического гаджета (ответ -- можно), а в том, как найти достаточно простую аксиоматику, чтобы это имело смысл. Пока получается сложно (3 дополнительные операции), думаю как упростить.
Sunday, March 12th, 2017
1:33 pm
Итак, предыдущая попытка оказалась неудачной. Однако, как известно, Мюнхгаузен знаменит не тем, что летал или не летал, а тем что не врёт. Попробуем адаптировать индексы де Брёйна чтобы получить работающую формулировку.

Все предварительные формулировки остаются такими же, за исключением того, что вместо V мы используем группу сложения целых чисел Z (т.е. x, y, z это теперь целые числа), а также вводим бинарную операцию σ:Z×T→T с такими свойствами:Read more...Collapse )
Thursday, March 2nd, 2017
6:14 pm
Лямбда
Чтобы проверить свое представление беcтиповой лямбды как алгебраического гаджета, решил это закодить. И проверить пользуясь этой статьей как шпаргалкой. Все работает до pred, т.е. логические операции, сложение, операции с парой -- всё работает. А в вычитании какая-то ошибка. Добью на следующей неделе. Пока вкратце.Read more...Collapse )
Sunday, February 26th, 2017
3:38 pm
Здесь будет ещё много всего. Лямбда как чисто алгебраический гаджет, зависимые типы в системе без типов вообще, в мечтах и набросках комбинаторика, анализ - всё как алгебраические либо теоретико-вычислительные штуковины... Ну и будет развитие моих старых идей: благодаря статье из поста akuklev понял как формализовать алгебраическую верификацию через лямбду так, чтобы это было понятно логикам, а удобная комбинаторика мне нужна чтобы достойно продолжить линию с "пучковым" теорвером.

Я не умею понимать что-либо иначе как придумывая это заново в совершенно ином виде. А понимать люблю. Поэтому ничего математически-нового как всегда не будет, а будут опять разные взгляды на старое.
Sunday, February 12th, 2017
6:04 pm
Сон
Приснится же:

Кардинал, с важным видом:
-- Смысл истории о трех китах, держащих Землю, состоит не в том, что таково устройство Вселенной, а в том, что Господь специальным Своим решением утверждает каждое изменение волновой функции, происходящее по известному нам закону...

Мефистофель, ехидно:
-- И какой же грех нам следует совершить ради того, чтобы некоторое следующее изменение наконец-то не было Им утверждено?
Sunday, December 4th, 2016
10:06 pm
Круговые панорамы моего любимого города*. Большая часть ветхих построек снесена, но старое здание милиции стоит )) На последней панораме видна стройка порта для ПАТЭС

-------------------
*выбирать панораму можно на нижней панели, либо нажать на вертолётик, после выбора панорамы можно крутить её стрелками клавиатуры
[ << Previous 20 ]
About LiveJournal.com