а не типизировать ли нам типы? ))
типизирование типов с точностью до изоморфизмов/гомоморфизмов
типа типизируем типы примерно
есть данные и есть операции, на операции можно смотреть как на данные
данные бывают какихто типов
операции бывают какихто типов
т.е. бывают типы данных и типы операций
значит бывают и типы типов
надо подумать и формализовать это
ps
Гомотопическая теория типов на пальцах.
https://deep-econom.livejournal.com/93934.html Теория категорий для школьников.
https://deep-econom.livejournal.com/42556.html главное это способ установления эквивалентности между типами, способ преобразования типов из одного в другой
как говорят )
гомоморфный образ группы до победы коммунизма
изоморфен факторгруппе по ядру гомоморфизма
Отношение изоморфизма на множестве однотипных алгебр является отношением эквивалентности.
Неразрешимые алгоритмические проблемы
http://mathhelpplanet.com/static.php?p=nerazreshimyye-algoritmicheskiye-problemy Алгоритмическая проблема - это проблема, в которой требуется найти единый метод (алгоритм) для решения бесконечной серии однотипных единичных задач. Такие проблемы называют также массовыми проблемами. Они возникали и решались в различных областях математики на протяжении всей ее истории. Примеры таких проблем рассматривались ранее.
---
такое бывает, это нормально )
в частности это означает существование случайности в математике, а поскольку математика суть модели, то некоторые задачи принципиально обладают решением, но не обладают общим решением казалось бы типовой проблемы
--
например
7. Случайность, порожденная математическими структурами.
https://deep-econom.livejournal.com/95947.html «Класс» уравнений порождается путём придания параметру k базового уравнения различных целочисленных значений.
диофантово уравнение k*x^2=2*k^2*y
где x,y неизвестные
k={1,2,3...} целочисленный параметр
оказывается число решений этого уравнения величина случайная.
---
http://mathhelpplanet.com/static.php?p=normalnyye-algoritmy-markovaНормальные алгоритмы Маркова
Марковские подстановки
--
ТЕОРЕМА (Маркова-Поста) Существует полугруппа, в которой проблема распознавания равенства слов алгоритмически неразрешима.
Пример Г.С.Цейтин нашел легко описываемый пример полугруппы, в которой проблема равенства слов алгоритмически неразрешима. В этой полугруппе всего пять образующих {а, 6, с, d, е} и семь определяющих соотношений
стр.83. Новиков Дискретная математика Учебник для вузов. 3-е изд
--
как решать такие вещи, это по сути говорит о неалгоритмизируемости многого, в том числе и ИСКИН, не так ли?
не страшно, мы легко преодолеваем всякие ограничения методом перебора и методом произвольной ассоциации (методом ненаучного тыка, методом создания новой модели как небывалой комбинации бывалых моделей), по сути выходим из формальной система в метасистему в произвольный момент времени и спускаемся снова в подтеорию, что конечно не гарантирует решение проблемы, но дает надежду иногда решать проблемы в частных случаях, как это и делает человек, так что это не является ограничением на создание ИСКИН, но является ограничением познания в целом, типа не все можно сделать быстро и легко, иногда думать надо
https://ru.wikipedia.org/wiki/L-система понятие Абстрактной Системы Редукций или ARS (от англ. Abstract Reduction Systems)
Каноничность или свойство Чёрча-Россера - конфлюентность плюс остановочность.
Переписывание - широкий спектр техник, методов и теоретических результатов, связанных с процедурами последовательной замены частей формул или термов формального языка по заданной схеме - системе переписывающих правил.
https://ru.wikipedia.org/wiki/Переписывание