Reflective oracles as a solution to the converse Lawvere problem

(This post was origi­nally pub­lished on Nov 30th 2017, and is 1 of 4 posts brought for­warded to­day as part of the AI Align­ment Fo­rum launch se­quence on fixed points.)

1 Introduction

Be­fore the work of Tur­ing, one could jus­tifi­ably be skep­ti­cal of the idea of a uni­ver­sal com­putable func­tion. After all, there is no com­putable func­tion such that for all com­putable there is some in­dex such that for all . If there were, we could pick , and then a con­tra­dic­tion. Of course, uni­ver­sal Tur­ing ma­chines don’t run into this ob­sta­cle; as Gödel put it, “By a kind of mir­a­cle it is not nec­es­sary to dis­t­in­guish or­ders, and the di­ag­o­nal pro­ce­dure does not lead out­side the defined no­tion.” [1]

The mir­a­cle of Tur­ing ma­chines is that there is a par­tial com­putable func­tion such that for all par­tial com­putable there is an in­dex such that for all . Here, we look at a differ­ent “mir­a­cle”, that of re­flec­tive or­a­cles [2,3]. As we will see in The­o­rem 1, given a re­flec­tive or­a­cle , there is a (stochas­tic) -com­putable func­tion such that for any (stochas­tic) -com­putable func­tion , there is some in­dex such that and have the same dis­tri­bu­tion for all . This ex­is­tence the­o­rem seems to skirt even closer to the con­tra­dic­tion men­tioned above.

We use this idea to an­swer “in spirit” the con­verse Law­vere prob­lem posed in [4]. Th­ese meth­ods also gen­er­al­ize to prove a similar analogue of the ubiquitous con­verse Law­vere prob­lem from [5]. The origi­nal ques­tions, stated in terms of topol­ogy, re­main open, but I find that the model pro­posed here, us­ing com­putabil­ity, is equally satis­fy­ing from the point of view of study­ing re­flec­tive agents. Those refer­ences can be con­sulted for more mo­ti­va­tion on these prob­lems from the per­spec­tive of re­flec­tive agency.

Sec­tion 3 proves the main lemma, and proves the con­verse Law­vere the­o­rem for re­flec­tive or­a­cles. In sec­tion 4, we use that to give a (cir­cu­lar) proof of Brouwer’s fixed point the­o­rem, as men­tioned in [4]. In sec­tion 5, we prove the ubiquitous con­verse Law­vere the­o­rem for re­flec­tive or­a­cles.

2 Definitions

For any mea­surable space , the set of prob­a­bil­ity mea­sures on is de­noted .

A prob­a­bil­is­tic or­a­cle is a map . A prob­a­bil­is­tic or­a­cle ma­chine is a prob­a­bil­is­tic Tur­ing ma­chine that can query a prob­a­bil­is­tic or­a­cle . On a given query , it gets the an­swer with prob­a­bil­ity and the an­swer oth­er­wise. Differ­ent queries are in­de­pen­dent events, so this com­pletely de­ter­mines the be­hav­ior of such a ma­chine.

We de­note by the stochas­tic par­tial -com­putable func­tion , where rep­re­sents non­halt­ing, com­puted by the prob­a­bil­is­tic Tur­ing ma­chine with in­dex . The no­ta­tion in­di­cates the event that halts on in­put , and is the event that halts and out­puts . Fi­nally, is the event that does not halt on in­put .

We use to rep­re­sent a com­putable cod­ing func­tion, in or­der to bi­ject ar­bi­trary countable sets to the nat­u­rals for the pur­pose of com­putabil­ity.

A re­flec­tive or­a­cle is a prob­a­bil­is­tic or­a­cle such that for all and , For more on re­flec­tive or­a­cles, see Fallen­stein et al., 2015 [2].

A func­tion is -com­putable if there is an in­dex such that for all , we have and That is, rep­re­sents by prob­a­bil­is­ti­cally out­putting ei­ther or .

For any , a func­tion is -com­putable if each co­or­di­nate for is -com­putable.

A func­tion is -com­putable if the cor­re­spond­ing func­tion given by is -com­putable.

For any point , a prob­a­bil­is­tic or­a­cle is com­pat­i­ble with if for all , we have if and if . More gen­er­ally, for any and any , a prob­a­bil­is­tic or­a­cle is com­pat­i­ble with if for all such that and all , we have if and if .

A func­tion is -com­putable if for each co­or­di­nate , there is an in­dex such that when­ever is com­pat­i­ble with , we have and

A map is -com­putably ubiquitous if for ev­ery -com­putable map , there is some such that .

3 Con­verse Law­vere property

