{"entities":{"Q732057":{"pageid":733906,"ns":120,"title":"Item:Q732057","lastrevid":63953109,"modified":"2026-04-11T16:39:44Z","type":"item","id":"Q732057","labels":{"en":{"language":"en","value":"A completeness result for the simply typed \\(\\lambda \\mu \\)-calculus"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5612546"}},"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":"Q732057$47F29EEB-A9C7-46CD-89B2-19F60DB5D211","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2851ebffa3f8e7449a4c763d35547f5353416cde","datavalue":{"value":{"text":"A completeness result for the simply typed \\(\\lambda \\mu \\)-calculus","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q732057$90048335-FFAC-4A0D-BC2F-D2739CC37CFC","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"62ce0d0390cc9fcc11a32decde2fa49b364dc638","datavalue":{"value":"1184.03007","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q732057$850C00C3-97DB-4195-B638-2ADF70DBAAF3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"03475eec65c2e868e184cfa393bdf90d107cae1e","datavalue":{"value":{"entity-type":"item","numeric-id":636352,"id":"Q636352"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q732057$658E5798-2A3F-42BE-AACA-D4E2004A85C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"87d98715daff21d7c75f3cdd719e2cf7258168bd","datavalue":{"value":{"entity-type":"item","numeric-id":732056,"id":"Q732056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q732057$EA0FC6D7-E522-4180-A93C-9A145EAF149A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q732057$21F07F43-1CE0-4870-A78A-BB4CC78BD4B1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"eca99fd9b1fdaf08a8ea0b1d2ea2e0c66a9f63c5","datavalue":{"value":{"time":"+2009-10-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q732057$53853E59-CBA4-415C-8652-D157CC9091B2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"30556299352e0b662ef0e737b8dc4007ae0aad7e","datavalue":{"value":"https://arxiv.org/abs/0905.0357","type":"string"},"datatype":"url"},"type":"statement","id":"Q732057$8FFCDAAC-38AB-48AF-BB6C-7BF351A684BF","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"73464342a8cacd8912277ba5fbba585730660634","datavalue":{"value":"The terms of the \\(\\lambda\\)-\\(\\mu\\)-calculus represent the proofs of theorems of classical implicational logic, which are types of these theorems, just as terms of the \\(\\lambda\\)-calculus represent proofs of their types which are theorems of intuitionistic implicational logic. In this paper, a realizability semantics is defined for the simply typed \\(\\lambda\\)-\\(\\mu\\)-calculus. This semantics is shown to be complete using a term model. In addition, for a term \\(e\\) of type \\(\\bot \\to X\\) or \\(((X \\to \\bot)\\to X)\\to X\\), the terms to which \\((\\dots((e x) y_1) \\dots y_n)\\) can reduce are found.","type":"string"},"datatype":"string"},"type":"statement","id":"Q732057$7E71BE4F-A1B5-496D-94F3-C0553CCFC566","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q732057$0A0978BC-E88A-433A-ADAB-614A83F1D3AC","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8b796be16a778a12e0e4f31375db10a83e324c88","datavalue":{"value":"5612546","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q732057$0ABF5483-C1FC-4B4F-A81E-1B2FD78FB04C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21e155ad1afa97824fdc6a44e26419a14d6aacc4","datavalue":{"value":"\\(\\lambda\\)-\\(\\mu\\)-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q732057$CB26A0C7-A3E0-4268-A6B3-B82B8A3A5DA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"988845729c3f4963366b1812ce9b6d4f9a29cc1b","datavalue":{"value":"realizability semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q732057$D11B4189-44C2-4EE4-8F35-360175F4A7E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f6816fdf79dd11ac09d9af4886c02baab03d2cf9","datavalue":{"value":"completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q732057$8E6C2136-F149-4732-80E4-C29796109A8A","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"376f136d3715d0668145bfef82b652dbeb24818d","datavalue":{"value":{"entity-type":"item","numeric-id":591019,"id":"Q591019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q732057$D4BFD1BC-92D8-4BC2-A6B9-E02D212345A7","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":"Q732057$661A5B57-C1EF-4A35-BB88-9DBF3EC7F28C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a5999f243e7275805ce84e301f6e81a63eea185d","datavalue":{"value":"W2963332220","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q732057$9EA40A6D-DF9F-47C2-84CE-D2DE6905A6F7","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"e1d50e7abfb3baf92eefbc7accf694fe29ae84ec","datavalue":{"value":{"entity-type":"item","numeric-id":5704003,"id":"Q5704003"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q732057$8E4E973F-591A-4529-8C05-80081C61A6FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a549f38ef99bfd672336f5501bd0f7f91ebe41d4","datavalue":{"value":{"entity-type":"item","numeric-id":4219570,"id":"Q4219570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q732057$A1987FA6-FDA6-4278-B2A8-7A65892FEF76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f13839e2eb1c1841ca6e6b07eb6f9393aaa84307","datavalue":{"value":{"entity-type":"item","numeric-id":4389762,"id":"Q4389762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q732057$FDB1E4EB-BA1B-4B98-AEF2-2C2F4F525AF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1650ec8986b79af49285234bcb3522e3340bd0b6","datavalue":{"value":{"entity-type":"item","numeric-id":3659755,"id":"Q3659755"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q732057$D49E4F72-2579-4BB4-9831-7E2D3353D7FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"706432819f6cf16b1a37d307080a71755ef9cfa7","datavalue":{"value":{"entity-type":"item","numeric-id":1839242,"id":"Q1839242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q732057$E9AD67B6-60B2-4891-97EF-0259B64E070F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c81ed1099943aeaeb1f4554d61ae2b7ae45129bd","datavalue":{"value":{"entity-type":"item","numeric-id":1839243,"id":"Q1839243"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q732057$7AF8B479-2C6B-40AB-9A87-37FAE1A5A97B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"01da1bbce82eb5f7f12b1d56e350ecb7ece50044","datavalue":{"value":{"entity-type":"item","numeric-id":882122,"id":"Q882122"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q732057$A2A0AB0C-72EF-4D97-A8DC-081C71811304","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":"Q732057$083CC312-D74B-4EC6-A844-F52B644BDAF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f7a3c34acdb0c6e70dbc14ab49bf7dd099b73494","datavalue":{"value":{"entity-type":"item","numeric-id":2851691,"id":"Q2851691"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q732057$630CB920-8C98-4207-999D-F45FA9D2C90B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"59511f92b4ab9425968b27555d8e7c4076935b63","datavalue":{"value":{"entity-type":"item","numeric-id":818927,"id":"Q818927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q732057$B6A1BB77-690E-406D-950C-1EEC597C908B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d2b448f94d79046d6183590aae96b7cfc591a0e4","datavalue":{"value":{"entity-type":"item","numeric-id":4717043,"id":"Q4717043"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q732057$5FCFDB3C-7C39-4510-B654-0582E41990EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"accd841049d6141a29dc0f203781fb03555bee48","datavalue":{"value":{"entity-type":"item","numeric-id":1570018,"id":"Q1570018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q732057$BAFD8007-5C8F-4653-8AE5-F22BD78D0843","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66257d76632b86525de5e8f5c47c6c6cf781ec1c","datavalue":{"value":{"entity-type":"item","numeric-id":4255509,"id":"Q4255509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q732057$F4095ADA-1643-48B6-8E33-7B88A639368C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bcaeb1c8d7f99e6d943db19cd7dab3c23ba7a3ca","datavalue":{"value":{"entity-type":"item","numeric-id":4382485,"id":"Q4382485"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q732057$79FE4A48-FBF2-443C-8A1F-31419C124BB0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"85768435e5ecf52554bf827f08d37984f548f753","datavalue":{"value":"10.1016/J.APAL.2008.10.012","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q732057$5066B23E-9591-47F6-B05D-7E7D66E3ED59","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"84d370cb7a5808a18e52a6a7ca186bdf3791cc9b","datavalue":{"value":{"entity-type":"item","numeric-id":5367052,"id":"Q5367052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c490daa10bbac10fea38d0925dfa709e2339801f","datavalue":{"value":{"amount":"+0.926491379737854","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":"Q732057$F165ADED-8020-4FEB-B3DB-7DB5AEC7B4F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c819cb150c4d225104efe1d97603db6a7cd0f4a9","datavalue":{"value":{"entity-type":"item","numeric-id":4964690,"id":"Q4964690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e9aa3f577c52cca24691ad0062dbc95ff2b14c65","datavalue":{"value":{"amount":"+0.8077122569084167","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":"Q732057$B9F7ED23-E19A-48D2-B401-DD68A30B1BB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2fb2c7584c950390b4f341a0d6d5b183ce416010","datavalue":{"value":{"entity-type":"item","numeric-id":2506496,"id":"Q2506496"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8f38f76ebb1b11a35a5b8a76255f9d8fdaab41cf","datavalue":{"value":{"amount":"+0.7947326898574829","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":"Q732057$3799562A-0926-4559-B374-7D628801D2C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cdb04cffa79c10b94b46f43c3aaf14e7c6a69a84","datavalue":{"value":{"entity-type":"item","numeric-id":3024853,"id":"Q3024853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bd8dc59f81966504b1ad6818c6a9ea498baee1b8","datavalue":{"value":{"amount":"+0.7915213108062744","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":"Q732057$BB1FAB62-F245-4CB4-B767-F32BD76BBDAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1e268013a2b619b7c21b2276357366cf3ebb236c","datavalue":{"value":{"entity-type":"item","numeric-id":4218109,"id":"Q4218109"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"29013ab6b5e08c178cf3db90e7d735f4dfcf2815","datavalue":{"value":{"amount":"+0.7858182787895203","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":"Q732057$0C11CDC6-7ED5-482F-A56D-A6B2AFD2C152","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A completeness result for the simply typed \\(\\lambda \\mu \\)-calculus","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_completeness_result_for_the_simply_typed_%5C(%5Clambda_%5Cmu_%5C)-calculus"}}}}}