Перейти к содержанию

Инварианты исходных формул и алгоритмов

  • Статус: исполняемый контракт прослеживаемости задачи #201
  • Область действия: текущие скалярные формулы и конечные алгоритмы
  • Источник истины: исполняемый код и специализированные математические контракты

Карта прослеживаемости

Карта связывает каждое нетривиальное семейство реализаций с определением, граничным контрактом, численным обоснованием и исполняемыми проверками. Это указатель, а не вторая копия подробных доказательств.

Область реализации Определение или вывод Обязательный инвариант Исполняемые свидетельства
Исторические семейства функций принадлежности Контракты функций принадлежности Проверенная геометрия; устойчивые семейства насыщаются; формулы раскрывают границы переполнения tests/test_formula_algorithm_invariants.py, тесты контрактов функций принадлежности
Параметрическое и параболическое отрицания Контракты операторов и вывод Перестановка концов, неподвижная точка, монотонное убывание, инволютивность Тесты отрицаний и инвариантов формул
T-нормы, s-нормы и операции над множествами Явные операции Замкнутость, граничные тождества, ассоциативность, коммутативность и двойственность де Моргана Алгебраические и эталонные тесты операторов
Точная высота и нормализация Высота и нормализация Только точные свидетельства; положительная высота масштабируется к единице; нулевая высота вызывает ошибку Тесты нормализации и вычисляемых свойств
Аналитические и выборочные вычисляемые свойства Универсальное множество и поддержка Аналитическая геометрия точна; конечная выборка остаётся свидетельством с информацией о происхождении Тесты вычисляемых свойств и инвариантов формул
Нестрогие альфа-срезы и равномерная выборка Контракт альфа-срезов Граница >=, вложенность срезов, точный дискретный перебор, явное выборочное приближение Тесты альфа-срезов и инвариантов формул
Равенство и включение Равенство и включение Полное дискретное сравнение; ограниченное непрерывное утверждение; явный допуск Тесты отношений нечётких множеств
Центроидная дефаззификация Численная политика Аналитические моменты или детерминированная адаптивная квадратура Аналитические, граничные, исторические эталонные тесты и проверки сходимости

Численно чувствительные ветви

Параболическое отрицание

Неявное соотношение квадратично по \(d=y-x\). Прямое вычисление корня

\[ d = \frac{-1 + \sqrt{D}}{2(2\alpha-1)} \]

теряет значащие цифры вблизи \(\alpha=1/2\) и делит на ноль в случае стандартного дополнения. Рационализация даёт реализованную непрерывную форму

\[ y = x + \frac{4(\alpha-x)}{1+\sqrt{D}}. \]

Два выражения дискриминанта в коде алгебраически эквивалентны и выбираются по разные стороны от \(\alpha=1/2\). Их слагаемые неотрицательны на допустимой области. Точные возвраты в концах защищают граничный контракт от устранимого округления.

Логистическая принадлежность

Для \(z=a(x-b)\) прямое выражение \(1/(1+e^{-z})\) переполняется, если \(z\) — большое по модулю отрицательное конечное значение. Поэтому реализация использует

\[ \sigma(z) = \begin{cases} 1/(1+e^{-z}), & z \ge 0, \\ e^z/(1+e^z), & z < 0. \end{cases} \]

Оба показателя неположительны, поэтому math.exp не переполняется. Binary64 всё же может округлить математический результат из открытого интервала точно к 0.0 или 1.0; это насыщение представления, а не обрезание.

Если вычитание конечных координат противоположных знаков переполняется, реализация вычисляет \(ax-ab\), не умножая уже бесконечное \(x-b\). Например, при slope=1e-308, midpoint=-1e308 и coordinate=1e308 показатель близок к \(2\), а принадлежность — примерно \(0.880797\), а не вызванная переполнением \(1\). В этой ветви распределённые произведения не могут привести к вычитанию бесконечностей, поскольку исходные координаты имеют противоположные знаки. Обычное конечное вычитание сохраняет прежнюю арифметику.

Линейные склоны и гауссовы расстояния

Склоны треугольника и трапеции делят одну разность координат на другую. Если любое вычитание конечных координат переполняется, деление всех четырёх операндов пополам перед вычитанием сохраняет отношение и конечность разностей binary64. Поэтому Triangle(-1e308, 1e308, 1e308) сохраняет принадлежность \(1/2\) в нуле и \(1\) в включённой правой вершине. Для обычных конечных разностей используются установленные операции; запасная ветвь не обрезает степени принадлежности.

