Topología computable

La topología computable es una disciplina de las matemáticas que estudia la estructura topológica y algebraica de la computación . La topología computable no debe confundirse con la topología algorítmica o computacional , que estudia la aplicación de la computación a la topología.

Topología del cálculo lambda

Como lo demostraron Alan Turing y Alonzo Church , el cálculo lambda es lo suficientemente fuerte como para describir todas las funciones computables mecánicamente (ver la tesis de Church-Turing ). ^{[1] [2] [3]} El cálculo lambda es, por lo tanto, efectivamente un lenguaje de programación, a partir del cual se pueden construir otros lenguajes. Por esta razón, cuando se considera la topología de la computación, es común centrarse en la topología del cálculo lambda. Nótese que esta no es necesariamente una descripción completa de la topología de la computación, ya que las funciones que son equivalentes en el sentido de Church-Turing aún pueden tener topologías diferentes.

La topología del cálculo lambda es la topología de Scott y, cuando se restringe a funciones continuas, el cálculo lambda libre de tipos equivale a un espacio topológico que depende de la topología de árbol . Tanto la topología de Scott como la de árbol muestran continuidad con respecto a los operadores binarios de aplicación (f aplicada a a = fa) y abstracción ((λx.t(x))a = t(a)) con una relación de equivalencia modular basada en una congruencia . Se ha descubierto que el álgebra lambda que describe la estructura algebraica del cálculo lambda es una extensión del álgebra combinatoria , con un elemento introducido para dar cabida a la abstracción.

El cálculo λ libre de tipos trata las funciones como reglas y no diferencia las funciones y los objetos a los que se aplican, lo que significa que el cálculo λ es libre de tipos . Un subproducto del cálculo λ libre de tipos es una computabilidad efectiva equivalente a la recursión general y las máquinas de Turing . ^[4] El conjunto de términos λ puede considerarse una topología funcional en la que se puede incrustar un espacio de funciones , lo que significa que las aplicaciones λ dentro del espacio X son tales que λ:X → X. ^{[4] [5]} Introducido en noviembre de 1969, el modelo teórico de conjuntos no tipados de Dana Scott construyó una topología adecuada para cualquier modelo de cálculo λ cuyo espacio de funciones esté limitado a funciones continuas. ^{[4] [5]} El resultado de una topología de cálculo λ continuo de Scott es un espacio de funciones construido sobre una semántica de programación que permite combinatorias de punto fijo, como el combinador Y , y tipos de datos. ^{[6] [7]} En 1971, el cálculo λ estaba equipado para definir cualquier cálculo secuencial y podía adaptarse fácilmente a los cálculos paralelos. ^[8] La reducibilidad de todos los cálculos al cálculo λ permite que estas propiedades λ-topológicas sean adoptadas por todos los lenguajes de programación. ^[4]

Álgebra computacional a partir del álgebra de cálculo λ

Basándose en los operadores del cálculo lambda , la aplicación y la abstracción, es posible desarrollar un álgebra cuya estructura de grupo utiliza la aplicación y la abstracción como operadores binarios. La aplicación se define como una operación entre términos lambda que produce un término λ, p. ej., la aplicación de λ sobre el término lambda a produce el término lambda λa . La abstracción incorpora variables no definidas al denotar λx.t(x) como la función que asigna la variable a al término lambda con valor t(a) mediante la operación ((λ xt(x))a = t(a)). Por último, surge una relación de equivalencia que identifica los términos λ módulo términos convertibles, un ejemplo es la forma normal beta .

Topología de Scott

