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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Источник

Поделитесь с другими:

Если материал понравился Вам и оказался для Вас полезным, поделитесь им со своими друзьями!

Читать по теме:

Интересные статьи: