Теоремы о неподвижной точке для конструктивных метрических пространств?

15

Теорема Банаха о неподвижной точке говорит, что если у нас есть непустое полное метрическое пространство , то любая равномерно сжимающая функция имеет единственную неподвижную точку . Однако доказательство этой теоремы требует аксиомы выбора - нам нужно выбрать произвольный элемент чтобы начать итерацию , чтобы получить последовательность Коши . 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. Как формулируются теоремы о неподвижной точке в конструктивном анализе?
  2. Кроме того, есть ли краткие ссылки на конструктивные метрические пространства?

Причина, по которой я спрашиваю, состоит в том, что я хочу построить модель Системы F, в которой типы дополнительно несут метрическую структуру (среди прочего). Весьма полезно, что в конструктивной теории множеств мы можем составить семейство множеств , такое, что замкнуто относительно произведений, экспонент и семейств, индексированных по , что упрощает создание модели системы F.U UUUU

Было бы очень хорошо, если бы я мог создать аналогичное семейство конструктивных ультраметрических пространств. Но поскольку добавление выбора в конструктивную теорию множеств делает ее классической, очевидно, мне нужно быть более осторожным в отношении теорем о неподвижной точке и, возможно, других вещей.

Нил Кришнасвами
источник
2
Вы можете изменить гипотезу на являющуюся обитаемым множеством . Вы не вызывая аксиому выбора , чтобы выбрать . AaA
Колин МакКийан,

Ответы:

22

Аксиома выбора используется, когда существует набор «вещей», и вы выбираете один элемент для каждой «вещи». Если в коллекции есть только одна вещь, это не аксиома выбора. В нашем случае у нас есть только одно метрическое пространство, и мы «выбираем» точку в нем. Так что это не аксиома выбора, а исключение экзистенциальных кванторов, т. Е. У нас есть гипотеза и мы говорим "пусть таково, что ". К сожалению, люди часто говорят « выберите такой что », что тогда выглядит как применение аксиомы выбора.x A ϕ ( x ) x A ϕ ( x )xA.ϕ(x)xAϕ(x) xAϕ(x)

Для справки приведем конструктивное доказательство теоремы Банаха о неподвижной точке.

Теорема: сжатие на обитаемом полном метрическом пространстве имеет единственную неподвижную точку.

Доказательство. Предположим, что - обитаемое полное метрическое пространство, а - сжатие. Поскольку является сокращением, существует такое, что и для всех ,f : M M f α 0 < α < 1 d ( f ( x ) , f ( y ) ) α d ( x , y ) x , y M(M,d)f:MMfα0<α<1d(f(x),f(y))αd(x,y)x,yM

Предположим, что и - фиксированная точка . Тогда имеем из чего следует, что , следовательно, и . Это доказывает, что имеет не более одной фиксированной точки.v f d ( u , v ) = d ( f ( u ) , f ( v ) ) α d ( u , v ) 0 d ( u , v ) ( α - 1 ) d ( u , v ) 0 d ( u , v ) = 0 uuvf

d(u,v)=d(f(u),f(v))αd(u,v)
0d(u,v)(α1)d(u,v)0d(u,v)=0fu=vf

Осталось доказать существование неподвижной точки. Поскольку населен существует . Определите последовательность рекурсивно с помощьюПо индукции мы можем доказать, что . Отсюда следует, что - последовательность Коши. Поскольку завершена, последовательность имеет предел . Поскольку - сокращение, оно равномерно непрерывно и поэтому коммутирует с пределами последовательностей: Таким образом, является фиксированной точкойx 0M ( x i ) x i + 1 = f ( x i ) . d ( x i , x i + 1 ) α id ( x 0 , x 1 ) ( x i ) M y = lim i x i f f ( y ) = f (Mx0M(xi)

xi+1=f(xi).
d(xi,xi+1)αid(x0,x1)(xi)My=limixif
f(y)=f(limixi)=limif(xi)=limixi+1=limixi=y.
yf . QED

Примечания:

  1. Я был осторожен, чтобы не сказать «выбрать » и «выбрать ». Такие вещи часто говорят, и они только добавляют путаницы, которая мешает обычным математикам определять, что является аксиомой выбора, а что нет.αx0

  2. В части единственности доказательства люди часто без необходимости предполагают, что существуют две разные фиксированные точки, и получают противоречие. Таким образом, им удалось только доказать, что если и являются неподвижными точками то . Так что теперь им нужно исключить середину, чтобы добраться до . Даже для классической математики это неоптимально и просто показывает, что автор доказательства не придерживается хорошей логической гигиены.uvf¬¬(u=v)u=v

  3. В доказательственной части доказательства последовательность зависит от экзистенциального свидетеля мы получим, исключив предположение . Там нет ничего плохого. Мы делаем такие вещи постоянно. Мы ничего не выбрали. Подумайте об этом так: кто-то еще дал нам свидетельство о населенности , и мы можем что-то с этим сделать.(xi)x0xM.x0M

  4. Классически « обитаем» ( ) и « непусто» ( ) эквивалентны. Конструктивно первое имеет больше смысла и полезно.х М . М ¬ х М . MxM.M¬xM.

  5. Поскольку мы показали уникальность фиксированных точек, мы фактически получаем оператор с фиксированными точками из сокращений в точки , а не просто оператор . MMfixMMM

  6. Наконец, следующие теоремы о неподвижной точке имеют конструктивные версии:

    • Теорема Кнастера-Тарского о неподвижной точке для монотонных отображений на полных решетках
    • Теорема Банаха о неподвижной точке для сжатий на полном метрическом пространстве
    • Теорема Кнастера-Тарского о неподвижной точке для монотонных отображений на dcpos (доказано Патараем)
    • Различные теоремы о неподвижной точке в теории областей обычно имеют конструктивные доказательства
    • Теорема о рекурсии является формой теоремы о неподвижной точке и имеет конструктивное доказательство
    • Я доказал теорему, Кнастер-Тарский с фиксированной точкой для карт монотонных на цепном полный ч.у.м. вовсе не имеет конструктивное доказательство. Точно так же теорема Бурбаки-Витта о неподвижной точке для прогрессивных отображений на полнотелых цепочках конструктивно не выполняется. Контрпример для более позднего происходит из эффективного топоса: в эффективных топосах ординалы (соответственно определенные) образуют множество, а карты-преемники являются прогрессивными и не имеют фиксированных точек. Кстати, карта преемников на ординалах не монотонна в эффективных топосах.

Теперь это гораздо больше информации, чем вы просили.

Андрей Бауэр
источник
1
Нужно ли переформулировать какую-либо из аксиом метрических пространств?
Нил Кришнасвами
это еще один хороший ответ, Андрей!
Суреш Венкат
1
@Neel: Нет, аксиомы такие же, как в классическом случае.
Андрей Бауэр
2
Я вижу, вы снимаете для системы F. В этом случае вы можете рассмотреть вопрос о том, является ли оператор с фиксированной точкой подходящим образом полиморфным. Но сначала вы должны ответить "это вообще функция?" потому что, похоже, в построении есть выбор (для каждого обитаемого полного метрического пространства мы «выбираем» точку). Однако выбора нет, поскольку значение не зависит от начальной точки. (продолжение)е я х е я хfixfixfix
Андрей Бауэр
2
Или, другими словами, все в порядке, потому что является единственным решением уравнения с фиксированной точкой где лежит в населенных полных метрических пространствах, а - сокращение на (если вы запишите тип, вы увидите полиморфизм в ). е я х = Х М . λ ф . f ( f i x M ( f ) ) M f M Mfixfix=λM.λf.f(fixM(f))MfMM
Андрей Бауэр