OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Среда, 20 Ноябрь, 2019 15:02

Часовой пояс: UTC + 3 часа




Начать новую тему Ответить на тему  [ Сообщений: 14 ] 
Автор Сообщение
 Заголовок сообщения: Рекурсия vs. инварианты
СообщениеДобавлено: Пятница, 26 Июнь, 2009 07:56 

Зарегистрирован: Четверг, 12 Июль, 2007 23:18
Сообщения: 1982
Откуда: Узбекистан, Чирчик
Info21 писал(а):
Info21 писал(а):
Книжка "Алгоритмы и структуры данных. Версия для Оберона" после доработки ...
Осталась только глава про рекурсию. В смысле доработки. Но там легко, никаких инвариантов -- один день на свежую голову. Плюс дня четыре свежую голову обеспечить.
Вот видите как здорово! С рекурсиями ваши циклические инварианты нафик не нужны... :lol:

В смысле -- правильная рекурсия сама себе инвариант!


Последний раз редактировалось Geniepro Пятница, 26 Июнь, 2009 14:03, всего редактировалось 2 раз(а).

Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Планы и их прогресс
СообщениеДобавлено: Пятница, 26 Июнь, 2009 09:36 

Зарегистрирован: Понедельник, 30 Июль, 2007 10:53
Сообщения: 1538
Откуда: Беларусь, Минск
Если частный случай рекурсии - это цикл, тогда логично предположить, что частный случай её инварианта - инвариант цикла.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Планы и их прогресс
СообщениеДобавлено: Пятница, 26 Июнь, 2009 09:57 

Зарегистрирован: Четверг, 12 Июль, 2007 23:18
Сообщения: 1982
Откуда: Узбекистан, Чирчик
Valery Solovey писал(а):
Если частный случай рекурсии - это цикл, тогда логично предположить, что частный случай её инварианта - инвариант цикла.

Вообще, если уж действительно серьёзно пользоваться инвариантами, то программа, нарушающая эти инварианты, просто не должна компилироваться.
И приходим к чему-то вроде зависимых типов...


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: ?-1
СообщениеДобавлено: Пятница, 26 Июнь, 2009 13:44 

Зарегистрирован: Суббота, 07 Март, 2009 15:39
Сообщения: 3109
Откуда: Астрахань
Приходим практически к Эйфелю Бертрана Мейера.
Книжка 1500 страниц :mrgreen:


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: ?-1
СообщениеДобавлено: Пятница, 26 Июнь, 2009 14:13 

Зарегистрирован: Четверг, 12 Июль, 2007 23:18
Сообщения: 1982
Откуда: Узбекистан, Чирчик
Валерий Лаптев писал(а):
Приходим практически к Эйфелю Бертрана Мейера.
Книжка 1500 страниц :mrgreen:

А там разве инварианты статически проверятся, при компиляции? Не помню, что бы писалось об этом -- вроде только динамически...


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Рекурсия vs. инварианты
СообщениеДобавлено: Пятница, 26 Июнь, 2009 15:02 

Зарегистрирован: Суббота, 07 Март, 2009 15:39
Сообщения: 3109
Откуда: Астрахань
Седни посмотрю дома в книжку - мож чего написано подробнее.
Статически инвариант же не проверить.
Статически - это доказательство правильности.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Рекурсия vs. инварианты
СообщениеДобавлено: Пятница, 26 Июнь, 2009 16:18 

Зарегистрирован: Четверг, 12 Июль, 2007 23:18
Сообщения: 1982
Откуда: Узбекистан, Чирчик
Валерий Лаптев писал(а):
Статически инвариант же не проверить.
Статически - это доказательство правильности.

Вот-вот! Для того и придумали зависимые типы, что бы статически проверять инварианты...


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Рекурсия vs. инварианты
СообщениеДобавлено: Пятница, 26 Июнь, 2009 18:59 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8196
Откуда: Троицк, Москва
Geniepro писал(а):
Валерий Лаптев писал(а):
Статически инвариант же не проверить.
Статически - это доказательство правильности.

Вот-вот! Для того и придумали зависимые типы, что бы статически проверять инварианты...
Гениально. Может, вообще всё будем статически вычислять?


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Рекурсия vs. инварианты
СообщениеДобавлено: Пятница, 26 Июнь, 2009 19:52 

