{"entities":{"Q1119620":{"pageid":1130369,"ns":120,"title":"Item:Q1119620","lastrevid":66168831,"modified":"2026-04-12T08:00:21Z","type":"item","id":"Q1119620","labels":{"en":{"language":"en","value":"BCK-combinators and linear \\(\\lambda\\)-terms have types"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4097341"}},"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":"Q1119620$FEF98CE2-8E63-4CCF-8C75-58514E91FB6A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bd54f8ac7f9d266eeabc7c3aa554dd3d076b382c","datavalue":{"value":{"text":"BCK-combinators and linear \\(\\lambda\\)-terms have types","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1119620$76BFD05E-1B08-45FC-85D2-DC9757BC5909","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a2c63c44e2e8cc57ab6b23fa063b1a034b0eeb84","datavalue":{"value":"0671.03010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1119620$D8D56DAC-4405-444F-BB4C-FFD6FC2FD55D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5ae266c0bc066c79252d96276c86efdae4600b81","datavalue":{"value":"10.1016/0304-3975(89)90100-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1119620$A99D2ACD-D35A-4335-A6DD-2676502F0742","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4715195926e2963dd021320bc2ac15ee05ecc606","datavalue":{"value":{"entity-type":"item","numeric-id":787127,"id":"Q787127"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1119620$7B46CE8D-85BA-4A0C-93B8-722D0A412E01","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1119620$66D8D946-8338-488C-8A8F-E24CB36E8965","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7211ad5ca16eb0d22cd0051fff3d0f3af254ceb6","datavalue":{"value":{"time":"+1989-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":"Q1119620$5767F459-81D5-4A98-9DDC-95B70A9FBB53","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"bdd39d8317794cb42eb1c86fe2291d89da6a5c9a","datavalue":{"value":"The main theorem of this paper proves that every linear \\(\\lambda\\)-term and, equivalently, that every BCK-combinator, has a type. This result, for BCK-combinators, was first stated as Theorem 1 by \\textit{R. K. Meyer} and the reviewer [Logique Anal., Nouv. S\u00e9r. 28, 33-40 (1985; Zbl 0574.03004)], but the proof, based on an induction on the ``level'' of a combinator, does not show that this level is defined for all BCK combinators. (The reviewer has since overcome this problem by a combinator based method.) The present paper translates the combinators into linear \\(\\lambda\\)-terms, for which the induction becomes simply one on length.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1119620$B1A2235C-DA5A-4E16-BA18-415E2EEBCD27","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1119620$0A139103-F2FF-4DA4-82DD-3653B5C2B829","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b8d9ce4b2b0431ca189c40198a66934f642b7bec","datavalue":{"value":"4097341","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1119620$D0F99238-0E7C-402B-AC54-D3E9546E736C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"485447b25ea9ae3ba0e28b66b16f57c15b7c1fe1","datavalue":{"value":"types","type":"string"},"datatype":"string"},"type":"statement","id":"Q1119620$FA1D0EC0-7500-4000-8F3D-C56652ED697B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"07037d387d955549982bb1de17ff82509f742adb","datavalue":{"value":"linear \\(\\lambda\\)-term","type":"string"},"datatype":"string"},"type":"statement","id":"Q1119620$12869F71-1F5C-4E6F-8033-5781D2E72ABB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7338e9b43e68dd7ea95b4dfd344613b7ebcacd2a","datavalue":{"value":"BCK-combinator","type":"string"},"datatype":"string"},"type":"statement","id":"Q1119620$28B2EA08-C1A2-4CCF-AFEF-87F7413B029E","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":"Q1119620$C4A63355-1515-4890-ADE9-A7B403328512","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":"Q1119620$DAFCAC7F-C7C2-4F07-B8AC-1763610485E3","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"e000333dcb543c2ada64aaed9439f85a806e7ef7","datavalue":{"value":{"entity-type":"item","numeric-id":3691634,"id":"Q3691634"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1119620$38B9C399-1253-4990-926E-24339D7FEEA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ccc272df6e3f638456d722d8f630056eceb056f","datavalue":{"value":{"entity-type":"item","numeric-id":5565113,"id":"Q5565113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1119620$FA34EC88-579A-45FB-A549-ECBB78B86D20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a2b2a8cf71a298beb3d5742fd0312db85012cf7","datavalue":{"value":{"entity-type":"item","numeric-id":579249,"id":"Q579249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1119620$6AA1058B-7570-456D-B2DE-140350BD21FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e8da94acaf95b26157aa8db77f1b3b250a394510","datavalue":{"value":{"entity-type":"item","numeric-id":4133942,"id":"Q4133942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1119620$88DEE92C-519C-47F4-A3B5-66A3827817E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f23417d0146cdc8808662ea4f0b0496e878f3547","datavalue":{"value":{"entity-type":"item","numeric-id":4722037,"id":"Q4722037"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1119620$B074DE3B-8D68-4A15-9859-771BC5EC1C7C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ded42d2371032539de0bbfa3b5f991fc637501d1","datavalue":{"value":"https://doi.org/10.1016/0304-3975(89)90100-x","type":"string"},"datatype":"url"},"type":"statement","id":"Q1119620$9BE6A3F4-BECC-42FF-ACDA-A9C3979FFA36","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"74ad535b9dc2b084df991a9576a626e48e522d4e","datavalue":{"value":"W1968532969","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1119620$D92DC57A-D840-41E0-8C0F-DD01A4DAA2F7","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b497a8ef1b8892322ad4f3a47610623f41a8ecd8","datavalue":{"value":{"entity-type":"item","numeric-id":1208417,"id":"Q1208417"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5a977cacf16b769d4056ad8b8e7f2ccde89a5c28","datavalue":{"value":{"amount":"+0.7984055876731873","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":"Q1119620$329FF8BB-E340-4A32-B36D-CF3B88C20852","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"78942b7ea60679f671a1298841ec7c566a704356","datavalue":{"value":{"entity-type":"item","numeric-id":3149663,"id":"Q3149663"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7e97384d8273d5b27508cf2feac7399b4d5a52d4","datavalue":{"value":{"amount":"+0.7961110472679138","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":"Q1119620$A363EFBD-CF80-47FE-AEEF-73348D08E2E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"16665f0c114d570f50b8a5afc346f37e39e5ecdb","datavalue":{"value":{"entity-type":"item","numeric-id":1583260,"id":"Q1583260"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2768ac745cdbdf33e9aac7dd4637ee59ee8b9e71","datavalue":{"value":{"amount":"+0.7960466146469116","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":"Q1119620$9171AD87-FEA8-4D31-B700-FA1583B2424C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"df7715d37aa83c72d0cc85449b40f0f2827adb54","datavalue":{"value":{"entity-type":"item","numeric-id":3352995,"id":"Q3352995"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"63535d70578b8c429f73136ee120d8ec93264ad6","datavalue":{"value":{"amount":"+0.7886888980865479","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":"Q1119620$98C87AA1-E123-49B4-A680-9728CCE28CBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8d38b991e3288c0f24981013a02fb25fd23630f7","datavalue":{"value":{"entity-type":"item","numeric-id":3612657,"id":"Q3612657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"571da8c7ae36574550fd29407494fa586324eb33","datavalue":{"value":{"amount":"+0.764324426651001","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":"Q1119620$34815930-3ABE-412B-80C6-C88A8F971BC8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"BCK-combinators and linear \\(\\lambda\\)-terms have types","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/BCK-combinators_and_linear_%5C(%5Clambda%5C)-terms_have_types"}}}}}