¿Teoremas de punto fijo para espacios métricos constructivos?

15

El teorema del punto fijo de Banach dice que si tenemos un espacio métrico completo no vacío , entonces cualquier función uniformemente contractiva tiene un punto fijo único . Sin embargo, la prueba de este teorema requiere el axioma de elección: debemos elegir un elemento arbitrario para comenzar a iterar desde, para obtener la secuencia de Cauchy . f : A A μ ( f ) a A f a , f ( a ) , f 2 ( a ) , f 3 ( a ) , Af:AAμ(f)aAfa,f(a),f2(a),f3(a),

  1. ¿Cómo se establecen los teoremas de punto fijo en el análisis constructivo?
  2. Además, ¿hay referencias concisas a espacios métricos constructivos?

La razón por la que pregunto es que quiero construir un modelo del Sistema F en el que los tipos también tengan una estructura métrica (entre otras cosas). Es bastante útil que, en la teoría de conjuntos constructivos, podamos preparar una familia de conjuntos , de modo que esté cerrada bajo productos, exponenciales y familias indexadas en , lo que facilita dar un modelo del Sistema F.U UUUU

Sería muy bueno si pudiera cocinar una familia similar de espacios ultramétricos constructivos. Pero dado que agregar opciones a la teoría de conjuntos constructiva lo hace clásico, obviamente necesito tener más cuidado con los teoremas de punto fijo, y probablemente también con otras cosas.

Neel Krishnaswami
fuente
2
Puede cambiar la hipótesis a siendo un conjunto habitado . No está invocando el axioma de la opción de escoger . AaA
Colin McQuillan

Respuestas:

22

El axioma de elección se usa cuando hay una colección de "cosas" y usted elige un elemento para cada "cosa". Si solo hay una cosa en la colección, ese no es el axioma de elección. En nuestro caso, solo tenemos un espacio métrico y estamos "eligiendo" un punto en él. Entonces ese no es el axioma de elección sino la eliminación de cuantificadores existenciales, es decir, tenemos una hipótesis y decimos "deja que sea ​​tal que ". Desafortunadamente, la gente a menudo dice " elija tal que ", que luego parece la aplicación del axioma de elección.x A ϕ ( x ) x A ϕ ( x )xA.ϕ(x)xAϕ(x) xAϕ(x)

Como referencia, aquí hay una prueba constructiva del teorema del punto fijo de Banach.

Teorema: una contracción en un espacio métrico completo habitado tiene un punto fijo único.

Prueba. Supongamos que es un espacio métrico completo habitado yf : M M es una contracción. Debido a que f es una contracción existe α tal que 0 < α < 1 y d ( f ( x ) , f ( y ) ) α d ( x , y ) para todo x , y M(M,d)f:MMfα0<α<1d(f(x),f(y))αd(x,y)x,yM.

Supongamos que y v son un punto fijo de f . Entonces tenemos d ( u , v ) = d ( f ( u ) , f ( v ) ) α d ( u , v ) de donde se deduce que 0 d ( u , v ) ( α - 1 ) d ( u , v ) uvf

d(u,v)=d(f(u),f(v))αd(u,v)
, por lo tanto delta ( u , v ) = 0 y u = v . Esto prueba que f tiene como máximo un punto fijo.0d(u,v)(α1)d(u,v)0d(u,v)=0u=vf

Queda por demostrar la existencia de un punto fijo. Debido a que está habitado existe x 0M . Defina la secuencia ( x i ) recursivamente por x i + 1 = f ( x i ) . Podemos demostrar por inducción que d ( x i , x i + 1 ) α id ( x 0 , x 1 ) . De esto se deduce queMx0M(xi)

xi+1=f(xi).
d(xi,xi+1)αid(x0,x1) es una secuencia de Cauchy. Debido a que M está completa, la secuencia tiene un límite y = lim i x i . Como f es una contracción, es uniformemente continua y, por lo tanto, conmuta con los límites de las secuencias: f ( y ) = f ( lim i x i ) = lim i f ( x i ) = lim i x i + 1 = lim i x yo(xi)My=limixif Por lo tanto, y es un punto fijo de f . QED
f(y)=f(limixi)=limif(xi)=limixi+1=limixi=y.
yf

Observaciones:

  1. Tuve cuidado de no decir "elegir " y "elegir x 0 ". Es común decir tales cosas, y solo se suman a la confusión que impide que los matemáticos comunes puedan decir qué es y qué no es el axioma de elección.αx0

  2. uvf¬¬(u=v)u=v

  3. (xi)x0xM.x0M

  4. MxM.M¬xM.

  5. fixMMM

  6. Finalmente, los siguientes teoremas de punto fijo tienen versiones constructivas:

    • Teorema de punto fijo de Knaster-Tarski para mapas monótonos en redes completas
    • Teorema de punto fijo de Banach para contracciones en un espacio métrico completo
    • Teorema de punto fijo de Knaster-Tarski para mapas monótonos en dcpos (probado por Pataraia)
    • Varios teoremas de punto fijo en la teoría de dominios generalmente tienen pruebas constructivas
    • El teorema de recursión es una forma de teorema de punto fijo y tiene una prueba constructiva
    • Probé que el teorema de punto fijo de Knaster-Tarski para mapas monótonos en posets de cadena completa no tiene una prueba constructiva. Del mismo modo, el teorema de punto fijo Bourbaki-Witt para mapas progresivos en posets de cadena completa falla constructivamente. El contraejemplo para el último proviene de los topos efectivos: en los topos efectivos, los ordinales (adecuadamente definidos) forman un conjunto y los mapas sucesores son progresivos y no tienen puntos fijos. Por cierto, el mapa sucesor en los ordinales no es monótono en los topos efectivos.

Ahora que es más información de la que pediste.

Andrej Bauer
fuente
1
¿Es necesario reformular alguno de los axiomas de los espacios métricos?
Neel Krishnaswami
esta es otra buena respuesta, Andrej!
Suresh Venkat
1
@Neel: No, los axiomas son los mismos que en el caso clásico.
Andrej Bauer
2
fixfixfix
2
fixfix=λM.λf.f(fixM(f))MfMM