We first need a lemma that tells us that we can re­place cer­tain par­tial -com­putable func­tions with to­tal ones when work­ing rel­a­tive to a re­flec­tive or­a­cle. As dis­cussed in the in­tro­duc­tion, this con­trasts strongly with the situ­a­tion for com­putable func­tions. All of our the­o­rems will make es­sen­tial use of this lemma.

Lemma 1 (to­tal­iz­ing): There is a com­putable map such that for all and any re­flec­tive or­a­cle , we have and for ,

Proof: We con­struct us­ing a re­cur­sive pro­ce­dure that en­sures that up­per-bounds us­ing what may be thought of as re­peated sub­di­vi­sion or bi­nary search. This is es­sen­tially the same as the func­tion in [3], but we han­dle com­putabil­ity is­sues differ­ently. Let be the set of pairs of dyadic ra­tio­nals such that . We re­cur­sively define a stochas­tic -com­putable func­tion ; the in­tent is to have equal if that quan­tity is in the in­ter­val , and take the clos­est pos­si­ble value, ei­ther or , oth­er­wise. Then, we will be able to define to be .

Con­struct so that a call first queries , where , and also flips a fair coin . Then, it ei­ther out­puts , , or the re­sult of a re­cur­sive call, as fol­lows: We can now choose so that .

This al­gorithm up­per bounds the prob­a­bil­ities and by bi­nary search. Once the ini­tial call has re­cursed to , it has already halted out­putting with prob­a­bil­ity , con­firm­ing that this is an up­per bound since it re­ceived an­swer from a call to . Similarly, it has out­put with prob­a­bil­ity , con­firm­ing this bound since it re­ceived the an­swer from a call to . Fur­ther, since each call to halts with­out re­curs­ing with prob­a­bil­ity , halts al­most surely. Thus, we get the to­tal­ity prop­erty and the bounds for .

Now we can prove our main the­o­rem.

The­o­rem 1 (con­verse Law­vere for re­flec­tive or­a­cles): Let be a re­flec­tive or­a­cle. Then, there is an -com­putable map such that for all -com­putable , there is some in­dex such that .

Proof: Us­ing from the to­tal­iz­ing lemma, let Given any -com­putable , there is some such that Then, and similarly , so .

This the­o­rem gives a com­putable analogue to the prob­lem posed in [4]. The anal­ogy would be strength­ened if we worked in a carte­sian closed cat­e­gory where the pre­sent no­tion of -com­putabil­ity gave the mor­phisms, and where is an ex­po­nen­tial ob­ject. In ad­di­tion, the to­tal­iz­ing lemma would have a nice analogue in this set­ting. I ex­pect that all this can be done us­ing some­thing like an effec­tive topos [6], but I leave this for fu­ture work.

4 Re­cov­er­ing Brouwer’s fixed point theorem

As men­tioned in [4], the in­ter­me­di­ate value the­o­rem would fol­low from the ex­is­tence of a space with the con­verse Law­vere prop­erty, that is, a space that sur­jects onto the map­ping space . Fur­ther, Brouwer’s fixed point the­o­rem on the -ball, , would fol­low from the ex­is­tence of a topolog­i­cal space with a sur­jec­tion . We can do some­thing similar to con­clude Brouwer’s fixed point the­o­rem from the con­verse Law­vere the­o­rem for re­flec­tive or­a­cles. Of course, this is cir­cu­lar; Kaku­tani’s fixed point the­o­rem, a gen­er­al­iza­tion of Brouwer’s fixed point the­o­rem, is used to prove the ex­is­tence of re­flec­tive or­a­cles. Still, it is in­ter­est­ing to see how this can be done.

We start with two tech­ni­cal lem­mas tel­ling us some ba­sic facts about re­flec­tive-or­a­cle-com­putable func­tions . Us­ing these, it will be easy to de­rive Brouwer’s fixed point the­o­rem.

Lemma 2 (con­tin­u­ous im­plies rel­a­tively com­putable): Take and let be con­tin­u­ous. Then, there is a (de­ter­minis­tic) or­a­cle such that is -com­putable.

Proof: For each co­or­di­nate of , each rec­t­an­gle with ra­tio­nal end­points, and each pair of ra­tio­nals with , let be if and oth­er­wise. To see that is -com­putable, we com­pute any for any with , and any , mak­ing use of and any or­a­cle com­pat­i­ble with .

We pro­ceed by a search pro­cess similar to the ar­gu­ment in the to­tal­iz­ing lemma. Start with , and . At each step , perform an ex­haus­tive search for a rec­t­an­gle and points such that a query to re­turns for all , a query to any re­turns 0, a query to re­turns , and where ei­ther and , or and . In the first case, out­put with prob­a­bil­ity and con­tinue with prob­a­bil­ity , and in the sec­ond case, out­put with prob­a­bil­ity and con­tinue with prob­a­bil­ity .

