{"entities":{"Q2732290":{"pageid":2743029,"ns":120,"title":"Item:Q2732290","lastrevid":47645485,"modified":"2026-01-02T07:28:18Z","type":"item","id":"Q2732290","labels":{"en":{"language":"en","value":"\\(\\lambda\\mu\\)-calculus and B\u00f6hm's theorem"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1623530"}},"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":"Q2732290$03956A9F-E77A-468B-A1C0-1EC594983DE3","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8c09c4e965bb8317e5448d02e291c1ff0f33d302","datavalue":{"value":"0981.03019","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2732290$A769D40E-80FF-4587-87B4-4B9B7863EDBB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"13ab030f6527ed4de0e9d6670452029bc04c8df8","datavalue":{"value":"10.2307/2694930","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2732290$524FE731-057C-4B46-B9B8-EC70B043474A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"54a3bc5df956a97ae33fbb6dc0e5255680feccb7","datavalue":{"value":{"entity-type":"item","numeric-id":2732289,"id":"Q2732289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2732290$5D07B26D-98A1-46EA-853E-D5C73D65F06D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"520624d6eff845494b19bcfca76abb567dc10a8d","datavalue":{"value":{"entity-type":"item","numeric-id":6768204,"id":"Q6768204"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2732290$3523378E-7496-4C36-B400-D146F0D4ED5F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"eda994ce54674f95a066f6d30cc466b0f4ae3187","datavalue":{"value":{"time":"+2002-03-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2732290$26704A87-5F5E-4C75-9C28-FD84A33D0203","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2732290$A1DCD9AF-DA8A-48FB-8A82-FAD01A7303F5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"71a33b8736f8224ed6e03688996adc5199e175b8","datavalue":{"value":"1623530","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2732290$F8FB2FE4-CFE6-461F-A350-EFB2CB688554","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9b113f44078a5cd5c47f908b9ed301791a901ec9","datavalue":{"value":"lambda mu calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q2732290$1A818E94-5C96-4E8A-BA5F-CEDA4D24F3F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"895b0720feb5deefc72f77e5cc2a9fccfa2348c3","datavalue":{"value":"classical lambda calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q2732290$861F1554-924B-4F16-9006-C3AFA56B7489","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6413b877eae48c16ba966fd4b98a92f140b7e9ad","datavalue":{"value":"B\u00f6hm's theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q2732290$59AD1D07-D888-444B-8170-5E8B4091E7AE","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":"Q2732290$F5D5F86B-A5E0-4ACD-9B41-094A4E7E0E9F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8632bcf3d268bb2c6f4aa8b40677891c349b6a94","datavalue":{"value":"https://doi.org/10.2307/2694930","type":"string"},"datatype":"url"},"type":"statement","id":"Q2732290$3A85E7F7-B3BD-4A42-9707-7DE9EC84EA5C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"af5f5fac6b8f92c470da0df94cc2ec382a663cf6","datavalue":{"value":"W1995963173","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2732290$1BB8E393-A614-4B30-87D9-FE2058AF133C","rank":"normal"}],"P223":[{"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":"Q2732290$3B31029E-B4A4-4F96-BB23-45A6382BDFE2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"79982f7dcdf29f9d4c77c5e3c3812a45c09430e4","datavalue":{"value":{"text":"\\(\\lambda\\mu\\)-calculus and B\u00f6hm's theorem","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2732290$15AF3990-46D6-4A9F-A95F-836264046F9A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"cd9ebe56ec423ec5335930a0b1a45ca7ae3b5c0f","datavalue":{"value":{"entity-type":"item","numeric-id":6768298,"id":"Q6768298"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2732290$2FB7CD07-E5CA-43A9-8595-53645F28363F","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"e722261dace4ad92c940a7a14394db5bb001b144","datavalue":{"value":"A closed lambda term \\(M\\) is solvable if there exist \\(M_1, \\ldots ,M_n\\) such that \\(MM_1\\ldots M_n\\;\\beta\\)-reduces to \\(I\\). B\u00f6hm's Theorem states that for any two closed lambda terms \\(M\\) and \\(N\\), if for all \\(N_1, \\ldots ,N_k, \\;MN_1, \\ldots ,N_k\\) is solvable if and only if \\(NN_1, \\ldots ,N_k\\) is solvable, then \\(M\\) is \\(\\eta\\)-equal to \\(N\\). David and Py consider this theorem for Parigot's \\(\\lambda \\mu\\)-calculus, which is \\(\\lambda \\)-calculus extended using a \\(\\mu\\)-operator so that the types of the terms are classical \\(\\neg\\to\\) theorems. The \\(\\lambda \\mu\\)-calculus however is not Church-Rosser when \\((\\eta)\\) is included. This problem has been overcome by Py by including an additional reduction rule that restores the Church-Rosser property. In this paper David and Py find a counterexample to B\u00f6hm's Theorem with this form of reduction.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2732290$7A76AA98-EEC9-4FCC-BCBA-EDF90FA720EA","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":"Q2732290$1617382C-BACD-46A4-8E01-6D3A8A6F2444","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bdd4b62f5232d7b00f9e6dcf99cee3f622b6409c","datavalue":{"value":{"entity-type":"item","numeric-id":428894,"id":"Q428894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"22b4b921eea3385554adfacb9fa24c6b633da604","datavalue":{"value":{"amount":"+0.8796769976615906","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":"Q2732290$15DFB7B6-0A7B-4E96-97EA-E8CE8BB16D91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1405c8437cd0b11039779d32ca90754b67047c6f","datavalue":{"value":{"entity-type":"item","numeric-id":3558334,"id":"Q3558334"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"025b1f787a0e7762c2f3b8df6937dbe67428b222","datavalue":{"value":{"amount":"+0.8049514889717102","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":"Q2732290$35ED9D36-D8E4-4318-8CDE-67CFB933EB06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f1e43db8af2de792edfe496108214f7668b61ba4","datavalue":{"value":{"entity-type":"item","numeric-id":4992395,"id":"Q4992395"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"652d15dfd3cd327752d1a3f8daca59baea1df135","datavalue":{"value":{"amount":"+0.7601426243782043","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":"Q2732290$728E8DA2-A8B8-48F4-81D5-6EFAEB4C2A64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9a545bf4fac674b6da581a6e0cfb51aaac8fe4ba","datavalue":{"value":{"entity-type":"item","numeric-id":4625694,"id":"Q4625694"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f35bf92c1d6a4dda640dec08f4397cc0b5d4569f","datavalue":{"value":{"amount":"+0.7595012784004211","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":"Q2732290$3C2577CE-B6DB-4910-8BDD-5DB443B8F13A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0897f2bfb12099cb1bbec7eb650bd13e6d20c35e","datavalue":{"value":{"entity-type":"item","numeric-id":732057,"id":"Q732057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4cd02d2e6a6a25d02b806486745924087e155f06","datavalue":{"value":{"amount":"+0.7534260153770447","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":"Q2732290$2AA74055-6DA0-4993-9EAC-3EE140C224C3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2732290","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2732290"}}}}}