El teorema de Bekić

Teorema sobre puntos fijos de múltiples variables.

En teoría de la computabilidad , el teorema de Bekić o el lema de Bekić es un teorema sobre puntos fijos que permite dividir una recursión mutua en recursiones en una variable a la vez. ^{[1] [2] [3]} Fue creado por el austriaco Hans Bekić (1936-1982) en 1969, ^[4] y publicado póstumamente en un libro de Cliff Jones en 1984. ^[5]

El teorema se plantea de la siguiente manera. ^{[1] [4]} Considere dos operadores y en órdenes parciales dirigidas-completas apuntadas y continuas en cada componente. Luego defina el operador . Esto es monótono con respecto al orden del producto (orden por componentes). Según el teorema del punto fijo de Kleene , tiene un punto mínimo fijo , un par tal que y . ${\displaystyle f:P\times Q\to P}$ ${\displaystyle g:P\times Q\to Q}$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle (f,g)(x,y)=(f(x,y),g(x,y))}$ ${\displaystyle \mu (x,y).(f,g)(x,y)}$ ${\displaystyle (x_{0},y_{0})}$ ${\displaystyle P\times Q}$ ${\displaystyle f(x_{0},y_{0})=x_{0}}$ ${\displaystyle g(x_{0},y_{0})=y_{0}}$

El teorema de Bekić (llamado "lema de bisección" en sus notas) ^[4] es que el punto menos fijo simultáneo se puede separar en una serie de puntos menos fijos en y , en particular: ${\displaystyle \mu (x,y).(f,g)(x,y)=(x_{0},y_{0})}$ ${\displaystyle P}$ ${\displaystyle Q}$

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

En esta presentación se define en términos de . En cambio, se puede definir en una presentación simétrica: ^{[1] [6] [7]} ${\displaystyle y_{0}}$ ${\displaystyle x_{0}}$

$${\displaystyle {\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}}}$$

Prueba (Bekić):

${\displaystyle y_{0}=g(x_{0},y_{0})}$ya que es el punto fijo. Similarmente . Por tanto es un punto fijo de . Por el contrario, si hay un punto prefijado con , entonces y ; por tanto y es el punto fijo mínimo. ${\displaystyle x_{0}=f(x_{0},\mu y.g(x_{0},y))=f(x_{0},y_{0})}$ ${\displaystyle (x_{0},y_{0})}$ ${\displaystyle (f,g)}$ ${\displaystyle (x_{1},y_{1})}$ ${\displaystyle (x_{1},y_{1})\geq (f(x_{1},y_{1}),g(x_{1},y_{1}))}$ ${\displaystyle x_{1}\geq f(x_{1},\mu y.g(x_{1},y)\geq x_{0}}$ ${\displaystyle y_{1}\geq \mu y.g(x_{1},y)\geq \mu y.g(x_{0},y)=y_{0}}$ ${\displaystyle (x_{1},y_{1})\geq (x_{0},y_{0})}$ ${\displaystyle (x_{0},y_{0})}$

Variantes

En una celosía completa

Una variante del teorema refuerza las condiciones de y para que sean redes completas y encuentra el punto menos fijo utilizando el teorema de Knaster-Tarski . El requisito de continuidad de y puede entonces debilitarse para exigir únicamente que sean funciones monótonas . ^{[1] [3]} ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle f}$ ${\displaystyle g}$

formulación categórica

El lema de Bekić se ha generalizado a puntos fijos de endofunctores de categorías ( álgebras iniciales ). ^[8] ${\displaystyle F}$

Dados dos funtores y tales que all y existen, el punto fijo lo lleva el par: ${\displaystyle F:\mathbf {C} \times \mathbf {D} \to \mathbf {C} }$ ${\displaystyle G:\mathbf {C} \times \mathbf {D} \to \mathbf {D} }$ ${\displaystyle \mu X.F(X,Y)}$ ${\displaystyle \mu Y.G(X,Y)}$ ${\displaystyle \mu \langle X,Y\rangle .\langle F(X,Y),G(X,Y)\rangle }$

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

Uso

El teorema de Bekić se puede aplicar repetidamente para encontrar el punto menos fijo de una tupla en términos de puntos menos fijos de variables individuales. Aunque la expresión resultante puede volverse bastante compleja, puede resultar más fácil razonar sobre puntos fijos de variables individuales al diseñar un demostrador de teoremas automatizado . ^[9]

Referencias

1. Winskel, Glynn (5 de febrero de 1993). La semántica formal de los lenguajes de programación: una introducción. Prensa del MIT. pag. 163.ISBN​ 978-0-262-73103-4.
2. Díaz-Caro, Alejandro; Martínez López, Pablo E. (2015). "Isomorfismos considerados como igualdades: Proyectar funciones y potenciar la aplicación parcial mediante una implementación de λ +". Actas del 27º Simposio sobre implementación y aplicación de lenguajes de programación funcionales - IFL '15 : 8. arXiv : 1511.09324 . doi :10.1145/2897336.2897346. S2CID  10413161.
3. Harper, Robert (primavera de 2020). "Teorema del punto fijo de Tarski para conjuntos de potencias" (PDF) . 15-819 Notas sobre la teoría de tipos computacionales . Consultado el 7 de marzo de 2022 .
4. Bekić, Hans (1984). "Operaciones definibles en álgebras generales y teoría de autómatas y diagramas de flujo". Lenguajes de programación y su definición . Apuntes de conferencias sobre informática. vol. 177, págs. 30–55. doi :10.1007/BFb0048939. ISBN 3-540-13378-X.
5. Jones, acantilado B. (1984). "Asunto preliminar" (PDF) . En Jones, CB (ed.). Lenguajes de programación y su definición . Apuntes de conferencias sobre informática. vol. 177.doi : 10.1007 /BFb0048933. ISBN 3-540-13378-X. S2CID  7488558.
6. Leiss, Hans (2016). "El anillo matricial de un álgebra de Chomsky mu-continua es mu-continua" (PDF) . 25ª Conferencia Anual de la EACSL sobre Lógica Informática (CSL 2016) . Procedimientos internacionales de informática de Leibniz (LIPIcs). 62 : 6:1–6:15. doi : 10.4230/LIPIcs.CSL.2016.6 . ISBN 9783959770224.
7. Arnold, A.; Niwinski, D. (7 de febrero de 2001). Rudimentos de cálculo. Elsevier. pag. 27.ISBN​ 978-0-08-051645-5.
8. Lehmann, Daniel J.; Smyth, Michael B. (1 de diciembre de 1981). "Especificación algebraica de tipos de datos: un enfoque sintético". Teoría de Sistemas Matemáticos . 14 (1): 97-139. doi :10.1007/BF01752392. ISSN  1433-0490. S2CID  23076697.Teorema 4.2.
9. Andersen, Henrik Reif; Winskel, Glynn (1992). "Comprobación composicional de la satisfacción". Verificación asistida por computadora . Apuntes de conferencias sobre informática. vol. 575, págs. 24-36. doi : 10.1007/3-540-55179-4_4 . ISBN 978-3-540-55179-9.