Fixed Point Discussion

Warn­ing: This post con­tains some im­por­tant spoilers for Topolog­i­cal Fixed Point Ex­er­cises, Di­ag­o­nal­iza­tion Fixed Point Ex­er­cises, and Iter­a­tion Fixed Point Ex­er­cises. If you plan to even try the ex­er­cises, read­ing this post will sig­nifi­cantly re­duce the value you can get from do­ing them.

Core Ideas

A fixed point of a func­tion is an in­put such that . Fixed point the­o­rems show that var­i­ous types of func­tions must have fixed points, and some­times give meth­ods for find­ing those fixed points.

Fixed point the­o­rems come in three fla­vors: Topolog­i­cal, Di­ag­o­nal, and Iter­a­tive. (I some­times re­fer to them by cen­tral ex­am­ples as Brouwer, Law­vere, and Banach, re­spec­tively.)

Topolog­i­cal fixed points are non con­struc­tive. If is con­tin­u­ous, , and , then we know must have some fixed point be­tween and , since must some­where tran­si­tion from be­ing greater than to be­ing less than . This does not tell us where it hap­pens. This can be es­pe­cially trou­ble­some when there are mul­ti­ple fixed points, and there is no prin­ci­pled way to choose be­tween them.

Di­ag­o­nal fixed points are con­structed with a weird trick where you feed a code for a func­tion into that func­tion it­self. Given a func­tion , if you can con­struct a func­tion , which on in­put , in­ter­prets as a func­tion, runs on it­self, and then runs on the re­sult (i.e. .), then is a fixed point of be­cause . This is not just an ex­am­ple; ev­ery­thing in the cluster looks like this. It is a weird trick, but it is ac­tu­ally very im­por­tant.

Iter­a­tive fixed points can be found through iter­a­tion. For ex­am­ple, if , then start­ing with any value, iter­at­ing for­ever will con­verge to the unique fixed point .

(There is a fourth cluster in num­ber the­ory dis­cussed here, but I am leav­ing it out, since it does not seem rele­vant to AI, and be­cause I am not sure whether to put it by it­self or to tack it onto the topolog­i­cal cluster.)

Topolog­i­cal Fixed Points

Ex­am­ples of topolog­i­cal fixed point the­o­rems in­clude Sperner’s lemma, the Brouwer fixed point the­o­rem, the Kaku­tani fixed point the­o­rem, the in­ter­me­di­ate value the­o­rem, and the Poin­caré-Miranda the­o­rem.

  • Brouwer is the cen­tral ex­am­ple of the cluster. Brouwer states that any con­tin­u­ous func­tion from a com­pact con­vex set to it­self has a fixed point.

  • Sperner’s Lemma is a dis­crete analogue which is used in one proof of Brouwer.

  • Kaku­tani is a strength­en­ing of Brouwer to de­gen­er­ate set val­ued func­tions, that look al­most like con­tin­u­ous func­tions.

  • Poin­caré-Miranda is an al­ter­nate for­mu­la­tion of Brouwer, which is about find­ing ze­ros rather than fixed points.

  • The In­ter­me­di­ate Value The­o­rem is a spe­cial case of Poin­caré-Miranda. To a first ap­prox­i­ma­tion, you can think of all of these the­o­rems as one big the­o­rem.

Topolog­i­cal fixed point the­o­rems also have some very large ap­pli­ca­tions. The Kaku­tani fixed point the­o­rem is used in game the­ory to show that Nash equil­ibria ex­ist, and to show that mar­kets have equil­ibrium prices! Sperner’s lemma is also used in some envy-free fair di­vi­sion re­sults. Brouwer is also used is to show the ex­is­tence of some differ­en­tial equa­tions.

In MIRI’s agent foun­da­tions work, Kaku­tani is used to con­struct prob­a­bil­is­tic truth pred­i­cates and re­flec­tive or­a­cles, and Brouwer is used to con­struct log­i­cal in­duc­tors.

Th­ese ap­pli­ca­tions all use topolog­i­cal fixed points very di­rectly, and so carry with them most of the philo­soph­i­cal bag­gage of topolog­i­cal fixed points. For ex­am­ple, while Nash equil­ibria ex­ist, they are not unique, are com­pu­ta­tion­ally hard to find, and feel non-con­struc­tive and ar­bi­trary.

Di­ag­o­nal Fixed Points