La topología de Scott es esencial para entender la estructura topológica de la computación expresada a través del cálculo λ. Scott encontró que después de construir un espacio de funciones usando el cálculo λ se obtiene un espacio de Kolmogorov , un espacio topológico que exhibe convergencia puntual , en resumen la topología del producto . ^[9] Es la capacidad del autohomeomorfismo así como la capacidad de incrustar cada espacio en tal espacio, denotado Scott continuo , como se describió previamente, lo que permite que la topología de Scott sea aplicable a la lógica y la teoría de funciones recursivas. Scott aborda su derivación usando una red completa , lo que resulta en una topología dependiente de la estructura de la red. Es posible generalizar la teoría de Scott con el uso de órdenes parciales completos . Por esta razón, se proporciona una comprensión más general de la topología computacional a través de órdenes parciales completos. Reiteraremos para familiarizarnos con la notación que se utilizará durante la discusión de la topología de Scott. ${\displaystyle T_{o}}$

Los pedidos parciales completos se definen de la siguiente manera:

Primero, dado el conjunto parcialmente ordenado D=(D,≤), un subconjunto no vacío X ⊆ D está dirigido si ∀ x,y ∈ X ∃ z ∈ X donde x ≤ z & y ≤ z .

D es una orden parcial completa (cpo) si:

⋅ Todo X ⊆D dirigido tiene un supremo , y:

∃ elemento inferior ⊥ ∈ D tal que ∀ x ∈ D ⊥ ≤ x .

Ahora podemos definir la topología de Scott sobre un cpo (D, ≤ ).

O ⊆ D está abierto si:

1. para x ∈ O, y x ≤ y, entonces y ∈ O, es decir, O es un conjunto superior .
2. para un conjunto dirigido X ⊆ D, y supremo (X) ∈ O, entonces X ∩ O ≠ ∅.

Utilizando la definición topológica de Scott de abierto, es evidente que se cumplen todas las propiedades topológicas.

⋅∅ y D, es decir, el conjunto vacío y todo el espacio, son abiertos.

⋅Las uniones arbitrarias de conjuntos abiertos son abiertas:

Demostración : Supongamos que es abierto donde i ∈ I, siendo I el conjunto índice. Definimos U = ∪{  ; i ∈ I}. Tomemos b como un elemento del conjunto superior de U, por lo tanto a ≤ b para algún a ∈ U Debe ser que a ∈ para algún i, asimismo b ∈ disturbio( ). Por lo tanto, U también debe ser superior ya que ∈ U. ${\displaystyle U_{i}}$ ${\displaystyle U_{i}}$ ${\displaystyle U_{i}}$ ${\displaystyle U_{i}}$ ${\displaystyle U_{i}}$

De la misma manera, si D es un conjunto dirigido con un supremo en U, entonces, por suposición, sup(D) ∈ donde es abierto. Por lo tanto, existe un b ∈ D donde b ∈ . Por lo tanto, la unión de conjuntos abiertos es abierta. ${\displaystyle U_{i}}$ ${\displaystyle U_{i}}$ ${\displaystyle U_{i}\cap D\subseteq U\cap D}$ ${\displaystyle U_{i}}$

⋅Los conjuntos abiertos bajo intersección son abiertos:

Demostración : Dados dos conjuntos abiertos, U y V , definimos W = U ∩ V . Si W = ∅ entonces W es abierto. Si no está vacío, digamos b ∈ trastornado(W) (el conjunto superior de W), entonces para algún a ∈ W , a ≤ b . Como a ∈ U ∩ V , y b es un elemento del conjunto superior de U y V , entonces b ∈ W .

Finalmente, si D es un conjunto dirigido con un supremo en W , entonces, por suposición sup( D ) ∈ . Por lo tanto, hay a ∈ y b ∈ . Como D es dirigido, hay c ∈ D con ; y como U y V son conjuntos superiores, c ∈ también. ${\displaystyle U\cap V}$ ${\displaystyle U\cap D}$ ${\displaystyle V\cap D}$ ${\displaystyle a\leq c,b\leq c}$ ${\displaystyle U\cap V}$

Aunque no se muestra aquí, es el caso que la función es continua si y sólo si f (sup( X )) = sup( f ( X )) para todo X ⊆ D dirigido , donde f ( X ) = { f ( x ) | x ∈ X } y el segundo supremo en . ^[4] ${\displaystyle f:D\rightarrow D^{'}}$ ${\displaystyle D^{'}}$

