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

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

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

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

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


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

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


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


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


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


[math]\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}[/math]

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


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


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


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


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


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


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


[math](\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}[/math]

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


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


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

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


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


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

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


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


[math]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).[/math]

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


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


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


[math][\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)!.[/math]

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


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


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


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


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


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

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