Гауссова принадлежность вычисляет \(e^{-(x-c)^2/(2s^2)}\) через безразмерное расстояние \((x-c)/s\). Если исходная разность переполняется, распределённое деление \(x/s-c/s\) позволяет не потерять конечное масштабированное расстояние. При центре \(-10^{308}\), масштабе \(10^{308}\) и координате \(10^{308}\) расстояние равно \(2\), а принадлежность — \(e^{-2}\), примерно \(0.135335\). Действительно непредставимое масштабированное расстояние по-прежнему даёт представимый нулевой хвост. Эти защиты используют те же скалярные ядра, что и исторические адаптеры.

Идентичность аналитического вычислителя

Точные области, высота, нормализация и моменты центроида описывают действующий скалярный вычислитель, а не только сохранённое имя семейства. Неизменённый унаследованный вычислитель MembershipFunction сохраняет встроенные аналитические основания. Переопределение __call__ или вызываемого им Evaluate делает вычислитель произвольным: центроид использует адаптивную квадратуру, а точная непрерывная высота недоступна. Отдельно переданный канонический связанный метод Evaluate сохраняет собственные проверенные основания, даже если __call__ его владельца переопределён. Исторические адаптеры также требуют, чтобы зарегистрированный связанный вычислитель был каноническим методом семейства; пользовательский метод подкласса не наследует аналитическое подтверждение.

Желательность Харрингтона

Формула \(d(y)=e^{-e^{-y}}\) имеет математический диапазон \((0,1)\). При очень отрицательном конечном \(y\) вычисление внутренней экспоненты сначала вызвало бы переполнение, хотя итоговый представимый результат уже равен 0.0. Защитная ветвь сравнивает \(y\) с логарифмом наибольшего конечного значения binary64 в Python и возвращает этот детерминированный предел потери представимости. При большом положительном конечном \(y\) обычное округление может дать 1.0.

Историческое переполнение промежуточных результатов

Конечные параметры и конечный ввод не гарантируют конечности каждого промежуточного результата binary64. Сохранённые выражения Hyperbolic, Bell и Parabolic вычисляются напрямую, без масштабирования крайних степеней или квадратов. Поэтому при достаточно больших величинах возможен OverflowError, хотя параметры и ввод прошли проверку конечности. Это документированное текущее численное ограничение, а не утверждение, что любой конечный ввод binary64 даёт степень принадлежности. Устойчивые логистические ветви и защита Харрингтона выше решают собственные известные пути экспоненциального переполнения, не распространяя гарантию на остальные исторические семейства.

Равномерные сетки

Для замкнутого интервала \([l,r]\) и \(n\ge2\) выборочные операции используют

\[ h=\frac{r-l}{n-1}, \qquad x_i=l+ih. \]

Последняя координата присваивается из r, а не вычисляется заново. Это делает инвариант конечной точки замкнутой области точным, даже если повторная арифметика binary64 дала бы соседнее значение. Построение и вычисление требуют \(O(n)\) времени и \(O(n)\) памяти для сохраняемых сведений о выборке.

Свидетельства удалённого исторического центроида

При accuracy = n историческая дефаззификация вычисляет правые концы \(x_i=l+i(r-l)/n\), \(i=1,\ldots,n\) и возвращает

\[ \frac{\sum_i x_i\mu(x_i)}{\sum_i\mu(x_i)}. \]

Общая ширина прямоугольников сокращается в частном. Требуются \(O(n)\) времени и \(O(1)\) дополнительной памяти, но это не адаптивная квадратура и не утверждение о сходимости. Тесты независимо сохраняют алгоритм как свидетельство задачи #78; он больше не используется в рабочей реализации.

Текущий центроид

Текущая стратегия вычисляет аналитические площадь и первый момент для поддерживаемых кусочно-полиномиальных и устойчивых гауссовых путей. Другие непрерывные вычислители используют адаптивную квадратуру Симпсона с неизменяемыми допусками отдельной операции и конечным пределом рекурсии. Нулевая площадь вызывает ValueError, а исчерпание адаптивного объёма работы — CentroidConvergenceError; ни одно условие не возвращает кэшированный результат, оценку на фиксированной сетке или лучшую промежуточную оценку. Полный контракт и карта свидетельств находятся в главе «Центроидная дефаззификация».

Конечные отношения

Равенство и включение используют каждую объявленную координату сравнения не более одного раза и останавливаются на первом контрпримере. В худшем случае требуются \(O(n)\) времени и \(O(1)\) дополнительной памяти. Равенство с допуском следует документированному критерию Python

\[ |a-b| \le \max(r\max(|a|,|b|), A), \]

где \(r\) и \(A\) — явные относительный и абсолютный допуски. Включение сначала принимает точный порядок и использует близость только для пары с небольшим нарушением; оно никогда не расширяет каждую степень принадлежности неявным epsilon.

Иерархия источников

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