Antes de comenzar a explicar que la aplicación común al cálculo λ es continua dentro de la topología de Scott, requerimos una cierta comprensión del comportamiento de los supremos sobre funciones continuas, así como las condiciones necesarias para que el producto de espacios sea continuo, a saber:

1. Con ser una familia dirigida de mapas, entonces si bien definidos y continuos. ${\displaystyle {f_{i}}_{i}\subseteq [D\rightarrow D^{'}]}$ ${\displaystyle f(x)=\cup _{i}f_{i}(x)}$
2. Si F es dirigida y cpo y a cpo donde sup({ f ( x ) | f ∈ F }). ${\displaystyle \subseteq [D\rightarrow D^{'}]}$ ${\displaystyle [D\rightarrow D^{'}]}$

Ahora demostramos la continuidad de la aplicación . Utilizando la definición de aplicación de la siguiente manera:

Ap: donde Ap ( f , x ) = f ( x ). ${\displaystyle [D\rightarrow D^{'}]\times D\rightarrow D^{'}}$

Ap es continua con respecto a la topología de Scott en el producto ( ): ${\displaystyle [D\rightarrow D^{'}]\times D\rightarrow D^{'}}$

Demostración : λx.f(x) = f es continua. Sea h = λ ff(x). Para F dirigida ${\displaystyle \subseteq [D\rightarrow D^{'}]}$

h (sup( F )) = sup( F )( x )

= sup( { f ( x ) | f ∈ F } )

= sup( { h ( f ) | f ∈ F } )

= sup( h ( F ))

Por definición de continuidad de Scott, se ha demostrado que h es continua. Todo lo que queda por demostrar es que la aplicación es continua cuando sus argumentos separados son continuos, es decir, y son continuos, en nuestro caso f y h . ${\displaystyle [D\rightarrow D^{'}]}$ ${\displaystyle D\rightarrow D^{'}}$

Ahora, abstrayendo nuestro argumento para mostrar que con y como argumentos para D y respectivamente, entonces para una dirección X ⊆ D ${\displaystyle f:D\times D^{'}\rightarrow D^{''}}$ ${\displaystyle g=\lambda x.f(x,x_{0})}$ ${\displaystyle d=\lambda x^{'}.f(x_{0},x^{'})}$ ${\displaystyle D^{'}}$

${\displaystyle g(\sup(X))=f(\sup(X),x_{0}^{'}))}$

= f(sup((x, ) | x ∈ X} )) ${\displaystyle x_{0}^{'}}$

(dado que f es continua y {(x, ) | x ∈ X}) está dirigida): ${\displaystyle x_{0}^{'}}$

= sup( {f(x, ) | x ∈ X} ) ${\displaystyle x_{0}^{'}}$

= sop(g(X))

Por lo tanto, g es continua. Se puede realizar el mismo proceso para demostrar que d es continua.

Ahora se ha demostrado que la aplicación es continua bajo la topología de Scott.

Para demostrar que la topología de Scott es adecuada para el cálculo λ, es necesario probar que la abstracción permanece continua a lo largo de la topología de Scott. Una vez completado, se habrá demostrado que la base matemática del cálculo λ es un paradigma funcional candidato bien definido y adecuado para la topología de Scott.

Con definimos (x) = λ y ∈ f(x,y)Mostraremos: ${\displaystyle f\in [D\times D^{'}\rightarrow D^{''}]}$ ${\displaystyle {\check {f}}}$ ${\displaystyle D^{'}}$

(i) es continua, lo que significa ∈ ${\displaystyle {\check {f}}}$ ${\displaystyle {\check {f}}}$ ${\displaystyle [D\rightarrow [D^{'}\rightarrow D^{''}]}$

(ii) λ es continua. ${\displaystyle f.{\check {f}}:[D\times D^{'}\rightarrow D^{''}]\rightarrow [D\rightarrow [D^{'}\rightarrow D^{''}]}$

Prueba (i): Sea X ⊆ D dirigida, entonces

${\displaystyle {\check {f}}}$(sup(X)) = λ yf(sup(X),y)

= λ y. ( f(x,y) ) ${\displaystyle \sup _{x\in X}}$

= ( λy.f(x,y) ) ${\displaystyle \sup _{x\in X}}$

= soportar( (X)) ${\displaystyle {\check {f}}}$

Prueba (ii): Definiendo L = λ entonces para F dirigida ${\displaystyle f.{\check {f}}}$ ${\displaystyle \subseteq [D\times D^{'}\rightarrow D^{''}]}$

L(sup(F)) = λ x λ y. (sup(F))(x,y))

= λ x λ y. f(x,y) ${\displaystyle \sup _{y\in F}}$

= λx λy.f(x,y) ${\displaystyle \sup _{y\in F}}$

= sup(L(F))

No se ha demostrado cómo y por qué el cálculo λ define la topología de Scott.

Árboles de Böhm y topología computacional

Los árboles de Böhm , que se representan gráficamente con facilidad, expresan el comportamiento computacional de un término lambda . Es posible predecir la funcionalidad de una expresión lambda dada a partir de su árbol de Böhm correlacionado. ^[4] Los árboles de Böhm pueden verse de manera algo análoga a donde el árbol de Böhm de un conjunto dado es similar a la fracción continua de un número real, y lo que es más, el árbol de Böhm correspondiente a una secuencia en forma normal es finito, similar al subconjunto racional de los Reales. ${\displaystyle \mathbb {R} }$

Los árboles de Böhm se definen como una aplicación de elementos dentro de una secuencia de números con orden (≤, lh) y un operador binario * a un conjunto de símbolos. El árbol de Böhm es entonces una relación entre un conjunto de símbolos a través de una aplicación parcial ψ.

De manera informal, los árboles de Böhm pueden conceptualizarse de la siguiente manera:

Dado: Σ = { λ x_{1} x_{n} . y | n ∈ y son variables y denotando BT(M) como el árbol de Böhm para un término lambda M, entonces tenemos: ${\displaystyle \perp \cup }$ ${\displaystyle \cdots }$ ${\displaystyle \mathbb {N} ,x_{1}...x_{n}}$

BT(M) = ⊥ si M no tiene solución (por lo tanto, es un solo nodo)

     BT(M) = λ .y                   / \      BT(    BT( ) ; si M es solucionable ${\displaystyle {\vec {x}}}$

${\displaystyle M_{1})}$ ${\displaystyle M_{m}}$

Más formalmente:

Σ se define como un conjunto de símbolos. El árbol de Böhm de un término λ M, denotado BT(M), es el árbol etiquetado como Σ que se define de la siguiente manera:

Si M no tiene solución:

${\displaystyle BT(M)(\langle \ \rangle )=\perp ,}$

BT(M)( ) no tiene solución ${\displaystyle \langle k\rangle *\alpha }$ ${\displaystyle \forall k,\alpha }$

Si M es solucionable, donde M = λ x_{1} : ${\displaystyle \cdots x_{n}.yM_{0}\cdots M_{m-1}}$

BT(M)(< >) = λx_{1} ${\displaystyle \cdots x_{n}.y}$

BT(M)( ) = BT(M_k)( ) y k < m ${\displaystyle \langle k\rangle *\alpha }$ ${\displaystyle \alpha }$ ${\displaystyle \forall \alpha }$

= indefinido y k ≥ m ${\displaystyle \forall \alpha }$

Ahora podemos pasar a demostrar que los árboles de Böhm actúan como aplicaciones adecuadas de la topología de árbol a la topología de Scott, lo que permite ver las construcciones computacionales, ya sea dentro de la topología de Scott o de árbol, como formaciones de árboles de Böhm.

Árbol de Böhm y topología de árboles

Se ha descubierto que los árboles de Böhm permiten un mapeo continuo de la topología del árbol a la topología de Scott. Más específicamente:

Comenzamos con el cpo B = (B,⊆) en la topología de Scott, con el ordenamiento de los árboles de Böhm denotado M⊆ N, lo que significa que M, N son árboles y M resulta de N. La topología de árbol en el conjunto Ɣ es el conjunto más pequeño que permite una función continua.

Es: B . ${\displaystyle \Gamma \rightarrow }$

Una definición equivalente sería decir que los conjuntos abiertos de Ɣ son la imagen del árbol de Böhm inverso (O) donde O es abierto de Scott en B. ${\displaystyle BT^{-1}}$

La aplicabilidad de los árboles Bömh y la topología de árboles tiene muchas consecuencias interesantes para los términos λ expresados ​​topológicamente:

Se descubre que las formas normales existen como puntos aislados.

Los términos λ irresolubles son puntos de compactificación.

La aplicación y la abstracción, de forma similar a la topología de Scott, son continuas en la topología del árbol.

Estructura algebraica de la computación

Los nuevos métodos de interpretación del cálculo λ no sólo son interesantes en sí mismos, sino que permiten nuevos modos de pensamiento en relación con los comportamientos de la ciencia informática. El operador binario dentro del álgebra λ A es aplicación. La aplicación se denota ⋅ y se dice que da estructura . Un álgebra combinatoria permite el operador de aplicación y actúa como un punto de partida útil, pero sigue siendo insuficiente para el cálculo λ al no poder expresar abstracción. El álgebra λ se convierte en un álgebra combinatoria M combinada con un operador sintáctico λ* que transforma un término B(x,y) , con constantes en M , en C( )≡ λ* xB(x, ). También es posible definir un modelo de extensión para evitar la necesidad del operador λ* permitiendo ∀x (fx =gx) ⇒ f =g . La construcción del álgebra λ mediante la introducción de un operador de abstracción procede de la siguiente manera: ${\displaystyle A=(X,\cdot )}$ ${\displaystyle {\hat {y}}}$ ${\displaystyle {\hat {y}}}$

Debemos construir un álgebra que permita soluciones a ecuaciones como axy = xyy tales que a = λ xy.xyy, por lo que es necesario el álgebra combinatoria. Los atributos relevantes del álgebra combinatoria son:

Dentro del álgebra combinatoria existen estructuras aplicativas . Una estructura aplicativa W es un álgebra combinatoria siempre que:

⋅W no es trivial, lo que significa que W tiene cardinalidad > 1

⋅W exhibe completitud combinatoria (ver completitud de la base SK ). Más específicamente: para cada término A ∈ el conjunto de términos de W, y con las variables libres de A dentro entonces: ${\displaystyle x_{1},...,x_{n}}$ ${\displaystyle {x_{1},...,x_{n}}}$

${\displaystyle \exists f\forall x_{1}\cdot \cdot \cdot x_{n}}$dónde ${\displaystyle fx_{1}\cdot \cdot \cdot x_{n}=A}$

El álgebra combinatoria es:

• Nunca conmutativo
• No asociativo.
• Nunca finito.
• Nunca recursivo.

Las álgebras combinatorias siguen sin poder actuar como estructura algebraica para el cálculo λ, siendo la falta de recursión una desventaja importante. Sin embargo, la existencia de un término aplicativo ) proporciona un buen punto de partida para construir un álgebra de cálculo λ. Lo que se necesita es la introducción de un término lambda , es decir, incluir λx.A(x, ). ${\displaystyle A(x,{\vec {y}}}$ ${\displaystyle {\vec {y}}}$

Comenzamos explotando el hecho de que dentro de un álgebra combinatoria M, con A(x, ) dentro del conjunto de términos, entonces: ${\displaystyle {\vec {y}}}$

${\displaystyle \forall {\vec {y}}}$ ${\displaystyle \exists b}$est bx = A(x, ). ${\displaystyle {\vec {y}}}$

Luego requerimos que b tenga una dependencia que dé como resultado: ${\displaystyle {\vec {y}}}$

${\displaystyle \forall x}$B( )x = A(x, ). ${\displaystyle {\vec {y}}}$ ${\displaystyle {\vec {y}}}$

B( ) se vuelve equivalente a un término λ y, por lo tanto, se define adecuadamente de la siguiente manera: B( λ*. ${\displaystyle {\vec {y}}}$ ${\displaystyle {\vec {y}})\equiv }$

Ahora se puede definir una pre-λ-álgebra (pλA).

pλA es una estructura aplicativa W = (X,⋅) tal que para cada término A dentro del conjunto de términos dentro de W y para cada x hay un término λ*xA ∈ T(W) (T(W) ≡ los términos de W) donde (el conjunto de variables libres de λ*xA) = (el conjunto de variables libres de A) - {x}. W debe demostrar también:

${\displaystyle (\beta )}$(λ*xA)x = A

${\displaystyle \alpha _{1}}$λ*xA≡ λ*xA[x:=y] siempre que y no sea una variable libre de A

${\displaystyle \alpha _{2}}$(λ*xA)[y:=z]≡λ*xA[x:=y] siempre que y,z ≠ x y z no sea una variable libre de A

Antes de definir el λ-álgebra completa debemos introducir la siguiente definición para el conjunto de λ-términos dentro de W denotado con los siguientes requisitos: ${\displaystyle \Gamma (W)}$

a ∈ W ${\displaystyle \Rightarrow c_{a}\in \Gamma (W)}$

x ∈ para x ∈ ( ) ${\displaystyle \Gamma (W)}$ ${\displaystyle v_{0},v_{1},...}$

M,N ∈ (MN) ∈ ${\displaystyle \Gamma (W)\Rightarrow }$ ${\displaystyle \Gamma (W)}$

M ∈ (λx.M) ∈ ${\displaystyle \Gamma (W)\Rightarrow }$ ${\displaystyle \Gamma (W)}$

Luego, se puede diseñar un mapeo de los términos dentro de todos los términos λ dentro de W, denotado *  : , de la siguiente manera: ${\displaystyle \Gamma (W)}$ ${\displaystyle \Gamma (W)\rightarrow \mathrm {T} (W)}$

${\displaystyle v_{i}^{*}=w_{i},c_{a}^{*}=c_{a}}$

(MN)* = M*N*

(λx.M)* = λ* x*.M*

Ahora definimos λ (M) para denotar la extensión después de evaluar los términos dentro de . ${\displaystyle \Gamma (W)}$

λx.(λy.yx) = λx. x en λ (W). ${\displaystyle c_{a}}$ ${\displaystyle c_{a}}$

Finalmente obtenemos el λ-álgebra completa a través de la siguiente definición:

(1) Una λ-álgebra es una pλA W tal que para M,N ∈ Ɣ(W):

λ (W) ⊢ M = N ⇒ W ⊨ M = N.

Aunque arduo, se han sentado las bases para un marco algebraico adecuado para el cual el cálculo λ, y por lo tanto la computación, pueden investigarse de una manera teórica de grupos .

Referencias

1. Church 1934:90 nota al pie en Davis 1952
2. Turing 1936-7 en Davis 1952:149
3. Barendregt, HP, Sintaxis y semántica del cálculo lambda. North-Holland Publishing Company. 1981
4. Barendregt, HP, Sintaxis y semántica del cálculo lambda. North-Holland Publishing Company. 1981.
5. DS Scott. Modelos para el cálculo λ. Distribuidos informalmente, 1969. Notas, diciembre de 1969, Oxford Univ.
6. Gordon, MJC, La descripción denotacional de los lenguajes de programación. Springer Verlag, Berlín. 1979.
7. Scott, DS y Strachey, C. Hacia una semántica matemática para lenguajes informáticos, Proc. Symp. sobre computadoras y autómatas, Instituto Politécnico de Brooklyn, 21, págs. 19-46. 1971.
8. G. Berry, Algoritmos secuenciales en estructuras de datos concretas, Theoretical Computer Science 20, 265 321 (1982).
9. DS Scott. "Redes continuas". Laboratorio de Computación de la Universidad de Oxford, agosto de 1971.