Дискуссионный математический форумМатематический форум
Математический форум Math Help Planet

Обсуждение и решение задач по математике, физике, химии, экономике

Теоретический раздел
Часовой пояс: UTC + 3 часа [ Летнее время ]
MathHelpPlanet.com RSS-лента Математического форума

Часовой пояс: UTC + 3 часа [ Летнее время ]


Принцип индукции по неподвижной точке

Принцип индукции по неподвижной точке


Пусть \mathcal{P} есть некоторое утверждение о программах, \mathcal{F} — непрерывное отображение множества (\Sigma\to\Sigma) в себя, f — наименьшая неподвижная точка отображения \mathcal{F} или, что то же самое, наименьшее решение уравнения X=\mathcal{F}(X).


Тогда, если \mathcal{P}(f^{(0)}) истинно и для каждого i из истинности \mathcal{P}(f^{(i)}) следует истинность \mathcal{P}(f^{(i+1)}), то истинно \mathcal{P}(f). (Под f^{(i)} понимается i-е приближение наименьшей неподвижной точки: f^{(0)}=\bold{0},~ f^{(i)}=\mathcal{F}(f^{(i-1)}).)


Проиллюстрируем применение этого принципа на примере анализа простейшей программы на языке MILAN. Рассмотрим программу вычисления факториала:


\begin{aligned}&\text{begin}\\ &\quad x^=n;~ y^=0;~ z^=1;\\ &\quad \text{while}(y\ne x)~\text{do}\\ &\qquad y^=y+1;~ z^=z\ast y;\\ &\quad \text{end}\\ &\text{end} \end{aligned}

Здесь предполагается, что все переменные принимают целые значения. Букву n следует понимать не как переменную программы, а как условное обозначение произвольного натурального числа, "засылаемого" в "ячейку" x. Мы вынуждены прибегать к столь неэстетичному (с программистской точки зрения) вводу исходного значения, так как наш простенький язык не имеет средств ввода/вывода.


Докажем следующее утверждение \mathcal{P} об этой программе: если после выполнения программы состояние памяти а таково, что \sigma(x)\ne\mathbb{O} и \sigma(z)\ne\mathbb{O}, то \sigma(z)=\sigma(x)!.


Заметим, что мы не определяли в языке операторов ввода и вывода и, следовательно, начальное состояние памяти задается априори (некоторым "оракулом"), а вопрос, как это состояние сформировано, остается за пределами формализации. В нашем примере речь идет о задании начального значения переменной n.


Проанализируем теперь, что означает в данном случае индукция по неподвижной точке.


Ясно, что перед выполнением цикла состояние памяти \sigma_0 таково, что всегда \sigma_0(z)=\sigma_0(y)!. Нам нужно доказать, что если выполнение цикла заканчивается после конечного числа итераций, то в результирующем состоянии а будем иметь \sigma(z)=\sigma(x)!=\sigma(y)!.


Нам будет удобно определить операцию p-дизъюнкции преобразователей состояний памяти, где p(t_1,\ldots,t_n) — некоторое условие языка MILAN.


Определение 8.19. Назовем p-дизъюнкцией преобразователей состояний памяти f и g преобразователь, обозначаемый {}_p(f\lor g) и определяемый следующим образом:


(\forall\nu\in\Sigma){}_p(f\lor g)(\nu)= \begin{cases}\mathbb{O},&\text{if}\quad \text{znachenie~predikata}~p~\text{v~sostoyanii}~\nu~\text{ne~ opredeleno};\\ f(\nu), &\text{if}\quad p_{\nu}=1;\\ g(\nu), &\text{if}\quad p_{\nu}=0;\end{cases}

(через p_{\nu} обозначено значение условия, или предиката, p в состоянии \nu\colon\, p_{\nu}=p(t_1^{\nu},\ldots,t_{n}^{\nu})).


В соответствии с тем, как мы определили выше, Преобразователь состояний f, соответствующий циклу, есть наименьшая неподвижная точка уравнения f=F(f), где функция F может быть представлена в виде


F(g)(\nu)={}_{\lnot p}(ID\lor [\kern-0.15em[S]\kern-0.15em]\circ g)(\nu) (для условия p и тела S цикла \text{while}).

Согласно алгоритму вычисления наименьшей неподвижной точки, f=\sup\{f^{(i)}\colon i\geqslant0\}, где f^{(0)}=\bold{0} — стирающий преобразователь.


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


