Комментарии 16
Отлично. Порадовал. Будет продолжение?
А чего хотелось бы?
вообще, я уже лет 10 разрабатываю теорию под минимальный комплект операторов для Тьюринг-полноты. По типу "все из ничего". Об этом я наверняка еще напишу - но не скоро. Пока что активно работаю над книжкой "Путеводитель по миру головоломок" (могу прислать в лс ссыль на блог, если тут нельзя)
Вот список Тьюринг-неполных языков, который мне предоставил человек, более знающий в теме, чем я (не могу оценить корректность, так что не ко мне претензии): Lean4, Idris, Coq, ...
Тьюринг полнота это не про написать любую ПРОГРАММУ а про смоделировать любую ФУНКЦИЮ. В песочнице браузера нельзя залезть в файловую систему но это не делает js неполным по Тьюрингу. Сложение в паре с умножением являются Тьюринг полными, что позволяет команде x86 mov быть Тьюринг полной (да, там еще циклы, я в курсе). Если зайти с логических функций то базисами являются или-не и и-не (возможно и другие есть, пишу по памяти, одна из них штрих Шеффера другая стрелка Пирса). Хорошо раскурить понятие Тьюринг полноты можно по доказательству ограничений однослойного персептрона (Минский и Паперт) в частности невозможность им смоделировать операцию XOR, что и привело к появлению многослойный нейросетей. Доказательство простенькое и там есть наглядное геометрическое описание.
Так вот, Lean4 не знаю, но утверждать что Idris и Coq не Тьюринг полные - ну такое. В Coq можно задать типы данных на которых буксует автоматический вывод доказательств, это да. Но смоделировать на них можно любую вычислимую функцию. Ни к чему не призываю, но тому кто на серьезных щах с претензией на осведомленность сказал бы мне что Coq не Тьюринг полный я бы плюнул в рожицу...
Спасибо! Про "любую программу" я потому и взял в кавычки, что понимал, что "любая программа" - гораздо более широкое понятие, а сформулировать это точнее не смог. В общем, теперь уточнилось.
Про полноту компонентной базы даже были лекции в институте (МИЭТ). Про персептроны мало, что знаю, так как, хоть об этом и рассказывали, но, видимо, в силу того, что это было не столь присуще дисциплинам направления, пробежались по верхам.
Про "задать типы данных" мало, что понял, так как (еще раз) про эти языки говорил не я - а товарищ. Спасибо, передам.
Моё утверждение касалось тоталити-чекера в этих языках. В Idris по крайней мере он не даёт написать либо функцию не сокращающуюся по хотя бы одному аргументу, либо не выдающую полезное каждый шаг бесконечного вычисления.
Тоталити-чекер конечно можно отключить, но на уровне типов все функции обязаны быть тотальными
Ну и разумеется тотальное подмножество Идриса не тьюринг-полное.
В Coq и Lean думаю похоже, так как они суть вариации на ту же тему хоть и на исчислении конструкций, вместо Мартин-Лёфа
js неполным по Тьюрингу
а он разве полный?
..в частности невозможность им смоделировать операцию XOR, что и привело к появлению многослойный нейросетей. Доказательство простенькое и там есть наглядное геометрическое описание..
Я без понтов, скинь ссылку в личку, я не знаю такого(
формулу можно перевести в алгоритм, но, как перевести всякий алгоритм в формулу данной нотации, затрудняюсь ответить даже я.
…
В моей же нотации это можно записать так:
Как в Вашей нотации выглядит формализация алгоритма (он же процесс, workflow)? Например, какого либо алгоритма из
Формализация WF2M сети на примере алгоритма Кофе-машина и два ученых
Прочел. Это выше моего понимания)
Задача ровна та же, которую пытались решить алгебры процессов \ теория процессов и т.п. См. предыдущую перед указанной мной статьей (CCS).
На входе: алгоритм - процесс - workflow со всякими развилками типа and \ or \ xor (в любой WF-нотации), механизмы синхронизации ветвлений и взаимодействия с внешним окружением (такими же процессами), а на выходе - формальная (математическая) запись, адекватная (т.е. модель) реальному (точнее нарисованному, но исходному) процессу.
Хотя матрицы смежности и инцендентности даже знакомы
О мат-нотациях и Машинах Тьюринга