Зарегистрирован: Суббота, 26 Ноябрь, 2005 18:38
Сообщения: 1857
Info21 писал(а):
Гениально. Может, вообще всё будем статически вычислять?


Все что можно - да.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Рекурсия vs. инварианты
СообщениеДобавлено: Пятница, 26 Июнь, 2009 20:17 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9159
Откуда: Россия, Орёл
Geniepro писал(а):
что бы статически проверять инварианты...

Те инварианты, которые можно проверить статически, тривиальны.

Разница между статикой и динамикой - это разница между полной разрешимостью и частичной (знаём всё множество интересующих нас вещей; или всего лишь имеем возможность относительно каждого конкретного объектов - конкретного хода выполнения - проверить его принадлежность к множеству).

Разница фундаментальная, и хоть убей себя ап стену :) Ну дык программёрам закон не писан.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Рекурсия vs. инварианты
СообщениеДобавлено: Пятница, 26 Июнь, 2009 20:22 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9159
Откуда: Россия, Орёл
Geniepro писал(а):
В смысле -- правильная рекурсия сама себе инвариант!


Сначала получите её - правильную.
Проведите доказательство рекурсии - через неподвижную точку функции и т.п. - повеселитесь.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Рекурсия vs. инварианты
СообщениеДобавлено: Суббота, 27 Июнь, 2009 01:04 

Зарегистрирован: Суббота, 26 Ноябрь, 2005 18:38
Сообщения: 1857
Илья Ермаков писал(а):
Те инварианты, которые можно проверить статически, тривиальны.


Это в обероне - ничего кроме тривиальных и не проверишь при все желании :) Поэтому даже мысли не возникает о том, что вот эти и эти и эти инварианты замечательно выносятся в статику.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Рекурсия vs. инварианты
СообщениеДобавлено: Суббота, 27 Июнь, 2009 10:30 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8196
Откуда: Троицк, Москва
Vlad писал(а):
Илья Ермаков писал(а):
Те инварианты, которые можно проверить статически, тривиальны.
Это в обероне ...

Да нет. Это определение тривиальности вообще.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Рекурсия vs. инварианты
СообщениеДобавлено: Суббота, 27 Июнь, 2009 11:54 

Зарегистрирован: Суббота, 07 Март, 2009 15:39
Сообщения: 3109
Откуда: Астрахань
Илья Ермаков писал(а):
Geniepro писал(а):
что бы статически проверять инварианты...

Те инварианты, которые можно проверить статически, тривиальны.

Разница между статикой и динамикой - это разница между полной разрешимостью и частичной (знаём всё множество интересующих нас вещей; или всего лишь имеем возможность относительно каждого конкретного объектов - конкретного хода выполнения - проверить его принадлежность к множеству).

Разница фундаментальная, и хоть убей себя ап стену :) Ну дык программёрам закон не писан.

Ну почему же не писан.
Просто о разных вещах говорится. Влад, как я понял, намекает на то, что нужно максимально применять что-то вроде шаблонов - для вычислений на этапе компиляции.
Смотрим на Ершова и его смешанные вычисления. Статика - это как раз подстановка максимально возможного количества известных параметров. А все, что осталось - это и есть исполняемая программа.
Ну, и ИМХО, "всего лишь имеем возможность проверить... принадлежность множеству" - это и есть РЕАЛЬНЫЕ задачи. Ибо множества, как правило либо бесконечные, либо очень большие... :)


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 14 ] 

Часовой пояс: UTC + 3 часа


Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 1


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Вся информация, размещаемая участниками на конференции (тексты сообщений, вложения и пр.) © 2005-2019, участники конференции «OberonCore», если специально не оговорено иное.
Администрация не несет ответственности за мнения, стиль и достоверность высказываний участников, равно как и за безопасность материалов, предоставляемых участниками во вложениях.
Без разрешения участников и ссылки на конференцию «OberonCore» любое воспроизведение и/или копирование высказываний полностью и/или по частям запрещено.
Powered by phpBB® Forum Software © phpBB Group
Русская поддержка phpBB