Teoremas de pontos fixos para espaços métricos construtivos?

15

O teorema do ponto fixo de Banach diz que, se tivermos um espaço métrico completo não vazio UMA , qualquer função uniformemente contrativa possui um ponto fixo único . No entanto, a prova desse teorema requer o axioma da escolha - precisamos escolher um elemento arbitrário para iniciar a iteração de, para obter a sequência de Cauchy . μ ( f ) a A f a , f ( a ) , f 2 ( a ) , f 3 ( a ) , f:AAμ(f)aAfuma,f(uma),f2(uma),f3(uma),...

  1. Como os teoremas do ponto fixo são declarados na análise construtiva?
  2. Além disso, existem referências concisas a espaços métricos construtivos?

O motivo pelo qual pergunto é que quero construir um modelo do Sistema F no qual os tipos também tenham estrutura métrica (entre outras coisas). É bastante útil que, na teoria construtiva dos conjuntos, possamos criar uma família de conjuntos , de modo que seja fechado em produtos, exponenciais e famílias indexadas em , o que facilita a criação de um modelo do Sistema F.U Uvocêvocêvocê

Seria muito bom se eu pudesse criar uma família semelhante de espaços ultramétricos construtivos. Mas como adicionar opções à teoria construtiva dos conjuntos a torna clássica, obviamente eu preciso ter mais cuidado com os teoremas do ponto fixo e provavelmente outras coisas também.

Neel Krishnaswami
fonte
2
Você pode alterar a hipótese para UMA sendo um conjunto habitado . Você não está invocando o axioma da escolha para escolher umaUMA .
Colin McQuillan

Respostas:

22

O axioma da escolha é usado quando há uma coleção de "coisas" e você escolhe um elemento para cada "coisa". Se houver apenas uma coisa na coleção, esse não é o axioma da escolha. No nosso caso, temos apenas um espaço métrico e estamos "escolhendo" um ponto nele. Então isso não é o axioma de escolha, mas a eliminação de quantificadores existenciais, ou seja, temos uma hipótese e dizemos "seja x A tal que ϕ ( x ) ". Infelizmente, as pessoas costumam dizer "xA.ϕ(x)xAϕ(x) xA ", que se parece com a aplicação do axioma de escolha.ϕ(x)

Para referência, aqui está uma prova construtiva do teorema do ponto fixo de Banach.

Teorema: Uma contração em um espaço métrico completo habitado tem um ponto fixo exclusivo.

Prova. Suponha que seja um espaço métrico completo habitado ef : M M é uma contração. Porque f é um contracção existe α tal que 0 < α < 1 e d ( f ( x ) , f ( y ) ) α d ( x , y ) para todos os x , y M(M,d)f:MMfα0 0<α<1 1d(f(x),f(y))αd(x,y)x,yM.

Suponha que e v são ponto de fixa f . Então temos d ( u , v ) = d ( f ( u ) , f ( v ) ) α d ( u , v ) a partir do qual se segue que 0 d ( u , v ) ( α - 1 ) d ( u , v ) vocêvf

d(você,v)=d(f(você),f(v))αd(você,v)
, portanto d ( u , v ) = 0 e u = v . Isso prova que f tem no máximo um ponto fixo.0 0d(você,v)(α-1 1)d(você,v)0 0d(você,v)=0 0u=vf

Resta provar a existência de um ponto fixo. Porque é habitado existe x 0M . Defina a sequência ( x i ) recursivamente por x i + 1 = f ( x i ) . Podemos provar por indução que d ( x i , x i + 1 ) α id ( x 0 , x 1 ) . Daí resulta queMx0M(xi)

xEu+1 1=f(xEu).
d(xEu,xEu+1 1)αEud(x0 0,x1 1) é uma sequência de Cauchy. Como M está completo, a sequência tem um limite y = lim i x i . Como f é uma contração, é uniformemente contínua e, portanto, comuta com limites de seqüências: f ( y ) = f ( lim i x i ) = lim i f ( x i ) = lim i x i + 1 = lim i x Eu(xEu)My=limEuxEuf Assim, y é um ponto fixo de f . QED
f(y)=f(limEuxEu)=limEuf(xEu)=limEuxEu+1 1=limEuxEu=y.
yf

Observações:

  1. Tomei cuidado para não dizer "escolha " e "escolha x 0 ". É comum dizer essas coisas, e elas apenas aumentam a confusão que impede os matemáticos comuns de serem capazes de dizer o que é e o que não é o axioma da escolha.αx0 0

  2. vocêvf¬¬(você=v)você=v

  3. (xEu)x0 0xM.x0 0M

  4. MxM.M¬xM.

  5. fEuxMMM

  6. Finalmente, os seguintes teoremas de ponto fixo têm versões construtivas:

    • Teorema de ponto fixo de Knaster-Tarski para mapas monótonos em treliças completas
    • Teorema de ponto fixo de Banach para contrações em um espaço métrico completo
    • Teorema de ponto fixo de Knaster-Tarski para mapas monótonos em dcpos (comprovado por Pataraia)
    • Vários teoremas de ponto fixo na teoria de domínio geralmente têm provas construtivas
    • O teorema da recursão é uma forma de teorema de ponto fixo e possui uma prova construtiva
    • Eu provei que o teorema de ponto fixo de Knaster-Tarski para mapas monótonos em posets completos em cadeia não tem uma prova construtiva. Da mesma forma, o teorema de ponto fixo de Bourbaki-Witt para mapas progressivos em posets de cadeia completa falha construtivamente. O contra-exemplo para o posterior vem dos topos efetivos: nos topos efetivos, os ordinais (adequadamente definidos) formam um conjunto e os mapas sucessores são progressivos e não têm pontos fixos. A propósito, o mapa sucessor nos ordinais não é monótono nos topos efetivos.

Agora isso é mais informações do que você pediu.

Andrej Bauer
fonte
11
Algum dos axiomas dos espaços métricos precisa ser reformulado?
Neel Krishnaswami
essa é mais uma boa resposta, Andrej!
Suresh Venkat
11
@ Neel: Não, os axiomas são os mesmos do caso clássico.
Andrej Bauer
2
fEuxfEuxfEux
2
fEuxfEux=λM.λf.f(fEuxM(f))MfMM