f^{(1)}={}_{\lnot p}(ID\lor [\kern-0.15em[S]\kern-0.15em]\circ \bold{0}), где S — тело цикла.

Очевидно, что для произвольного состояния \nu\ne\mathbb{O} неравенство f^{(1)}\ne\mathbb{O} имеет место тогда и только тогда, когда p_{\nu} определено и равно 0. Тогда f^{(1)}(\nu)=\nu.


Таким образом, первое приближение соответствует нулевому числу повторений тела цикла. Для второго приближения имеем


f^{(2)}={}_{\lnot p}\bigl(ID\lor [\kern-0.15em[S]\kern-0.15em]\circ_{\lnot p} (ID\lor [\kern-0.15em[S]\kern-0.15em]\circ \bold{0})\bigr).

Точно так же легко видеть, что f^{(2)}(\nu)\ne\mathbb{O} тогда и только тогда, когда p_{\nu} определено и равно 0 (f^{(2)}(\nu)=\nu) или когда p_{\nu}=1, но p_{[\kern-0.15em[S]\kern-0.15em](\nu)}=0 (f^{(2)}(\nu)= [\kern-0.15em[S]\kern-0.15em](\nu)). Таким образом, второе приближение соответствует не более чем однократному числу повторений тела цикла. Методом математической индукции несложно доказать, что i-е приближение наименьшей неподвижной точки для семантики цикла соответствует не более чем (i-1)-кратному повторению тела цикла, если f^{(i)}\ne \mathbb{O} для произвольного состояния \nu\ne\mathbb{O}.


Следовательно, индукция по неподвижной точке сводится в данном случае к индукции по числу повторений цикла, и нам для данного конкретного примера нужно доказать, что выполнение тела цикла сохраняет соотношение значений переменных y и z: для любого \nu, такого, что \nu(z)=\nu(y)!, имеем [\kern-0.15em[S]\kern-0.15em](\nu)(z) где S — тело цикла в программе вычисления факториала.


В самом деле (что и требовалось доказать),


[\kern-0.15em[S]\kern-0.15em](\nu)(z)= [\kern-0.15em[z^=z\ast y]\kern-0.15em] \bigl([\kern-0.15em[y^=y+1]\kern-0.15em](\nu)\bigr)(z)= \nu(y)!\ast (\nu(y)+1)= (\nu(y)+1)!= [\kern-0.15em[S]\kern-0.15em](\nu)(y)!.

Теперь остается заметить, что поскольку условие выхода из цикла имеет вид y\ne x, то, задав переменной n некоторой значение из множества натуральных чисел \mathbb{N}, после выполнения нашей программы достигнем требуемого результата.


Мы рассмотрели простейший случай денотационного определения для языка, не содержащего даже блоков и процедур. При появлении последних возникают локальные определения переменных и необходимо модифицировать понятие состояния памяти. Это может быть реализовано с помощью понятия среды, которая формально определяется как декартово произведение I\times Loc множества переменных на множество "адресов", а состояние памяти при этом понимается как отображение вида \sigma\colon I\times Loc\to D.


Денотационное определение, как уже упоминалось, не является единственным в рамках экстенсионального подхода. Кроме него наиболее употребительными являются операциональное и трансформационное определения. При операциональном определении в качестве экстенсионала программы рассматривается множество последовательностей состояний памяти, генерируемых при выполнении программы. Трансформационное определение сопоставляет программе преобразователь вида "состояние памяти → пара (программа, состояние памяти)". А именно если программа начинает работать над некоторым исходным состоянием памяти \sigma, то все операторы, которые могут быть выполнены, выполняются, а все операторы, которые не могут быть выполнены (из-за неопределенности значений переменных) "складываются" в новую программу (называемую остаточной): таким образом возникает пара (остаточная программа, частичный результат = новое состояние \sigma'). Подобное вычисление, называемое смешанным, позволяет определять различные преобразования (трансформации) программ.


Семантика языков программирования в настоящее время является бурно развивающейся областью теории формальных языков, используемой при разработке и реализации языков программирования и программных продуктов (в частности, при разработке надежного программного обеспечения).

Математический форум (помощь с решением задач, обсуждение вопросов по математике).
Кнопка "Поделиться"

Часовой пояс: UTC + 3 часа [ Летнее время ]


Яндекс.Метрика

Copyright © 2010-2019 MathHelpPlanet.com. All rights reserved