{"entities":{"Q1337495":{"pageid":1348234,"ns":120,"title":"Item:Q1337495","lastrevid":67615878,"modified":"2026-04-12T19:02:46Z","type":"item","id":"Q1337495","labels":{"en":{"language":"en","value":"Interpreting higher computations as types with totality"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 682649"}},"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":"Q1337495$5BC2843F-C599-4BA9-BACC-5C923AFA2FD2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"67cf56653e855731967117fbc81283da9c603067","datavalue":{"value":{"text":"Interpreting higher computations as types with totality","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1337495$4637C83B-3233-4C02-A85C-1E119F507107","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2720ca1f980d6f600da06c35c2c8b096656eb6d3","datavalue":{"value":"0830.03019","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1337495$777F7A2D-4DDF-4028-8B4D-72CC104C1399","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f3435b045e334c5092c3fc87f0a8e0e022b59886","datavalue":{"value":"10.1007/BF01270624","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1337495$08271E81-D66B-4F6B-B264-AB9B8B764BC1","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":"Q1337495$466D10D2-7BF9-41FA-8569-19552710637D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"32d1d77beb5f3bc65c221a38015efeb024af2386","datavalue":{"value":{"time":"+1994-11-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1337495$A7A0FF82-5E8F-4D4E-A4E2-4B9B4993D2CF","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"e8bd225f87bfeba7d94bf8df9c88199d0191a9e4","datavalue":{"value":"The paper may be seen as a foundational study on the notion of totality, using Girard's qualitative domains as a tool. The starting observation is that in qualitative domains there is no ``intrinsic'' way to refer to total objects. Hence, the authors add more structure to qualitative domains, defining (partial) \\(E\\)-structures and totality domains, where a certain subset of total elements is selected (interestingly, these total elements are not in general the maximal elements of the domain). Each of these new classes of structures is proved closed under products \\(\\Pi (x\\in X)Y_x\\) indexed by stable parameterization. The principal object of study is now introduced by a monotone inductive definition: a hierarchy of totality domains and of names for them, where new structures are obtained via stable parameterization. The main theorem of the paper, proved by the so-called mollification method, is that the complexity of the hierarchy definition is equivalent to recursion in Kleene's \\({}^3 E\\) functional.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1337495$46A42E0F-2DB1-46D8-8F6C-E53BF419114A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"57eee2f313463199e20b9235bce5c88ea02d3389","datavalue":{"value":"03D65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1337495$FB15C920-2664-4241-A983-DB6EE45AE2D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1337495$BD7DD5B4-F2B3-422B-A7D5-B6F21CCAE673","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a7dde57cbaf704d564d8f981ca98d6340e3d4aaf","datavalue":{"value":"68Q05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1337495$60E9A581-F44D-49A1-9C68-C896B7FEA7D7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5ffb442a905688081850a473457c5fd8818663d9","datavalue":{"value":"682649","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1337495$9F9D7B82-AD10-4AFF-A20B-6862DBAC7914","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"18d1b7a2c28e77906da4104fb636290a5dcfcc3d","datavalue":{"value":"recursive functionals","type":"string"},"datatype":"string"},"type":"statement","id":"Q1337495$7FC7C2C3-CBC0-4252-BAC1-A6514FF803CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f9f10c41064384fcf055f75530010cda63ebbc1a","datavalue":{"value":"qualitative domains","type":"string"},"datatype":"string"},"type":"statement","id":"Q1337495$45ADA216-6B33-4769-A2F0-6DDC8FC5F61F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e295e270e8c365f0bff79d4f820f96ca6e9c71b5","datavalue":{"value":"totality domains","type":"string"},"datatype":"string"},"type":"statement","id":"Q1337495$A8D92C14-9C6D-47F2-BA57-294287606102","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6262b9451636d32609cdcfea42efa7f758fdb2fb","datavalue":{"value":"mollification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1337495$D6B5A238-B585-491E-8EDD-C3DCCC02C020","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3e7502148509557576dd7d15218a1a612c5e1fbb","datavalue":{"value":{"entity-type":"item","numeric-id":1374673,"id":"Q1374673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337495$C7103CC3-8A75-4A40-8DD8-A8469DAED8F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"23e2194cbd076f554310c20043be5c70c039c27e","datavalue":{"value":{"entity-type":"item","numeric-id":1063590,"id":"Q1063590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337495$7BE028A4-C712-43B6-B113-2539C0E5EAC2","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"00ea4a5ed8879c1a6adc0802c8c4ce48d27b9055","datavalue":{"value":{"entity-type":"item","numeric-id":596036,"id":"Q596036"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337495$09E89AAD-AC1E-45BB-A4A0-5246537BDAD3","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":"Q1337495$7E3A9F6A-4F94-4115-A666-A2258B02AF84","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c3319f248092bb0f68b64ff1019d98d12cacb759","datavalue":{"value":{"entity-type":"item","numeric-id":1210138,"id":"Q1210138"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337495$B9292C6C-67D9-4085-8EB4-E41B45667665","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b17989129559e41cfb06edc0b79311d4fa6022df","datavalue":{"value":{"entity-type":"item","numeric-id":3960844,"id":"Q3960844"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337495$E39F87F3-33A5-41FB-82B3-401EBC9E0D45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22ee85ee408ceb2acfb30c438cac3496a36c4200","datavalue":{"value":{"entity-type":"item","numeric-id":1091379,"id":"Q1091379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337495$CB48A6A1-B99F-466F-811C-4661AB43D9E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"690eac6707df294089bbb4811045c174c4de9fef","datavalue":{"value":{"entity-type":"item","numeric-id":3260568,"id":"Q3260568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337495$AC276C34-7ED8-4D29-9855-F40D3EF8339F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a91b42d0abf471d5779088ab76257caef8bd226","datavalue":{"value":{"entity-type":"item","numeric-id":1374674,"id":"Q1374674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337495$EA43E845-83EC-4B15-9653-ECE6FF8D6247","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df236345f891889a483c60bd0a6e60c9f72c1317","datavalue":{"value":{"entity-type":"item","numeric-id":4694213,"id":"Q4694213"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337495$161EE7D7-3674-4750-8E7E-6A02A440C309","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a11a39f5732ffdb54b8de3eb7976a129c5a21eb2","datavalue":{"value":"https://doi.org/10.1007/bf01270624","type":"string"},"datatype":"url"},"type":"statement","id":"Q1337495$E5A507D2-0A6B-472A-A0FD-5EADB806106B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e501fae4a9175bf9e2a2797e5a4a08a1970c7d98","datavalue":{"value":"W1965724811","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1337495$EEA4EC7E-05DA-47DC-8A16-244DEDFCA46F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2c98732784dbc0818d9328bdc4d52c6759bacd25","datavalue":{"value":{"entity-type":"item","numeric-id":3750112,"id":"Q3750112"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2e83bcb7e66c3265cc85403846268c65ce85fbf6","datavalue":{"value":{"amount":"+0.91767573","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1337495$E1934963-4DD5-4CA8-9F0D-AE2D74F8F659","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"64ee28c935680583520f591a20d7c0f057ae42e5","datavalue":{"value":{"entity-type":"item","numeric-id":5370902,"id":"Q5370902"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"565f3b10c374b4db39088e38f4f8a41c32a2e52e","datavalue":{"value":{"amount":"+0.90905946","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1337495$3CE9EAFB-C5F2-4916-9A01-3E61EA114F04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0627095eea66db634fda4421e1e92d7c3f8e791c","datavalue":{"value":{"entity-type":"item","numeric-id":1192333,"id":"Q1192333"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"56e305dd49c2a9d41ab92defed511fecb99ccf6a","datavalue":{"value":{"amount":"+0.9023791","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1337495$6E051871-BA46-436C-8448-3E00F457577B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e001309006a43b2c682ba66be212a39e7be2b26a","datavalue":{"value":{"entity-type":"item","numeric-id":4958656,"id":"Q4958656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f8f32d6d5f97a38485ff893a99150d22164c9e04","datavalue":{"value":{"amount":"+0.8995878","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1337495$8ACD7BAA-0F61-4956-B4B5-05CA091EF074","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"696d83aaec159cdf8ddedd031545e8cc3910de03","datavalue":{"value":{"entity-type":"item","numeric-id":4247306,"id":"Q4247306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7ca2fa7467876fe5ff72597208df13d3f2a6f312","datavalue":{"value":{"amount":"+0.8978195","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1337495$E217ED9C-A236-4DFD-BE0F-4F716B126B45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a7905963af015b44505496ce809c13a1a6c52306","datavalue":{"value":{"entity-type":"item","numeric-id":4348037,"id":"Q4348037"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6bbfe7f959c187203ddc9b3b294f426415e7d294","datavalue":{"value":{"amount":"+0.89690846","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1337495$6E173165-209C-4E9F-9E9E-38E927B7E3FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8f40e82af06ee6bc50270ec0b438a0d53a271fd7","datavalue":{"value":{"entity-type":"item","numeric-id":579245,"id":"Q579245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2765fb0cd58d6c2d024a9ab1022c2249eb1618bb","datavalue":{"value":{"amount":"+0.89677644","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1337495$9AA93599-F241-4D1A-ACE4-306EE27E06E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"20add77e9ee835adb27f7fc2c4363bcf5c28c8b7","datavalue":{"value":{"entity-type":"item","numeric-id":1283126,"id":"Q1283126"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b801f2986449be3e46a0bd9642207a3ff89bf6d4","datavalue":{"value":{"amount":"+0.8936317","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1337495$3AB4C629-7BF5-4DCE-9DF2-EC46CFF7ECC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a83ca2aa00dcd1b7a31acb549bc5e6b0114a83ec","datavalue":{"value":{"entity-type":"item","numeric-id":5718672,"id":"Q5718672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6ddca0d0461cc486217fb306aa31760052c4b69a","datavalue":{"value":{"amount":"+0.8929868","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1337495$0A5D0889-20CA-41B9-A26D-BE7C5C9D8C62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"92f8863c0ad8f47e8885016b775f423134b8191f","datavalue":{"value":{"entity-type":"item","numeric-id":6064279,"id":"Q6064279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"38c26b33d1c6e71698ff83d2fab79bdf2dc361b3","datavalue":{"value":{"amount":"+0.8927389","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1337495$DE5CBEEA-9E9B-48FD-9605-8FA6CB595AB2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Interpreting higher computations as types with totality","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Interpreting_higher_computations_as_types_with_totality"}}}}}