| OberonCore https://forum.oberoncore.ru/ |
|
| Рекурсия vs. инварианты https://forum.oberoncore.ru/viewtopic.php?f=27&t=1675 |
Страница 1 из 1 |
| Автор: | Geniepro [ Пятница, 26 Июнь, 2009 07:56 ] |
| Заголовок сообщения: | Рекурсия vs. инварианты |
Info21 писал(а): Info21 писал(а): Книжка "Алгоритмы и структуры данных. Версия для Оберона" после доработки ... Осталась только глава про рекурсию. В смысле доработки. Но там легко, никаких инвариантов -- один день на свежую голову. Плюс дня четыре свежую голову обеспечить. В смысле -- правильная рекурсия сама себе инвариант! |
|
| Автор: | Valery Solovey [ Пятница, 26 Июнь, 2009 09:36 ] |
| Заголовок сообщения: | Re: Планы и их прогресс |
Если частный случай рекурсии - это цикл, тогда логично предположить, что частный случай её инварианта - инвариант цикла. |
|
| Автор: | Geniepro [ Пятница, 26 Июнь, 2009 09:57 ] |
| Заголовок сообщения: | Re: Планы и их прогресс |
Valery Solovey писал(а): Если частный случай рекурсии - это цикл, тогда логично предположить, что частный случай её инварианта - инвариант цикла. Вообще, если уж действительно серьёзно пользоваться инвариантами, то программа, нарушающая эти инварианты, просто не должна компилироваться. И приходим к чему-то вроде зависимых типов... |
|
| Автор: | Валерий Лаптев [ Пятница, 26 Июнь, 2009 13:44 ] |
| Заголовок сообщения: | Re: ?-1 |
Приходим практически к Эйфелю Бертрана Мейера. Книжка 1500 страниц 
|
|
| Автор: | Geniepro [ Пятница, 26 Июнь, 2009 14:13 ] |
| Заголовок сообщения: | Re: ?-1 |
Валерий Лаптев писал(а): Приходим практически к Эйфелю Бертрана Мейера. Книжка 1500 страниц А там разве инварианты статически проверятся, при компиляции? Не помню, что бы писалось об этом -- вроде только динамически... |
|
| Автор: | Валерий Лаптев [ Пятница, 26 Июнь, 2009 15:02 ] |
| Заголовок сообщения: | Re: Рекурсия vs. инварианты |
Седни посмотрю дома в книжку - мож чего написано подробнее. Статически инвариант же не проверить. Статически - это доказательство правильности. |
|
| Автор: | Geniepro [ Пятница, 26 Июнь, 2009 16:18 ] |
| Заголовок сообщения: | Re: Рекурсия vs. инварианты |
Валерий Лаптев писал(а): Статически инвариант же не проверить. Статически - это доказательство правильности. Вот-вот! Для того и придумали зависимые типы, что бы статически проверять инварианты... |
|
| Автор: | Info21 [ Пятница, 26 Июнь, 2009 18:59 ] |
| Заголовок сообщения: | Re: Рекурсия vs. инварианты |
Geniepro писал(а): Валерий Лаптев писал(а): Статически инвариант же не проверить. Статически - это доказательство правильности. Вот-вот! Для того и придумали зависимые типы, что бы статически проверять инварианты... |
|
| Автор: | Vlad [ Пятница, 26 Июнь, 2009 19:52 ] |
| Заголовок сообщения: | Re: Рекурсия vs. инварианты |
Info21 писал(а): Гениально. Может, вообще всё будем статически вычислять? Все что можно - да. |
|
| Автор: | Илья Ермаков [ Пятница, 26 Июнь, 2009 20:17 ] |
| Заголовок сообщения: | Re: Рекурсия vs. инварианты |
Geniepro писал(а): что бы статически проверять инварианты... Те инварианты, которые можно проверить статически, тривиальны. Разница между статикой и динамикой - это разница между полной разрешимостью и частичной (знаём всё множество интересующих нас вещей; или всего лишь имеем возможность относительно каждого конкретного объектов - конкретного хода выполнения - проверить его принадлежность к множеству). Разница фундаментальная, и хоть убей себя ап стену  Ну дык программёрам закон не писан.
|
|
| Автор: | Илья Ермаков [ Пятница, 26 Июнь, 2009 20:22 ] |
| Заголовок сообщения: | Re: Рекурсия vs. инварианты |
Geniepro писал(а): В смысле -- правильная рекурсия сама себе инвариант! Сначала получите её - правильную. Проведите доказательство рекурсии - через неподвижную точку функции и т.п. - повеселитесь. |
|
| Автор: | Vlad [ Суббота, 27 Июнь, 2009 01:04 ] |
| Заголовок сообщения: | Re: Рекурсия vs. инварианты |
Илья Ермаков писал(а): Те инварианты, которые можно проверить статически, тривиальны. Это в обероне - ничего кроме тривиальных и не проверишь при все желании Поэтому даже мысли не возникает о том, что вот эти и эти и эти инварианты замечательно выносятся в статику.
|
|
| Автор: | Info21 [ Суббота, 27 Июнь, 2009 10:30 ] |
| Заголовок сообщения: | Re: Рекурсия vs. инварианты |
Vlad писал(а): Илья Ермаков писал(а): Те инварианты, которые можно проверить статически, тривиальны. Это в обероне ...Да нет. Это определение тривиальности вообще. |
|
| Автор: | Валерий Лаптев [ Суббота, 27 Июнь, 2009 11:54 ] |
| Заголовок сообщения: | Re: Рекурсия vs. инварианты |
Илья Ермаков писал(а): Geniepro писал(а): что бы статически проверять инварианты... Те инварианты, которые можно проверить статически, тривиальны. Разница между статикой и динамикой - это разница между полной разрешимостью и частичной (знаём всё множество интересующих нас вещей; или всего лишь имеем возможность относительно каждого конкретного объектов - конкретного хода выполнения - проверить его принадлежность к множеству). Разница фундаментальная, и хоть убей себя ап стену Ну дык программёрам закон не писан.Ну почему же не писан. Просто о разных вещах говорится. Влад, как я понял, намекает на то, что нужно максимально применять что-то вроде шаблонов - для вычислений на этапе компиляции. Смотрим на Ершова и его смешанные вычисления. Статика - это как раз подстановка максимально возможного количества известных параметров. А все, что осталось - это и есть исполняемая программа. Ну, и ИМХО, "всего лишь имеем возможность проверить... принадлежность множеству" - это и есть РЕАЛЬНЫЕ задачи. Ибо множества, как правило либо бесконечные, либо очень большие...
|
|
| Страница 1 из 1 | Часовой пояс: UTC + 3 часа |
| Powered by phpBB® Forum Software © phpBB Group https://www.phpbb.com/ |
|