Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Прошлый пост

То, что прошлый пост написался 31 декабря – чистая случайность. Тем забавнее, что в нём я впервые смог сформулировать математическую мысль которая крутилась на самом деле весь год в голове:
– С тех пор как я поразбирался в HoTT я практически уверен, что это сила, кремень и будущее языков программирования и метаматематики.
– С тех пор как я начитался codedot'а я понял, что interaction nets рулят. Это реально элегантный, прозрачный, и оптимальный способ записывать пурые вычисления. Не то что машины Тьюринга, алгорифмы Маркова и лямбда-исчисление. Мне всегда казалось, что Fixpoint combinators и Church encoding это некрасивые dirty hacks, привносящие кучу нерелевантного произвола в модель вычислений, а теперь я убедился что это так.

Потом ещё под влиянием размышлений над макросами (спасибо xeno_by) я стал лиспером мне стало казаться, что тип данных AST должен быть в языках программирования явным и редукция выражений до представлений их значений тоже не должна быть под ковром. А в MLTT оно всё под ковром и очень лямбдёвое в плохом смысле. И вот с тех пор всё крутилось в голове, как бы так скрестить interaction nets и HoTT, да ещё чтобы выражения и их редукция были не под ковром. И вот потом щёлкнуло, что когда мы определяем новую функцию func, то это мы просто дополняем текущий тип AST ещё одним конструктором func, но при этом сразу определяем редукцию, при помощи которой этот конструктор может быть убран. Вот и получился прошлый пост.

На самом деле я уверен, что под тем или иным соусом это точно можно реализовать, и что соответствие Directed Inductive Types ~ Interaction Nets может оказаться весьма глубоким. Например, что такое равенства путей в сетях взаимодействия? — это формализация возможных оптимизаций. Возможно для чего-то может понадобится направленность и на этом уровне, ведь эти самые directed cubical sets как раз используются для того чтобы изучать Higher Automata (n-мерный автомат это просто автомат, у которого n лент ввода, на которые он реагирует независимо, не считая блокировок внутри, которые как раз и есть гомотопические свойства автомата).

Ну и отдельная тема, что HoTT неаскетичная теория, так что в идеале хотелось бы получить её точную истинную модель в рамках какой-нибудь совсем аскетичной теории, где ничего кроме натуральных чисел и диофантовых уравнений. ;-) См. http://akuklev.livejournal.com/1138512.html, естественно. Там всё, конечно, вообще вилами по воде писано, но больно уж красиво.
Tags: fprog
Subscribe

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

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

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 6 comments