{"entities":{"Q923069":{"pageid":924917,"ns":120,"title":"Item:Q923069","lastrevid":49427152,"modified":"2026-01-07T03:33:50Z","type":"item","id":"Q923069","labels":{"en":{"language":"en","value":"Op\u00e9rateurs de mise en m\u00e9moire et traduction de G\u00f6del. (Storage operators and G\u00f6del translation)"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4170867"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q923069$467C5C1C-CB92-4EBF-AA57-A81C3147B50C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c2e664e878aec07fea7d9770d7406e199ff8e5be","datavalue":{"value":{"text":"Op\u00e9rateurs de mise en m\u00e9moire et traduction de G\u00f6del. (Storage operators and G\u00f6del translation)","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q923069$8829501E-38E5-4329-839F-7DB40F31A56D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b6f6a037fefebe616c5bb6e9e047a733d58f3fff","datavalue":{"value":"0712.03009","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q923069$60762371-93B1-4CD7-AEE9-E9CCB2E7B7E0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d9053c6531efa75edd99b08cb8802c6636b991ea","datavalue":{"value":"10.1007/BF01792986","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q923069$E2A87F43-E108-41F0-9E53-D7A8DC578F98","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3c930bfaa88d0466feb9bef34cfbca5f6b60b9e3","datavalue":{"value":{"entity-type":"item","numeric-id":206560,"id":"Q206560"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q923069$8B6167BB-3C2F-4910-B35C-13F7EB1B5E41","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a0a7cd28a9f85b9c6ad57bd5bb1ae477bfe37846","datavalue":{"value":{"entity-type":"item","numeric-id":114337,"id":"Q114337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q923069$06136E1E-0E38-4A3D-8DC3-CA237DB8DBC2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"70d2fbf8bcd48a5ca1ac752985098b379d0dbb65","datavalue":{"value":{"time":"+1990-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q923069$D37A7CE4-1AD5-4BD9-8CC5-39059630F789","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"1fad3960bdbf61f27328a53aaa7719e409783486","datavalue":{"value":"The leftmost reduction strategy S of \\(\\lambda\\)-calculus (``call by name'') has many mathematical advantages: for example it always terminates when applied to a normalizable term. A practical advantage of S is that the argument of a function is evaluated only if it is really needed; on the negative side it will be evaluated each time it is used.    The author remedies to this drawback by means of ``storage operators'' (for each data type). A storage operator T, say for the integers, will be a term of pure \\(\\lambda\\)-calculus, with the property that: for each \\(\\lambda\\)-term \\(\\phi\\) and for each \\(\\nu\\) which is \\(\\beta\\)-equivalent to an integer there will be a reduced form \\(\\nu_ 0\\) of \\(\\nu\\) (not far from its normal form) such that the left computation of \\(T\\nu\\) f is equivalent (same length and same result) to the computation of \\(\\nu\\) to \\(\\nu_ 0\\) followed by the (left) computation of \\(\\phi \\nu_ 0\\). Thus, the call-by- value computation of \\(\\phi\\nu\\) will be simulated by the call-by-name computation of \\(T\\nu\\phi\\).    Let D[x] be a formula of second order functional arithmetic defining a data type D, and let \\(D^*[x]\\) be a G\u00f6del transform of D[x]. The main theorem of the paper states that any term T of \\(\\lambda\\)-calculus which encodes a 2nd order intuitionistic proof of the theorem \\(\\forall x(D[x]^*\\to \\neg \\neg D[x])\\) will be a storage operator. This solves the conjecture raised by the author [RAIRO, Inf. Th\u00e9or. Appl. 25, No.1, 67-84 (1991)] (with a slightly different definition of storage operators).    The logical framework (and type system) is the second order functional arithmetic, \\(AF_ 2\\), developed by the author in his book [Lambda- calcul, types et mod\u00e8les (1990; Zbl 0697.03004)], however the paper is self-contained. The conceptual part of the proof, which is also highly technical, relies on a simple version of G\u00f6del's translation and a systematic use of realisability in standard models of \\(AF_ 2\\).","type":"string"},"datatype":"string"},"type":"statement","id":"Q923069$93058F9E-10E0-4109-B779-9F28D6617FBE","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q923069$29BDCE35-71A0-4287-AD9E-786E0107D88D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q923069$F1AFF780-276A-4FE8-AD8B-9DA13F30597F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q923069$335304CE-26A5-4B06-99DD-F7FE2FAB9024","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"782a7a9863899bbb6ce9226e576bec9ced7b2421","datavalue":{"value":"4170867","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q923069$41C97A5E-F6F7-4E35-94B7-AEE1C12E965A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9704b0891f58c076ea782ddbe331fa1a648b3e29","datavalue":{"value":"leftmost reduction strategy","type":"string"},"datatype":"string"},"type":"statement","id":"Q923069$5E05B826-B3AE-47A1-AFCE-021DBF32D662","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e77f6b122613ab28ed1949959e76bf4107c78456","datavalue":{"value":"\\(\\lambda \\) -calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q923069$964277F9-C528-45DE-A868-1E4B99A62EB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4ca51a4f901a0386be4cacd8d75b35348c653605","datavalue":{"value":"call by name","type":"string"},"datatype":"string"},"type":"statement","id":"Q923069$C7156BF9-9A93-4CCE-B9E0-90D749373A75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8237243ac39caa3580f4136f84722538eb343898","datavalue":{"value":"storage operators","type":"string"},"datatype":"string"},"type":"statement","id":"Q923069$D30DF343-3CDE-4AAD-96E4-60EEF696089B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"08f76fc5023f120a176e50cb65f454d9592f5e85","datavalue":{"value":"second order functional arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q923069$1ADFCCBA-48F2-4B21-AC01-33A1C3A341C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a2444da0282f3c15bb118f9be04f6022ecaf9f9c","datavalue":{"value":"data type","type":"string"},"datatype":"string"},"type":"statement","id":"Q923069$97C36A92-6932-425C-BCB4-06C68292B387","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"cfea56292579072863c42a6e983fef653b45e536","datavalue":{"value":{"entity-type":"item","numeric-id":1391738,"id":"Q1391738"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q923069$51B5C9A2-8B55-4EBD-A74B-BAB693E19FEC","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q923069$14711490-1BA5-4CA4-8162-29816A22DB88","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"787e8787fc0800d23d78fddfd9bf35254e758553","datavalue":{"value":{"entity-type":"item","numeric-id":801050,"id":"Q801050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q923069$B714128C-6603-4F41-AD28-9746A29A2448","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16de9a4f8e129e311d9ce09ae9e120dd4a226b8b","datavalue":{"value":{"entity-type":"item","numeric-id":3997016,"id":"Q3997016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q923069$1F61DF9C-2784-4332-B0CD-18C77060D17C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"36b355c034a15b6951cab8a2fb9dd01fb3be3dbf","datavalue":{"value":{"entity-type":"item","numeric-id":3477935,"id":"Q3477935"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q923069$86A1C8C8-93A7-4864-8CA9-799975607DE0","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4db78fd63e4377c07a547e19509873ac907360e8","datavalue":{"value":{"entity-type":"item","numeric-id":1329740,"id":"Q1329740"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0f15cc495fa514ba4854c737933c8231435f64db","datavalue":{"value":{"amount":"+0.8785780668258667","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q923069$711F8DCA-CDD0-426B-A64E-6C0543BE94F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"25ccbecfbc626beea6f239547add4cea8fa0c237","datavalue":{"value":{"entity-type":"item","numeric-id":3142911,"id":"Q3142911"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"18736539059b1301becd1837d0a0ff50c203b5da","datavalue":{"value":{"amount":"+0.877196729183197","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q923069$2B575BC5-6845-4EFE-BC1E-326140648A93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"699488f7df6896abc88acf8fb7dfdd7df82dddbc","datavalue":{"value":{"entity-type":"item","numeric-id":4247307,"id":"Q4247307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"29df9b1aaed96036861df87898916cc3616d806e","datavalue":{"value":{"amount":"+0.8703373670578003","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q923069$20957644-64F7-4E2C-B44C-44796DA458E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"38e62f4678bc9c2e53e57e5da562a1836949c6a8","datavalue":{"value":{"entity-type":"item","numeric-id":1805408,"id":"Q1805408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bca7b00ed60a08e6f5eb48a99df4d55dc14748fe","datavalue":{"value":{"amount":"+0.8703371286392212","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q923069$797BED76-A625-4969-A604-0AC23458DF44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e49f1ced8d0bc003652f3e84c305d6b439ebf23a","datavalue":{"value":{"entity-type":"item","numeric-id":1382182,"id":"Q1382182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"541abf776e6bb1387cb2592c9e80cb6851931b5b","datavalue":{"value":{"amount":"+0.8381140232086182","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q923069$81E38B92-ED6D-40FF-8022-656982E3593B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:923069","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:923069"}}}}}