Di­ag­o­nal fixed point the­o­rems are all cen­tered around the ba­sic struc­ture of , where , as men­tioned pre­vi­ously.

The pat­tern is used in many places.

In MIRI’s agent foun­da­tions work, this shows up in the Löbian ob­sta­cle to self-trust, Löbian hand­shakes in Mo­dal Com­bat and Bounded Open Source Pri­soner’s Dilemma, as well as pro­vid­ing a ba­sic foun­da­tion for why an agent rea­son­ing about it­self might make sense at all through quines.

Iter­a­tive Fixed Points

Iter­a­tive fixed point the­o­rems are less of one cluster than the oth­ers; I will fac­tor it into two sub-clusters, cen­tered around the Banach fixed point the­o­rem and Tarski fixed point the­o­rem. (Each the same size as the origi­nal.)

The Tarski cluster is about fixed points of mono­tonic func­tions on (par­tially) or­dered sets found by iter­a­tion. Tarski’s fixed point the­o­rem states that any or­der pre­serv­ing func­tion on a com­plete lat­tice has a fixed point (and fur­ther the set of fixed points forms a com­plete lat­tice). The least fixed point can be found by start­ing with the least el­e­ment and iter­at­ing the func­tion trans­finitely. This, for ex­am­ple, im­plies that ev­ery mono­tonic func­tion on from to it­self has a fixed point, even if it is not con­tin­u­ous. Kleene’s fixed point the­o­rem strength­ens the as­sump­tions of Tarski by adding a form of con­ti­nu­ity (and also re­moves some ir­rele­vant as­sump­tions), which gives us that the least fixed point can be found by iter­at­ing the func­tion only ω times. The fixed point lemma for nor­mal func­tions is similar to Kleene, but with or­di­nals rather than par­tial or­ders. It states that any strictly in­creas­ing con­tin­u­ous func­tion on or­di­nals has ar­bi­trar­ily large fixed points.

The Banach cluster is about fixed points of con­trac­tive func­tions on met­ric spaces found by iter­a­tion. A con­trac­tive func­tion is a func­tion that sends points closer to­gether. A func­tion is con­trac­tive if there ex­ists an such that for all . Banach’s fixed point the­o­rem state that any con­trac­tive func­tion has a unique fixed point. This fixed point is for any start­ing point . An ap­pli­ca­tion of this to lin­ear func­tions is that any er­godic sta­tion­ary Markov chain has a sta­tion­ary dis­tri­bu­tion (which is a fixed point of the tran­si­tion map), which is con­verged to via iter­a­tion. This is also used in show­ing that cor­re­lated equil­ibria ex­ist and can be found quickly. Banach can also be used to show that gra­di­ent de­scent con­verges ex­po­nen­tially quickly on a strongly con­vex func­tion.

In­ter­dis­ci­plinary Nature

I think of Pure Math­e­mat­ics as di­vided at the top into 5 sub­fields: Alge­bra, Anal­y­sis, Topol­ogy, Logic, and Com­bi­na­torics.

The map­ping of the key fixed point the­o­rems dis­cussed in the ex­er­cises into these cat­e­gories is sur­jec­tive:

  • Law­vere’s fixed point the­o­rem is Algebra

  • Banach’s fixed point the­o­rem is Analysis

  • Brouwer fixed point the­o­rem is Topology

  • Gödel’s first in­com­plete­ness the­o­rem is Logic

  • Sperner’s lemma is Com­bi­na­torics.

On top of that, ma­jor ap­pli­ca­tions of fixed point the­o­rems show up in Differ­en­tial Equa­tions, CS the­ory, Ma­chine Learn­ing, Game The­ory, and Eco­nomics.

To­mor­row’s AI Align­ment Fo­rum se­quences post will be two short posts ‘Ap­proval-di­rected boot­strap­ping’ and ‘Hu­mans con­sult­ing HCH’ by Paul Chris­ti­ano in the se­quence Iter­ated Am­plifi­ca­tion.

The next post­ing in this se­quence will be four posts of Agent Foun­da­tions re­search that use fixed point the­o­rems, on Wed­nes­day 28th Novem­ber. Th­ese will be re-posts of con­tent from the now-de­funct Agent Foun­da­tions fo­rum, all of whose con­tent is now find­able on the AI Align­ment Fo­rum (and all old links will soon be re-di­rected to the AI Align­ment Fo­rum).