Hyperreal Brouwer

(This post was origi­nally pub­lished on Oct 6th 2017, and has been tem­porar­ily brought for­warded as part of the AI Align­ment Fo­rum launch se­quence on fixed points.)

This post ex­plains how to view Kaku­tani’s fixed point the­o­rem as a spe­cial case of Brouwer’s fixed point the­o­rem with hy­per­real num­bers. This post is just math in­tu­itions, but I found them use­ful in think­ing about Kaku­tani’s fixed point the­o­rem and many things in agent foun­da­tions. This came out of con­ver­sa­tions with Sam Eisen­stat.

Brouwer’s fixed the­o­rem says that a con­tin­u­ous func­tion from a com­pact con­vex sub­set of to it­self has fixed point. Kaku­tani’s fixed point is similar, but in­stead of con­tin­u­ous func­tions, it uses Kaku­tani func­tions, which are set val­ued func­tions with closed graph which are point wise nonempty and con­vex.

When I think about Kaku­tani func­tions, I usu­ally think about them as limits of con­tin­u­ous func­tions. For ex­am­ple, con­sider the kaku­tani func­tion from to it­self which sends nega­tive in­puts to , pos­i­tive in­puts to , and sends to the en­tire in­ter­val. You can view as a the limit of a se­quence of func­tions sends to . This is not a point wise limit, since if it was would be sent to 0, rather than the en­tire in­ter­val. In­stead, it is a limit in the Haus­dorff met­ric be­tween the graphs of the func­tions.

Given two com­pact nonempty sub­sets and of , the Haus­dorff dis­tance be­tween and is the max­i­mum over all points in or of the Eu­clidean dis­tance be­tween that point and the clos­est point in the other set. Since and are com­pact, this max­i­mum is achieved.

Given com­pact con­vex sub­sets and of , we say that a se­quence of con­tin­u­ous func­tions from to con­verges in graph Haus­dorff dis­tance to the closed graph set val­ued func­tion if the graphs of viewed as sub­sets of con­verges to the graph of in Haus­dorff dis­tance.

We say that a closed graph func­tion from to is a con­tin­u­ous graph limit of if there ex­ists a se­quence of con­tin­u­ous func­tions which con­verges to in graph Haus­dorff dis­tance.

The­o­rem 1: Every con­tin­u­ous graph limit from a com­pact con­vex sub­set of to it­self has a fixed point (a point con­tained in its image).

Proof: is a limit of con­tin­u­ous func­tions each of which has a fixed point by Brouwer. Choose one fixed point from each to get a se­quence of points which has a con­ver­gent sub­se­quence by Bolzano–Weier­strass. Let be the limit of this con­ver­gent sub­se­quence. If did not con­tain , then would not be in the graph of . Since is closed graph, a ball around would not be in the graph of , which con­tra­dicts the fact that must con­tain func­tions with graphs ar­bi­trar­ily close to the graph of with fixed points ar­bi­trar­ily close to and thus points in their graphs ar­bi­trar­ily close to .

This the­o­rem is not equiv­a­lent to Kaku­tani’s fixed point the­o­rem. There ex­ist con­tin­u­ous graph limits which are not point wise con­vex (but only in more than one di­men­sion). For ex­am­ple the func­tion from to which sends ev­ery point to the cir­cle of points dis­tance 1 from is not Kaku­tani, but is a con­tin­u­ous graph limit. It is the limit of func­tions given by .

How­ever, this the­o­rem is strictly stronger that Kaku­tani’s fixed point the­o­rem (al­though some­times harder to use, since show­ing a func­tion is Kaku­tani might be eas­ier than show­ing it is a con­tin­u­ous graph limit)

The­o­rem 2: Given com­pact con­vex sub­sets and of , ev­ery Kaku­tani func­tion from to is a con­tin­u­ous graph limit.

Proof: We define a func­tion as fol­lows. Take a finite set of ra­dius open balls in such that each ball in­ter­sects the graph of , the co­or­di­nates of the cen­ters of all the balls are dis­tinct, and the balls cover the en­tire graph of . This in­duces a cov­er­ing of by ra­dius open balls by tak­ing balls cen­tered at the co­or­di­nates of the cen­ters of . We con­tin­u­ously map each point in to a weighted av­er­age of balls in as fol­lows. If a point is the cen­ter of some ball, it is sent to 100% that ball. Other­wise, it is sent to a com­bi­na­tion of all the balls in which it is con­tained with weight pro­por­tional to (the re­cip­ro­cal of the dis­tance to the cen­ter of that ball) minus . This gives a func­tion from to by map­ping each point to the weighted av­er­age of the co­or­di­nates of the cen­ters of the balls in with weights equal to the weights of the cor­re­spond­ing balls in above. One can ver­ify that is con­tin­u­ous.

Ob­serve that the graph of con­tains the cen­ters of all balls in . Thus, con­tains points within of ev­ery point is the graph of . Thus, if did not con­verge to , it must be be­cause in­finitely many con­tain points a dis­tance from the graph of bounded away from . Con­sider a con­ver­gent sub­se­quence of these points. This gives a point not in the graph of and a sub­se­quence of the with points in their graphs con­verg­ing to .

