Namdak Tonpa (maxim) wrote,
Namdak Tonpa
maxim

Идея для дисера, дарю!

Рабочее название: Непрерывные отображения лямбда термов

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

Пример. Точка — Юнит. Две точки — Булевый тип. Две точки и одна перменная — например обработчик ошибок OK | Err reason. Две точки и две переменных — протокол с кодом возврата OK value | Err reason. Или другое ветвление. Две точки, одна переменная и рекурсивное зацикливание или петля — List A = Nil | Cons A (List A). И так далее. Если вы запустите генератор такой группы (какая у нее симметрия?) то вы получите все возможные базовые библиотеки функциональных языков программирования. Напоминаю, согласно МакБрайду орнамента всего три: точка, переменная и рекурсивное зацикливание. Ну и переменных может быть любое количество, кодировать нумералами черча, как и вселенные.

В гомотопической теории еще конструктор Пути, или просто говоря равенство, четвертый орнамент. Там альтернативное ветвление такое. Путь — Отрезок. Точка и Путь — S1. Но конструктор пути многомерный! Поэтому. Сфера — это Точка и двумерный путь (движение одномерного пути). Дальше высшие сферы, конусы, надстройки и так далее. Возможно добавление трех предыдущих орнаментов, что означает добавление носителя, т.е. для первых поллов генератора — типы натуральных Nat = 0 | S Nat, целых Z = 0 | S | P, действительных R = Stream Digit чисел. Да, да, для действительных чисел нужна корекурсия и коиндуктивные типы, простейший из которых стрим. Стрим от листового конса отличается тем что у него элиминатор и интродакшин поменяны местами.

Добавление генерации коиндуктивных сигнатур будет создавать все возможные конкурентные программы изоморфные акторам и прочим моделям, которых множество, включая сети петри и прочую лабуду. Это врата в пи калкулус, линейные типы и другие категории. Пи калкулус — это когда мы паралельно можем симулировать выбранные нами коиндуктивные стримы. Все распределенные алгоритмы работают в этих категориях.

Кто нарисует карту? Так что б до монад хотябы. Можно будет создать роботов, которые будут искать неведанные нам сигнатуры и пытаться доказывать неведанные теоремы или находить точки в этих высших пространствах. Естественно все это подключить к роботам из бостон дайнамикс, или что там вселяет ужас в гуманоидов.
Tags: cs
  • Post a new comment

    Error

    default userpic

    Your IP address will be recorded 

  • 13 comments