By con­struc­tion, and at each stage . Since is con­tin­u­ous, there is some neigh­bour­hood of on which its image is con­tained in ei­ther or . There are two pos­si­bil­ities to con­sider. If , then there is some rec­t­an­gle con­tained in such a neigh­bour­hood of , and with . This rec­t­an­gle would be cho­sen if con­sid­ered, so the al­gorithm will move be­yond step .

The re­main­ing pos­si­bil­ity is that is on the bound­ary of ; say, . Since was cho­sen pre­vi­ously though, we know that query­ing has re­turned at least once, so . Thus, the al­gorithm will al­most surely even­tu­ally ac­cept or an­other rec­t­an­gle.

Put­ting this to­gether, this al­gorithm al­most surely halts, out­putting ei­ther or . By stage , it has halted out­putting with prob­a­bil­ity and out­putting with prob­a­bil­ity , so over­all it out­puts with prob­a­bil­ity . Thus, is -com­putable.

Lemma 3 (com­po­si­tion): Let be a re­flec­tive or­a­cle and let and be -com­putable. Then, is -com­putable.

Proof: For each with , take such that wit­nesses the com­putabil­ity of . Then, if and if , so lets us simu­late a prob­a­bil­is­tic or­a­cle com­pat­i­ble with . Hence, by the -com­putabil­ity of , for each with , we have a prob­a­bil­is­tic -ma­chine that always halts, out­putting ei­ther or , and that on in­put out­puts with prob­a­bil­ity .

The­o­rem 2 (Brouwer’s fixed point the­o­rem): Take and . Then, has a fixed point.

Proof: By Lemma 2, we have an or­a­cle such that is -com­putable. By rel­a­tiviz­ing the con­struc­tion of a re­flec­tive or­a­cle [2,3] to , we get a re­flec­tive or­a­cle above . No­tice that is -com­putable. Let­ting be the -com­putable func­tion con­structed in the con­verse Law­vere the­o­rem for re­flec­tive or­a­cles, define by The rest will now fol­low the proof of Law­vere’s fixed point the­o­rem [7].

Define by ; this is -com­putable by Lemma 3. Now, by con­verse Law­vere the­o­rem, for each co­or­di­nate of , there is some such that . Let­ting , we have so , and so is a fixed point of .

5 Ubiquitous con­verse Law­vere property

The­o­rem 3 (ubiquitous con­verse Law­vere): Let be a re­flec­tive or­a­cle. Then, there is an -com­putable, -com­putably ubiquitous map .

Proof: This fol­lows by a com­bi­na­tion of the re­cur­sion the­o­rem and the to­tal­iz­ing lemma. We use the same map from The­o­rem 1. Let be any -com­putable map. There is a com­putable map such that for all , we have and By the re­cur­sion the­o­rem, there is some such that . Then, so .

References

[1] Kurt Gödel. 1946. “Re­marks be­fore the Prince­ton bi­cen­ten­nial con­fer­ence of prob­lems in math­e­mat­ics.” Reprinted in: Martin Davis. 1965. “The Un­de­cid­able. Ba­sic Papers on Un­de­cid­able Propo­si­tions, Un­solv­able Prob­lems, and Com­putable Func­tions.” Raven Press.

[2] Benja Fallen­stein, Jes­sica Tay­lor, and Paul F. Chris­ti­ano. 2015. “Reflec­tive Or­a­cles: A Foun­da­tion for Clas­si­cal Game The­ory.” arXiv: 1508.04145.

[3] Benya Fallen­stein, Nate Soares, and Jes­sica Tay­lor. 2015. “Reflec­tive var­i­ants of Solomonoff in­duc­tion and AIXI.” In Ar­tifi­cial Gen­eral In­tel­li­gence. Springer.

[4] Scott Garrabrant. 2017. “For­mal Open Prob­lem in De­ci­sion The­ory.” https://​agent­foun­da­tions.org/​item?id=1356.

[5] Scott Garrabrant. 2017. “The Ubiquitous Con­verse Law­vere Prob­lem.” https://​agent­foun­da­tions.org/​item?id=1372

[6] Jaap van Oosten. 2008. “Real­iz­abil­ity: an in­tro­duc­tion to its cat­e­gor­i­cal side.” Stud­ies in Logic and the Foun­da­tions of Math­e­mat­ics, vol. 152. El­se­vier.

[7] F. William Law­vere. 1969. “Di­ag­o­nal ar­gu­ments and carte­sian closed cat­e­gories.” In Cat­e­gory The­ory, Ho­mol­ogy The­ory and their Ap­pli­ca­tions, II (Bat­telle In­sti­tute Con­fer­ence, Seat­tle, Wash., 1968, Vol. Two), pages 134–145. Springer.


This post was origi­nally pub­lished on Nov 30th 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.