Изучал автоматическую теорию управления в универе. Это потрясающе.
Описываем модель. Накладываем желаемые ограничения, подмножество желаемых состояний. Играемся с уравнениями, применяем разные теоремы чтобы получить функцию управления системой.
Я заметил, что программы по-сути тоже динамические системы. Также как и в классических динамических системах там есть состояние, есть время, есть ввод и вывод.
Просто они существуют не в векторном пространстве вещественных числе R^n, а в векторном пространстве нулей и единиц: https://en.wikipedia.org/wiki/Vector_logic
Хочу описывать программы как уравнения, исследовать их сходимость к определённому подмножеству состояний.
Как ни искал, чёт не могу найти чтобы кто-то это уже делал, хотя идея вроде бы лежит на поверхности.
Кто-нибудь занимался чем-то похожим? Накидайте ссылок или ключевых слов по которым можно что-то похожее найти
Описываем модель. Накладываем желаемые ограничения, подмножество желаемых состояний. Играемся с уравнениями, применяем разные теоремы чтобы получить функцию управления системой.
Я заметил, что программы по-сути тоже динамические системы. Также как и в классических динамических системах там есть состояние, есть время, есть ввод и вывод.
Просто они существуют не в векторном пространстве вещественных числе R^n, а в векторном пространстве нулей и единиц: https://en.wikipedia.org/wiki/Vector_logic
Хочу описывать программы как уравнения, исследовать их сходимость к определённому подмножеству состояний.
Как ни искал, чёт не могу найти чтобы кто-то это уже делал, хотя идея вроде бы лежит на поверхности.
Кто-нибудь занимался чем-то похожим? Накидайте ссылок или ключевых слов по которым можно что-то похожее найти
Не хочу разочаровывать твой восторженный школьный мозг. Сам был таким же ещё пару лет назад, лол. Но в универе разбирают только toy examples. Т.е. в реальной разработке это всё непременимо. Серьёзно, венец использования прикладного матанчика - это нейронки, причём матанчика довольно примитивного, фактически там просто градиентный спуск и пару безпруфных, чисто жмпирических идей из башки. И всё, что могут эти нейронки - генерировать бред, используя при этом огромные вычислительные мощности. Тебе не об этом нужно думать, а как по-бустрее вкатиться и лутать хотя бы пару тысяч бачей в месяц. Всё остальное вторично.
>>297323 (OP)
Функциональную и логическую парадигмы придумали ещё на заре программирования. Вот только на практике эта не прижилось, писать алгоритмы пошагового изменения состояния оказалось тупо удобнее и быстрее, чем трёхэтажные уравнения. Программы больше похожи на инженерные изделия, чем на физические системы, описываемые уравнениями.
Функциональную и логическую парадигмы придумали ещё на заре программирования. Вот только на практике эта не прижилось, писать алгоритмы пошагового изменения состояния оказалось тупо удобнее и быстрее, чем трёхэтажные уравнения. Программы больше похожи на инженерные изделия, чем на физические системы, описываемые уравнениями.
>>297323 (OP)
Ты не поверишь... Матлаб/Simulink умеет генерировать код. https://www.mathworks.com/help/overview/code-generation.html По-твоему, на кой хуй вообще существует матлаб? Его чё ради прикола чтоли создали? Чисто шоп поиграться/поугарать, но кстати он не единственный. Их куча подобных решений.
>Хочу описывать программы как уравнения
>чёт не могу найти чтобы кто-то это уже делал
Ты не поверишь... Матлаб/Simulink умеет генерировать код. https://www.mathworks.com/help/overview/code-generation.html По-твоему, на кой хуй вообще существует матлаб? Его чё ради прикола чтоли создали? Чисто шоп поиграться/поугарать, но кстати он не единственный. Их куча подобных решений.
>>297328
То о чём говорится в посте в универе и не изучается. Это вообще неисследованная тема. Не понимаю к чему ты всё это написал.
Уже был там, 10+ лет опыта в программировании.
> Не хочу разочаровывать твой восторженный школьный мозг.
> Но в универе разбирают только toy examples. Т.е. в реальной разработке это всё непременимо.
То о чём говорится в посте в универе и не изучается. Это вообще неисследованная тема. Не понимаю к чему ты всё это написал.
> Тебе не об этом нужно думать, а как по-бустрее вкатиться и лутать хотя бы пару тысяч бачей в месяц.
Уже был там, 10+ лет опыта в программировании.
>>297337
Логические языки максимально близко подошли к идее "программы как уравнения". Если посмотреть на Dedalus, его @next клозы почти напоминают dx/dt = f(x).
Но почему-то их так и не привели к привычному выражению динамических систем.
Они сегодня похожи, потому что у нас тупо выбора нет. Нет инструментов.
Когда-то детали не моделировали, просто на глаз хуячили молотком. Сегодня мы так пишем софт.
В промышленности ты можешь указать желаемые свойства детали, нажать на кнопку и получить новую форму детали. Путём решения какие-то уравнений и симуляций.
А мы сегодня пишем распределённый алгоритм для акторной системы, но не можем указать требование отсутствия дедлока, нажать на кнопку, и получить новую модифицированную программу где этого дедлока не будет.
ОП
>Функциональную и логическую парадигмы придумали ещё на заре программирования. Вот только на практике эта не прижилось, писать алгоритмы пошагового изменения состояния оказалось тупо удобнее и быстрее,
Логические языки максимально близко подошли к идее "программы как уравнения". Если посмотреть на Dedalus, его @next клозы почти напоминают dx/dt = f(x).
Но почему-то их так и не привели к привычному выражению динамических систем.
> Программы больше похожи на инженерные изделия, чем на физические системы, описываемые уравнениями.
Они сегодня похожи, потому что у нас тупо выбора нет. Нет инструментов.
Когда-то детали не моделировали, просто на глаз хуячили молотком. Сегодня мы так пишем софт.
В промышленности ты можешь указать желаемые свойства детали, нажать на кнопку и получить новую форму детали. Путём решения какие-то уравнений и симуляций.
А мы сегодня пишем распределённый алгоритм для акторной системы, но не можем указать требование отсутствия дедлока, нажать на кнопку, и получить новую модифицированную программу где этого дедлока не будет.
ОП
>>297337
Так и не надо писать уравнения.
Надо найти математический аппарат позволяющий выразить программы матрицами для какого-то векторного пространства состояний, позволяющий исследовать свойства программ.
А потом придумать ЯП, который будет иметь ту же семантику.
Скорее всего это будет какой-то модифицированный Пролог или около того. Не нужно будет писать никаких уравнений.
ОП
>писать алгоритмы пошагового изменения состояния оказалось тупо удобнее и быстрее, чем трёхэтажные уравнения.
Так и не надо писать уравнения.
Надо найти математический аппарат позволяющий выразить программы матрицами для какого-то векторного пространства состояний, позволяющий исследовать свойства программ.
А потом придумать ЯП, который будет иметь ту же семантику.
Скорее всего это будет какой-то модифицированный Пролог или около того. Не нужно будет писать никаких уравнений.
ОП
>>297353
Про симулинк забыл кстати, спасибо. Посмотрю на в каких терминах там выражаются системы. Похожи ли они на динамические системы с векторным пространством состояний.
Если не трудно, можешь вкинуть пару названий, ключевых слов? Я чёт искал, но не находил ничего интересного.
ОП
>Ты не поверишь... Матлаб/Simulink умеет генерировать код.
Про симулинк забыл кстати, спасибо. Посмотрю на в каких терминах там выражаются системы. Похожи ли они на динамические системы с векторным пространством состояний.
> но кстати он не единственный. Их куча подобных решений.
Если не трудно, можешь вкинуть пару названий, ключевых слов? Я чёт искал, но не находил ничего интересного.
ОП
>>297353
Щас посмотрел симулинк, в нём моделируются непрерывные динамические системы.
В программах же время дискретное, логическое, не то же самое.
Там есть блоки для дискретного управления, но они лишь сэмплируют непрерывное время, вместо того делать всю систему дискретной.
Наверное можно что-то нагородить сверху, но кажется это не тот инструмент. Не то о чём я говорил в изначальном посте.
ОП
>Ты не поверишь... Матлаб/Simulink умеет генерировать код. https://www.mathworks.com/help/overview/code-generation.html По-твоему, на кой хуй вообще существует матлаб?
Щас посмотрел симулинк, в нём моделируются непрерывные динамические системы.
В программах же время дискретное, логическое, не то же самое.
Там есть блоки для дискретного управления, но они лишь сэмплируют непрерывное время, вместо того делать всю систему дискретной.
Наверное можно что-то нагородить сверху, но кажется это не тот инструмент. Не то о чём я говорил в изначальном посте.
ОП
>>297404
очко с ОПа горит, да сладкий?
очко с ОПа горит, да сладкий?
>>297392
LabVIEW же очевидный. Набери просто в гугле "software for mathematical modelling". Там их куча.
В чём конкретно смысл твоего треда? Ну окей, какие-то уравнения перевел в код. Иииииии? Что это даёт? Корректность? Есть язык TLA+ который проверяет математическую корректность алгоритма. Оптимизацию? Есть язык AMPL, программа arena для оптимизаций. Сложные мат модели? Ну есть матлаб для этого. Тот же magnolia есть, который тоже может модели создавать.
LabVIEW же очевидный. Набери просто в гугле "software for mathematical modelling". Там их куча.
В чём конкретно смысл твоего треда? Ну окей, какие-то уравнения перевел в код. Иииииии? Что это даёт? Корректность? Есть язык TLA+ который проверяет математическую корректность алгоритма. Оптимизацию? Есть язык AMPL, программа arena для оптимизаций. Сложные мат модели? Ну есть матлаб для этого. Тот же magnolia есть, который тоже может модели создавать.
>>297405
Ну посмотри ещё modelica, juliaControl controlSystems.jl на гитаре там гозиллион тулбоксов под теорию управления.
Ну посмотри ещё modelica, juliaControl controlSystems.jl на гитаре там гозиллион тулбоксов под теорию управления.
>>297383
Лол, дауненок без образования программировал 10 лет коммерчески а потом решил изучить матан и теперь радуется как школьник-максималист высирая бредовые идеи. Хех мде.
>Уже был там, 10+ лет опыта в программировании.
Лол, дауненок без образования программировал 10 лет коммерчески а потом решил изучить матан и теперь радуется как школьник-максималист высирая бредовые идеи. Хех мде.
>>297619
Будто что-то плохое. Порадовался бы за чувачка.
мимо такой же кодер вебмакака взялся за книжку Math for programmers
>Лол, дауненок без образования программировал 10 лет коммерчески а потом решил изучить матан
Будто что-то плохое. Порадовался бы за чувачка.
мимо такой же кодер вебмакака взялся за книжку Math for programmers
>>298507
Таким не место в айти. Даже в роли веб макаки.
Таким не место в айти. Даже в роли веб макаки.
>>297405
Simulink прекрасно работает и с дискретным моделями
Simulink прекрасно работает и с дискретным моделями
>>297323 (OP)
есть такая абстракция, как машина Тьюринга
есть т.н. проблема останова машины Тьюринга, и она алгоритмически не разрешима - т.е. зная описание алгоритма для МТ и входные данные, нельзя сказать, придет ли алгоритм к какому-то конечному решению или зациклится
>Хочу описывать программы как уравнения,
есть такая абстракция, как машина Тьюринга
> исследовать их сходимость к определённому подмножеству состояний.
есть т.н. проблема останова машины Тьюринга, и она алгоритмически не разрешима - т.е. зная описание алгоритма для МТ и входные данные, нельзя сказать, придет ли алгоритм к какому-то конечному решению или зациклится
332 Кб, 1024x1280>>301176
Дружок, и лямбда исчисления ещё есть.
Но они не позволяют исследовать программу как динамическую систему.
В общем виде она конечно неразрешима. Но если мы берём конкретный алгоритм и его исследуем, может можно что-то найти.
Дифференциальные уравнения в общем виде тоже не решаются. Но некоторые классы уравнений -- вполне решаются, есть специальные техники.
Тут то же самое.
ОП
>есть такая абстракция, как машина Тьюринга
Дружок, и лямбда исчисления ещё есть.
Но они не позволяют исследовать программу как динамическую систему.
> есть т.н. проблема останова машины Тьюринга, и она алгоритмически не разрешима
В общем виде она конечно неразрешима. Но если мы берём конкретный алгоритм и его исследуем, может можно что-то найти.
Дифференциальные уравнения в общем виде тоже не решаются. Но некоторые классы уравнений -- вполне решаются, есть специальные техники.
Тут то же самое.
ОП
>>301176
Во, я понял.
Лямбда Исчисление и Машина Тьюринга описывают компьютер архитектуры фон Неймана, где и данные и программа все хранятся в едином пространстве.
Это более мощная и гибкая абстракция, но и анализировать её сложнее.
То что я ищу, это абстракция для Гарвардской архитектуры, где код программы и данные разделены.
У меня данные это вектор состояния, программа это сами уравнения. Одно нельзя перелить в другое и наоборот.
Соответственно система, менее гибкая, менее мощная, и соответственно больше закономерностей о её поведении можно предсказать.
ОП
Во, я понял.
Лямбда Исчисление и Машина Тьюринга описывают компьютер архитектуры фон Неймана, где и данные и программа все хранятся в едином пространстве.
Это более мощная и гибкая абстракция, но и анализировать её сложнее.
То что я ищу, это абстракция для Гарвардской архитектуры, где код программы и данные разделены.
У меня данные это вектор состояния, программа это сами уравнения. Одно нельзя перелить в другое и наоборот.
Соответственно система, менее гибкая, менее мощная, и соответственно больше закономерностей о её поведении можно предсказать.
ОП
>>297323 (OP)
Ты лучше с электросхемами такое проверни
>
>Хочу описывать программы как уравнения, исследовать их сходимость к определённому подмножеству состояний.
>
Ты лучше с электросхемами такое проверни
>>297323 (OP)
Вот тебе ключевики: теория вычислимости, частично-рекурсивные функции, машина Тьюринга, лямбда-исчисления
Вот тебе ключевики: теория вычислимости, частично-рекурсивные функции, машина Тьюринга, лямбда-исчисления
>>302994
Ещё можешь про формальную верификацию алгоритмов почитать. Там тоже что-то похожее может быть.
Ещё можешь про формальную верификацию алгоритмов почитать. Там тоже что-то похожее может быть.
