Теорема Бекича

В вычислимости теории теорема Бекича или лемма Бекича — это теорема о неподвижных точках , которая позволяет разбить взаимную рекурсию на рекурсии по одной переменной за раз. ^{[ 1 ]}^{[ 2 ]}^{[ 3 ]} Его создал австрийец Ганс Бекич (1936-1982) в 1969 году. ^{[ 4 ]} и опубликовано посмертно в книге Клиффа Джонса в 1984 году. ^{[ 5 ]}

Теорема формулируется следующим образом. ^{[ 1 ]}^{[ 4 ]} Рассмотрим два оператора $f:P\times Q\to P$ и $g:P\times Q\to Q$ по указанным направленно-полным частичным заказам $P$ и $Q$ , непрерывный в каждой компоненте. Затем определите оператор $(f,g)(x,y)=(f(x,y),g(x,y))$ . Это монотонно относительно порядка произведения (покомпонентного порядка). По теореме Клини о неподвижной точке он имеет наименьшую неподвижную точку. $\mu (x,y).(f,g)(x,y)$ , пара $(x_{0},y_{0})$ в $P\times Q$ такой, что $f(x_{0},y_{0})=x_{0}$ и $g(x_{0},y_{0})=y_{0}$ .

Теорема Бекича (в его заметках называемая «леммой о делении пополам») ^{[ 4 ]} заключается в том, что одновременная наименьшая фиксированная точка $\mu (x,y).(f,g)(x,y)=(x_{0},y_{0})$ можно разделить на ряд наименее неподвижных точек на $P$ и $Q$ , в частности:

${\begin{aligned}x_{0}&=\mu x.f(x,\mu y.g(x,y))\\y_{0}&=\mu y.g(x_{0},y)\end{aligned}}$

В этой презентации $y_{0}$ определяется с точки зрения $x_{0}$ . Вместо этого его можно определить в симметричном представлении: ^{[ 1 ]}^{[ 6 ]}^{[ 7 ]}

${\begin{aligned}x_{0}&=\mu x.f(x,\mu y.g(x,y))\\y_{0}&=\mu y.g(\mu x.f(x,y),y)\end{aligned}}$

Доказательство (Бекич):

y_{0}=g(x_{0},y_{0})

так как это фиксированная точка. Сходным образом

x_{0}=f(x_{0},\mu y.g(x_{0},y))=f(x_{0},y_{0})

. Следовательно

(x_{0},y_{0})

является фиксированной точкой

(f,g)

. И наоборот, если существует заранее фиксированная точка

(x_{1},y_{1})

с

(x_{1},y_{1})\geq (f(x_{1},y_{1}),g(x_{1},y_{1}))

, затем

x_{1}\geq f(x_{1},\mu y.g(x_{1},y))\geq x_{0}

и

y_{1}\geq \mu y.g(x_{1},y)\geq \mu y.g(x_{0},y)=y_{0}

; следовательно

(x_{1},y_{1})\geq (x_{0},y_{0})

и

(x_{0},y_{0})

– минимальная фиксированная точка.

Варианты

В полной решетке

Вариант теоремы усиливает условия на $P$ и $Q$ быть в том, что они являются полными решетками , и находит наименьшую неподвижную точку, используя теорему Кнастера-Тарского . Требование непрерывности $f$ и $g$ затем можно ослабить, требуя, чтобы они были монотонными функциями . ^{[ 1 ]}^{[ 3 ]}

Категориальная формулировка

Лемма Бекича была обобщена на неподвижные точки эндофункторов категорий (начальные $F$ -алгебры ). ^{[ 8 ]}

Учитывая два функтора $F:\mathbf {C} \times \mathbf {D} \to \mathbf {C}$ и $G:\mathbf {C} \times \mathbf {D} \to \mathbf {D}$ такой, что все $\mu X.F(X,Y)$ и $\mu Y.G(X,Y)$ существует, фиксированная точка $\mu \langle X,Y\rangle .\langle F(X,Y),G(X,Y)\rangle$ переносится парой:

${\begin{aligned}X_{0}&=\mu X.F(X,\mu Y.G(X,Y))\\Y_{0}&=\mu Y.G(X_{0},Y)\end{aligned}}$

Использование

Теорему Бекича можно применять неоднократно, чтобы найти наименьшую неподвижную точку кортежа с точки зрения наименьших неподвижных точек одиночных переменных. будет проще рассуждать о фиксированных точках отдельных переменных Хотя полученное выражение может оказаться довольно сложным, при разработке автоматизированного средства доказательства теорем . ^{[ 9 ]}

Ссылки

