?

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. Если Вы математик и нашли ошибку у меня, скажите прямо - я исправлю и буду благодарен.

Все около-научные тексты в этом блоге являются дилетантскими.
Saturday, June 24th, 2017
4:12 pm
Постоянное соревнование в злом остроумии, ерничестве, жестокой иронии есть несомненный признак интеллектуальной жизни русскоязычного общества. Это соревнование, вне зависимости от политической принадлежности соревнующегося унаследованное от Маркса, Ленина и других блестящих полемистов, в наше время наносит непоправимый вред доверию, а значит и совокупному интеллекту. И, похоже, никакая степень знакомства со священным текстами тут не помеха. Борьба с чем бы то ни было такими средствами ни к чему рационально хорошему не приведет.
Thursday, April 6th, 2017
6:51 pm
Все же не успеваю заняться вплотную требующимися доказательствами, поэтому расскажу всё как гипотезы. Итак, в дальнейшем под лямбда-исчислением подразумевается такая алгебраическая структура, дополненная такими расширениями. Все это может измениться, улучшиться, упроститься, но для изложения моих гипотез этого достаточно.

Раньше алгебраическая верификация в моем понимании состояла из двух частей:

1. Язык программирования с (каким-то правильно устроенным) information hiding пригоден для верификации алгебраических (не)равенств. Это иллюстрировалось конкурсом, в котором так никто и не поучаствовал.
2. Программы на разных языках программирования можно верифицировать через (не)равенства. Это иллюстрировалось примером доказательства.

Теперь туда добавляется третий пункт:
3. Вся Curry-Howard тематика естественным и удобным образом выразима в идеологии алгебраической верификации. Это еще иллюстрировать и иллюстрировать.
Далее: как эти пункты переосмысляются через лямбду.
Read more...Collapse )
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
Круговые панорамы моего любимого города*. Большая часть ветхих построек снесена, но старое здание милиции стоит )) На последней панораме видна стройка порта для ПАТЭС

-------------------
*выбирать панораму можно на нижней панели, либо нажать на вертолётик, после выбора панорамы можно крутить её стрелками клавиатуры
Sunday, November 27th, 2016
9:46 pm
Гугловский ИИ для перевода действительно кое-что улучшил. Но:
Скоро тринадцать лет, как соловей из клетки лопаются и улетела. А с наступлением темноты, Богдыхан таблетки пьет немного крови заблудших портной, откидывается на подушки и включают в обмотку, усыплять, убаюканный уровнем песни.
Saturday, September 17th, 2016
2:00 pm
Певекский апокалипсис
Когда я был в последний раз в Певеке, в феврале 1990, я вышел на Обручева и долго смотрел на дома. Видимо, предчувствие было.


Pevek_apokalipse от Вадим Максимов на Rutube.

Sunday, September 11th, 2016
11:52 pm
Логическая теория метафоры?
отсюда:

Чтобы расширить наше понимание рациональности, нужно чтобы некоторые составляющие процесса мышления попали в поле публичных обсуждений.

Я говорю конкретно о метафорах. Мне кажется, что в метафорическом мышлении скрывается огромная "вычислительная" мощь, которая пока скрыта от публичного обсуждения, во всяком случае в научной жизни. Не то, чтобы ее специально скрывали -- обсуждают (см. напр. "Математика как метафора", Ю. Манин). Но просто не найдено достаточного выразительного языка для обсуждения. Если логическая теория метафоры будет построена, это будет определенно развитием рациональности, по сравнению с теорией. Сейчас я пытаюсь сказать, что теория менее богата чем порождающие ее метафоры, и даже могу примерно указать почему, как это понять.

В математике слабым отражением метафоры является функтор.Read more...Collapse )
Friday, June 10th, 2016
2:04 pm
[ << Previous 20 ]
About LiveJournal.com