Let be half the dis­tance be­tween and , and con­sider the set of all points in at most from the near­est point in . Note that is con­vex. Note that all in the graph of with suffi­ciently close to must have in , since oth­er­wise there would be with con­verg­ing to which must have a con­ver­gent sub­se­quence with con­verg­ing to a point not in , con­tra­dict­ing the fact that has closed graph.

How­ever must send all points within dis­tance of to a point in the con­vex hull of the images un­der of points within of . But, we showed that for suffi­ciently small and suffi­ciently large all of these points must be in . There­fore, for all suffi­ciently large , must send all points within of to points in , which are bounded away from , con­tra­dict­ing the as­sump­tion that points in the con­verge to .

Corol­lary: Kaku­tani’s fixed point theorem

We have proven (a strength­en­ing of) Kaku­tani’s Fixed Point The­o­rem from Brouwer’s fixed point the­o­rem, and given a way to think about Kaku­tani func­tions as just limits of graphs of con­tin­u­ous func­tions, and thus have bet­ter in­tu­itions about what (a su­per­set of) Kaku­tani func­tions look like. We will now take this fur­ther and think about Kaku­tani as a con­se­quence of an analogue of Brouwer us­ing Hyper­real in­finites­i­mal num­bers. (I am go­ing to be in­for­mal now. I am not go­ing to use stan­dard no­ta­tion here. I am not go­ing to make sense to peo­ple who don’t already know some­thing about non-stan­dard anal­y­sis. Sorry.)

Given a com­pact con­vex sub­set of , we can define to be the set of all equiv­alence classes of in­finite se­quences of el­e­ments of , where two se­quences are equiv­a­lent if they agree on a set that mat­ters ac­cord­ing to some ul­tra­filter on . A func­tion from to it­self is defined by a se­quence of func­tions from to it­self , where you ap­ply the func­tions poin­t­wise. I will call a func­tion hy­per-con­tin­u­ous if each of the com­po­nent func­tions is con­tin­u­ous. (I am not sure what this is ac­tu­ally called.) Each point in has a stan­dard part, which is a point in , which is the unique point such that a sub­set of com­po­nents that mat­ter con­verges to .

Claim: Every hy­per con­tin­u­ous func­tion from to it­self has a fixed point.

Proof: Just take the se­quence of the fixed points of the in­di­vi­d­ual com­po­nent func­tions.

Claim: Con­tin­u­ous graph limits from to are ex­actly those closed graph set-val­ued func­tions such that there ex­ists a hy­per-con­tin­u­ous func­tion such that if and only if there ex­ist points and with stan­dard parts and re­spec­tively such that

Proof: Use the same se­quence of func­tions with graphs con­verg­ing to that of as the se­quence of func­tions defin­ing .

Thus, we can view con­tin­u­ous graph limits (and thus Kaku­tani func­tions) as some­thing you get when look­ing at just the stan­dard part of a hy­per-con­tin­u­ous func­tion from the hy­per ver­sion of to it­self. The fixed point will fix ev­ery­thing, in­clud­ing the in­finites­i­mal parts, and we do not have to deal with any set-val­ued func­tions.

For ex­am­ple, con­sider our origi­nal func­tion from to it­self which sends nega­tive in­puts to , pos­i­tive in­puts to , and sends to the en­tire in­ter­val. We can view this as a func­tion in­volv­ing in­finites­i­mals where ev­ery­thing with pos­i­tive real part is sent to some­thing with real part , ev­ery­thing with nega­tive real part is sent to some­thing with real part , and the in­finites­i­mal num­bers very close to 0 are sent to some­thing in-be­tween. If we use the se­quence of func­tions from above and let the in­finites­i­mal be , then zoom­ing in on the in­puts be­tween and , will just be a steep lin­ear func­tion with slope .

Now to be even more vague and con­nect things back up with agent foun­da­tions, per­haps this can give some good in­tu­itions about what is hap­pen­ing with re­flec­tive or­a­cles and prob­a­bil­is­tic truth pred­i­cates. The or­a­cle/​truth pred­i­cate is effec­tively “zoom­ing in” on the area around a spe­cific prob­a­bil­ity, and when you stack or­a­cle calls or truth pred­i­cates within each other, you can zoom in fur­ther. The fact that the prob­a­bil­is­tic truth pred­i­cate does not know that it is re­flec­tively con­sis­tent, can be viewed as it not be­liev­ing a sen­tence akin to “If I as­sign prob­a­bil­ity less that to , then I also as­sign prob­a­bil­ity less that to ,” which seems very rea­son­able. It also makes re­flec­tive or­a­cles and the prob­a­bil­is­tic truth pred­i­cates look more similar to other ap­proaches to the same prob­lem that are more hi­er­ar­chy form­ing solu­tions to the same prob­lem like nor­mal halt­ing or­a­cles. Here the hi­er­ar­chy comes from zoom­ing in fur­ther and fur­ther on the in­finites­i­mal in the Kaku­tani func­tion.

This post was origi­nally pub­lished on Oct 6th 2017, and has been brought for­warded as part of the AI Align­ment Fo­rum launch se­quences.

To­mor­row’s AIAF se­quences post will be ‘Iter­ated Am­plifi­ca­tion and Distil­la­tion’ by Ajeya Co­tra, in the se­quence on iter­ated am­plifi­ca­tion.