^ Jump up to: ^а ^б ^с ^д Винскель, Глинн (5 февраля 1993 г.). Формальная семантика языков программирования: введение . МТИ Пресс. п. 163. ИСБН 978-0-262-73103-4 .
^ Диас-Каро, Алехандро; Мартинес Лопес, Пабло Э. (2015). «Изоморфизмы, рассматриваемые как равенства: проецирование функций и улучшение частичного применения посредством реализации λ +». Материалы 27-го симпозиума по реализации и применению языков функционального программирования — IFL '15 : 8. arXiv : 1511.09324 . дои : 10.1145/2897336.2897346 . S2CID 10413161 .
^ Jump up to: ^а ^б Харпер, Роберт (весна 2020 г.). «Теорема Тарского о неподвижной точке для степенных множеств» (PDF) . 15-819 Заметки по теории вычислительных типов . Проверено 7 марта 2022 г.
^ Jump up to: ^а ^б ^с Бекич, Ганс (1984). «Определимые операции в общих алгебрах, теории автоматов и блок-схем». Языки программирования и их определение . Конспекты лекций по информатике. Том. 177. С. 30–55. дои : 10.1007/BFb0048939 . ISBN 3-540-13378-Х .
^ Джонс, Клифф Б. (1984). «Фронт вопроса» (PDF) . В Джонсе, CB (ред.). Языки программирования и их определение . Конспекты лекций по информатике. Том. 177. дои : 10.1007/BFb0048933 . ISBN 3-540-13378-Х . S2CID 7488558 .
^ Лейсс, Ганс (2016). «Матричное кольцо мю-непрерывной алгебры Хомского является мю-непрерывным» (PDF) . 25-я ежегодная конференция EACSL по логике компьютерных наук (CSL 2016) . Международные труды Лейбница по информатике (LIPIcs). 62 : 6:1–6:15. дои : 10.4230/LIPIcs.CSL.2016.6 . ISBN 9783959770224 .
^ Арнольд, А.; Нивински, Д. (7 февраля 2001 г.). Основы исчисления . Эльзевир. п. 27. ISBN 978-0-08-051645-5 .
^ Леманн, Дэниел Дж.; Смит, Майкл Б. (1 декабря 1981 г.). «Алгебраическая спецификация типов данных: синтетический подход» . Теория математических систем . 14 (1): 97–139. дои : 10.1007/BF01752392 . ISSN 1433-0490 . S2CID 23076697 . Теорема 4.2.
^ Андерсен, Хенрик Рейф; Винскель, Глинн (1992). «Композиционная проверка удовлетворенности». Компьютерная проверка . Конспекты лекций по информатике. Том. 575. стр. 24–36. дои : 10.1007/3-540-55179-4_4 . ISBN 978-3-540-55179-9 .

[Winskel-1] Jump up to: ^а ^б ^с ^д Винскель, Глинн (5 февраля 1993 г.). Формальная семантика языков программирования: введение . МТИ Пресс. п. 163. ИСБН 978-0-262-73103-4 .

[2] Диас-Каро, Алехандро; Мартинес Лопес, Пабло Э. (2015). «Изоморфизмы, рассматриваемые как равенства: проецирование функций и улучшение частичного применения посредством реализации λ +». Материалы 27-го симпозиума по реализации и применению языков функционального программирования — IFL '15 : 8. arXiv : 1511.09324 . дои : 10.1145/2897336.2897346 . S2CID 10413161 .

[harper-3] Jump up to: ^а ^б Харпер, Роберт (весна 2020 г.). «Теорема Тарского о неподвижной точке для степенных множеств» (PDF) . 15-819 Заметки по теории вычислительных типов . Проверено 7 марта 2022 г.

[Bekic-4] Jump up to: ^а ^б ^с Бекич, Ганс (1984). «Определимые операции в общих алгебрах, теории автоматов и блок-схем». Языки программирования и их определение . Конспекты лекций по информатике. Том. 177. С. 30–55. дои : 10.1007/BFb0048939 . ISBN 3-540-13378-Х .

[5] Джонс, Клифф Б. (1984). «Фронт вопроса» (PDF) . В Джонсе, CB (ред.). Языки программирования и их определение . Конспекты лекций по информатике. Том. 177. дои : 10.1007/BFb0048933 . ISBN 3-540-13378-Х . S2CID 7488558 .

[6] Лейсс, Ганс (2016). «Матричное кольцо мю-непрерывной алгебры Хомского является мю-непрерывным» (PDF) . 25-я ежегодная конференция EACSL по логике компьютерных наук (CSL 2016) . Международные труды Лейбница по информатике (LIPIcs). 62 : 6:1–6:15. дои : 10.4230/LIPIcs.CSL.2016.6 . ISBN 9783959770224 .

[7] Арнольд, А.; Нивински, Д. (7 февраля 2001 г.). Основы исчисления . Эльзевир. п. 27. ISBN 978-0-08-051645-5 .

[8] Леманн, Дэниел Дж.; Смит, Майкл Б. (1 декабря 1981 г.). «Алгебраическая спецификация типов данных: синтетический подход» . Теория математических систем . 14 (1): 97–139. дои : 10.1007/BF01752392 . ISSN 1433-0490 . S2CID 23076697 . Теорема 4.2.

[9] Андерсен, Хенрик Рейф; Винскель, Глинн (1992). «Композиционная проверка удовлетворенности». Компьютерная проверка . Конспекты лекций по информатике. Том. 575. стр. 24–36. дои : 10.1007/3-540-55179-4_4 . ISBN 978-3-540-55179-9 .

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]