Выражение инвариантов на языке функ На этой странице я буду выкладывать часть своих мыслей по связи понятий функи и инварианта. Здесь я смотрю на функу и С++-подобный "псевдокод" лишь как на способ очень просто описывать классы функций, удовлетворяющие заданным свойствам.Cвойства
Пусть задана функция f:A->B. Ее свойством будем называть пару (g:AxA->{0,1}, h:BxB->{0,1}) такая, что если g(a1,a2)=1, то и h(f(a1),f(a2))=1. Инварианты (см. ниже) - частный случай "свойств".
1. Выражение четких инвариантов. Наивный - задается две функи, одна из которых описывает преобразование входа (т.е. принимает структуру-вход и возвращает структуру того же типа), а вторая - соответствующее преобразование выхода (принимает структуру-выход, возвращает структуру того же типа). Иначе говоря, заданы две функи: void TransformEntry( SEntry* ); void TransformOutlet( SOutlet* ); эти функи интерпретируются так: если применить к входу функу TransformEntry, то выход изменится так, как если бы к нему была применена TransformOutlet. Параметризованный - задается тип TParam, и функи void TransformEntry( SEntry*, const TParam& ); void TransformOutlet( SOutlet* ); Этим функции интерпретируются так: если выбрать некоторое произвольное значение TParam, и применить к входу функу TransformEntry (с этим значением в качестве второго аргумента), то выход изменится так, как если бы к нему была применена TransformOutlet с тем же самым вторым аргументом. На множестве TParam должна быть задана структура группы так, что TransformEntry( &entry, a ); TransformEntry( &entry, b ) преобразует вход в точности то же, что TransformEntry( &entry, b*a ). Наивный способ, хоть и дословно соответствует определению инварианта, гораздо менее гибкий. Так, например, первым способом невозможно описать такой инвариант, как "если интерпретировать вход, как список координат точек на плоскости, то инвариантом является поворот всего множества точек вокруг произвольной точки на произвольный угол". К тому же, наивный способ является частным случаем параметризованного. Поэтому мы далее будем рассматривать только параметризованный способ. В дальнейшем множество, состоящее из некоторого входа и его преобразований при помощи TransformEntry со всеми возможными значениями TParam, будем называть инвариантной траекторией. Рассмотрим для начала идею того, как создать функу, выдерживающую заданный параметрически инвариант, в очень простом случае. Пусть TParam представляет собой некоторый enum (на котором задана структура циклической группы). Иначе говоря, параметр может принимать некоторое конечное число заранее известных значений. SOutlet MaxChooser( const SEntry& entry ) { bool bChanged = false; float fMax = mutable Chooser( entry ); SEntry realEntry = entry; TParam bestParam; foreach( param in TParam ) { SEntry temp = entry; TransformOutlet( &temp, param ); float fChooser = mutable Chooser( temp ); if ( fEffectiveness > fMax ) { bestParam = param; bChanged = true; fMax = fChooser; } } SOutlet out = mutable FinalTransform( realEntry ); if ( bChanged ) TransformOutlet( &out, bestParam ); return out; } Здесь нужно сделать замечание по синтаксису, которое заключается в том, что все mutable-части с одинаковым названием (в данном случае я имею в виду mutable Chooser) представляют собой вызов одной и той же функции. Этот пример довольно прост. Такая схема заставляет задать два вопроса: как быть, если мы не можем перебрать все возможные значения TParam (а такое происходит почти всегда)? И, что не менее важно, любая ли функция, имеющая инвариант ( TParam, TransformEntry, TransformOutlet ) может являться частным экземпляром данной функи? Ответ на второй вопрос кажется очевидным. В самом деле, пусть мы ищем некую функцию Transform. Очевидно, что если FinalTransform = Transform, то и MaxChooser совпадает с Transform. Но нас интересует не то, можем ли мы найти Transform "в принципе", а то, насколько такая схема облегчает поиск. Иначе говоря, насколько часто MaxChooser будет "случайно" совпадать с Transform? Всегда, когда Transform и FinalTransform совпадают на максимумах функции Chooser по инвариантным траекториям. Таким образом, в этой схеме от вида функции Chooser вообще практически ничего не зависит. Единственное ограничение, которое должно быть выполнено для этой функции, состоит в том, чтобы она не принимала равных значений на инвариантных траекториях. Немного усложнив пример, мы могли бы избавиться и от него, но сейчас это неважно. Чтобы ответить на первый вопрос, подумаем, каким свойством можно заменить конечность TParam. Мы использовали ее, чтобы найти значение входа, на котором некая функа Chooser максимальна. Таким образом, видоизменение схемы может быть получено так: на пару (TParam, Chooser) теперь накладывается единственное ограничение - максимум функи Chooser по инвариантной траектории entry может быть найден достаточно быстро для любого entry. 2. Выражение нестрогих инвариантов. 3. Выражение нечетких инвариантов. |