Comments 19
Буквально прошлым утром читал про специализацию программ и прогонку на сайте Института Рефала ИПС РАН, а сегодня утром — эта статья.
Кто-то сдал математическую логику :)
А по сути статьи — что вы подразумеваете под анализом программы? Как будут реализованы «грязные» (с побочными эффектами в виде вывода на экран) функции? Чем это кардинально отличается от нынешних функциональных языков?
А по сути статьи — что вы подразумеваете под анализом программы? Как будут реализованы «грязные» (с побочными эффектами в виде вывода на экран) функции? Чем это кардинально отличается от нынешних функциональных языков?
Нет, кто-то пишет вступительный раздел диссертации и хочет при этом провести время с пользой.
Под анализом программы имеется в виду нахождения способа ее разбития. «Грязные» функции пусть остаются грязными. Дело в том, что, как писалось ранее, всезаменяющее решение не предлагается. Тут скорее хотелось бы предложить средство проектирования именно вычислительных задач, забыв при этом что «грязные функции» существуют. Собственно, как я себе представляю это:
1. Человек строит композиционное представление решения задачи, разбивая ее на композиции.
2. Решение задачи автоматически конвертируется в один из языков программирования, да и не только программирования. Я, например, разработал конвертер такого решения в Verilog.
3. Дописывается все остальное прямо не имеющее отношение к вычислениям ввод-вывод, например.
Чем кардинально отличается? Я в статье ответил, может, надо было еще более ярко подчеркнуть. Я не видел средств порождения новых композиций. Собственно это и хотелось бы предложить в своей работе.
Под анализом программы имеется в виду нахождения способа ее разбития. «Грязные» функции пусть остаются грязными. Дело в том, что, как писалось ранее, всезаменяющее решение не предлагается. Тут скорее хотелось бы предложить средство проектирования именно вычислительных задач, забыв при этом что «грязные функции» существуют. Собственно, как я себе представляю это:
1. Человек строит композиционное представление решения задачи, разбивая ее на композиции.
2. Решение задачи автоматически конвертируется в один из языков программирования, да и не только программирования. Я, например, разработал конвертер такого решения в Verilog.
3. Дописывается все остальное прямо не имеющее отношение к вычислениям ввод-вывод, например.
Чем кардинально отличается? Я в статье ответил, может, надо было еще более ярко подчеркнуть. Я не видел средств порождения новых композиций. Собственно это и хотелось бы предложить в своей работе.
Никогда не понимал. Как в таких измышлизмах волшебным образом у функций то появляется аргумент X, то вообще исчезает обозначение (X). Да, высшая математика — это не мое, не нашел еще ни одного человека и книги, с помощью которых понял бы эти вещи.
Все зависит от уровня абстракции, на котором работаем. Если мы записываем композиции, то X не нужен, так как функции выполняют роль аргумента. Но как только композицию применили, то X появляется. Так как примененная композиция над заданными функциями в результате дает тоже функцию. Надеюсь помогло. Может, картинку надо нарисовать, не знаю :)
Я думаю что такие языки не распространены по причине своей ограниченной применимости. Далеко не всегда стоит задача математически строгого обоснования решения. Приведу пример из курса математической физики, который нам читали в универе.
Мы тогда разбирали уравнение колебаний струны. На лекциях была доказана единственность решения и долго-долго разбирали доказательство существования решения и ограничения на граничные условия, чтобы доказать сходимость получаемого ряда. А на семинарах мы вовсю решали данные задачи и не занимались доказательством сходимости ряда, т.к. «из физической интуиции» ясно что задача имеет решение, а значит ряд удовлетворяющий уравнению является решением, по свойству единственности решения.
Аналогично возьмём пример из программирования — минимальное количество бинарных операций (вентилей) реализующие заданную функцию. Построить функцию гораздо легче, чем найти точную нижнюю границу количества операций. Для «прикладных» задач не всегда нужно точное математическое описание (хотя иногда необходимо), а Computer Science меньше оперирует языками программирования.
А если говорить по делу то, как мне кажется, полезно отделять описание алгоритма от его программной реализации. Для описания существуют, например, блок-схемы или UML. Они не зависят от окружения в котором будут исполняться и наглядны (иногда). А для реализации существует куча ЯП, роблегчающих тот или иной аспект. Пример — доступ к предпоследнему символу строки в языке Python: my_str[-2] — это короткая запись эквивалентна my_str[len(my_str) — 2], но проще, короче и менее подвержена ошибкам. И скрывает детали реализации, ненужные в данный момент прикладному программисту. Хотя и затрудняет верификацию программы.
Вообщем хочется помянуть пост о необходимости прямой работы с памятью в некоторых случаях.
Мы тогда разбирали уравнение колебаний струны. На лекциях была доказана единственность решения и долго-долго разбирали доказательство существования решения и ограничения на граничные условия, чтобы доказать сходимость получаемого ряда. А на семинарах мы вовсю решали данные задачи и не занимались доказательством сходимости ряда, т.к. «из физической интуиции» ясно что задача имеет решение, а значит ряд удовлетворяющий уравнению является решением, по свойству единственности решения.
Аналогично возьмём пример из программирования — минимальное количество бинарных операций (вентилей) реализующие заданную функцию. Построить функцию гораздо легче, чем найти точную нижнюю границу количества операций. Для «прикладных» задач не всегда нужно точное математическое описание (хотя иногда необходимо), а Computer Science меньше оперирует языками программирования.
А если говорить по делу то, как мне кажется, полезно отделять описание алгоритма от его программной реализации. Для описания существуют, например, блок-схемы или UML. Они не зависят от окружения в котором будут исполняться и наглядны (иногда). А для реализации существует куча ЯП, роблегчающих тот или иной аспект. Пример — доступ к предпоследнему символу строки в языке Python: my_str[-2] — это короткая запись эквивалентна my_str[len(my_str) — 2], но проще, короче и менее подвержена ошибкам. И скрывает детали реализации, ненужные в данный момент прикладному программисту. Хотя и затрудняет верификацию программы.
Вообщем хочется помянуть пост о необходимости прямой работы с памятью в некоторых случаях.
Мне кажется что описанный вами композиционный подход имеет будущее не как язык программирования, а как язык общения математиков.
Возможно что будут (если ещё нет) программные пакеты для проверки истинности утверждений записанных в данном формализме.
Возможно что будут (если ещё нет) программные пакеты для проверки истинности утверждений записанных в данном формализме.
как язык общения математиков
Совершенно верно. Более того, согласитесь, ведь такую запись можно перевести в любой язык программирования машинным способом, так как алгоритм становится полностью формализованным. А разработчик потом ее доработает, добавив ввод-вывод, события, интерфейсы и т.д.
После перевода в «любой язык» может возникнуть куча сложностей:
А вот применение в ускорителях вычислений на базе ПЛИС с сильно ограниченным интерфейсом — весьма интересно. Ну и в совсем суровых DSP.
- Доказательство корректности перевода из математического описания в ЯП
- Ограниченность используемых возможностей ЯП в сгенерированном коде.
- Плохое оформление сгенерированного кода может привести к сложностям в доработках.
- Плохая поддержка «тонкостей» языка не связанных с математическим аппаратом. Например — поддержка инструкции count leading zeros. Либо мы её включаем как примитив в «математический» язык, что плохо. Либо нужно чтобы транслятор понимал что данный «математический» код сводится к единственной инструкции в «нативном» и т.д.
А вот применение в ускорителях вычислений на базе ПЛИС с сильно ограниченным интерфейсом — весьма интересно. Ну и в совсем суровых DSP.
Благо корректность такого «переводчика», надо доказывать один раз. А корректность конкретной переведенной программы будет наследоваться от корректности построенной функции (тут поправьте, если не прав).
Насчет третьего пункта, то в с генерированном коде важна только интерфейсная часть, т.к. с учетом того, что он предположительно корректен, никто туда лезть не будет. Ну кроме того случая, когда надо внести улучшения, но это приводит к необходимости доказывать корректность еще раз.
Насчет тонкостей языка, то не обязательно опускаться на такой низкий уровень, когда надо считать нули вначале. Хотя в целом, действительно, много нюансов, но из-за этого не особо переживают разработчики GHC. Конечно, это не повод следовать их примеру, но единственное, что мы можем сделать в этом случае, так это лучше анализировать код, находить эвристики.
Также можно пофантазировать и представить сообщество, которое добавляет в общую базу кода код с «вручную» доказанной корректностью.
Справедливо всё замечено.
P.S. Собственно, всё и начиналось с того, что я пришел к своему научруку и сказал, что круто было бы делать «кастомные» вычислители на ПЛИС, максимально автоматизировав процесс генерации решения, а он доктор физико-математических наук и про ПЛИС и электронику в общем он мало чего знал, но сказал что может помочь заложить под это теоретический базис.
Насчет третьего пункта, то в с генерированном коде важна только интерфейсная часть, т.к. с учетом того, что он предположительно корректен, никто туда лезть не будет. Ну кроме того случая, когда надо внести улучшения, но это приводит к необходимости доказывать корректность еще раз.
Насчет тонкостей языка, то не обязательно опускаться на такой низкий уровень, когда надо считать нули вначале. Хотя в целом, действительно, много нюансов, но из-за этого не особо переживают разработчики GHC. Конечно, это не повод следовать их примеру, но единственное, что мы можем сделать в этом случае, так это лучше анализировать код, находить эвристики.
Также можно пофантазировать и представить сообщество, которое добавляет в общую базу кода код с «вручную» доказанной корректностью.
Справедливо всё замечено.
P.S. Собственно, всё и начиналось с того, что я пришел к своему научруку и сказал, что круто было бы делать «кастомные» вычислители на ПЛИС, максимально автоматизировав процесс генерации решения, а он доктор физико-математических наук и про ПЛИС и электронику в общем он мало чего знал, но сказал что может помочь заложить под это теоретический базис.
Безусловно корректность будет наследоваться. С этим я не спорю и даже сам пользуюсь таким подходом, хотя и в гораздо менее сложных теоретических случаях.
А вообще начинание, безусловно, интересное.
Кстати — а вы не изучали генерацию дизайнов ПЛИС средствами Matlab? Понимаю, что это не совсем то, чем вы собираетесь заняться, но вроде бы родственная штука.
не обязательно опускаться на такой низкий уровень, когда надо считать нули вначалеЯ боюсь что в некоторых вычислительных задачах это будет обязательно. Например при анализе вектора ошибки в каких-нибудь линейных кодах. Т.е. безусловно можно обойтись без этого. Или придётся сильно жертвовать быстродействием. Или после «ручных» оптимизаций узких мест доказывать уже только их корректность.
А вообще начинание, безусловно, интересное.
Кстати — а вы не изучали генерацию дизайнов ПЛИС средствами Matlab? Понимаю, что это не совсем то, чем вы собираетесь заняться, но вроде бы родственная штука.
Начнем с понятия программы. С математической точки зрения программа — это функция.
Вот этот посыл кажется мне спорным. Я бы допустил, что программа — это монада. А композиция монад существенно замысловатей композиции функций. Надеюсь вы не потеряете время впустую глянув к примеру Composing Monads Mark P. Jones and Luc Duponcheel, Research Report YALEU/DCS/RR-1004, Yale University, New Haven, Connecticut, USA, December 1993.[PDF]
UFO just landed and posted this here
Прочитал пост, так и не понял мысли за ней. Программа без побочных эффектов смысла не имеет. Если опустить побочные эффекты остаётся чистый математик с чистой математикой с помощью которой он может делать любую математику с помощью математики.
А если от компьютера нужна не математика, то надо либо начинать делать грязные функции, либо «потребности не-в-математике на сегодня не имеется».
А если от компьютера нужна не математика, то надо либо начинать делать грязные функции, либо «потребности не-в-математике на сегодня не имеется».
Мысль проста: там где возможно и разумно, почему бы не использовать композиционный подход, который может дать преимущества, описанные в статье. Это больше чем преимущества при просто применении функционального языка. В первую очередь, это иной подход к конструированию ПО, который заключается в абстрагировании от синтаксиса конкретного языка, а так же в автоматизированной поддержке (про средства поддержки позже напишу) мыслительного процесса человека, если он мыслит композициями. Моя вина, что как раз эту самую интересную тему в этом материале не задел. Так бы еще бы понятней было.
Естественно, но вместе с этим я ж не стремлюсь абсолютизировать, это было бы неправильно.
А если от компьютера нужна не математика, то надо либо начинать делать грязные функции, либо «потребности не-в-математике на сегодня не имеется».
Естественно, но вместе с этим я ж не стремлюсь абсолютизировать, это было бы неправильно.
UFO just landed and posted this here
Sign up to leave a comment.
Языки программирования. Композиционный взгляд