{"entities":{"Q1840460":{"pageid":1851202,"ns":120,"title":"Item:Q1840460","lastrevid":69318882,"modified":"2026-04-13T06:12:23Z","type":"item","id":"Q1840460","labels":{"en":{"language":"en","value":"Normalization without reducibility"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1562993"}},"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":"Q1840460$A6CC0534-B5C5-4ACA-8921-EECB6E32E6F8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"53e1c64b313dbb66e53f8e6022f5b152bbe03592","datavalue":{"value":{"text":"Normalization without reducibility","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1840460$B9353156-0739-4A6B-B54B-85792A186257","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"11f5d4630aff53a908c7d0bacf3c853149f8c7ad","datavalue":{"value":"0966.03015","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1840460$024945AF-E7F1-4E55-A094-D0E4AD36DC7B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8117b220ae7fc9123e4ed2e3b28674aa532d2b25","datavalue":{"value":"10.1016/S0168-0072(00)00030-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1840460$7CB1F57C-C267-489D-8984-4E5365D60CCE","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b8a2b41fc82fc820470803336cf6817ae0318cec","datavalue":{"value":{"entity-type":"item","numeric-id":172779,"id":"Q172779"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1840460$48F5ACEB-63FC-4598-9A58-149259C4D4B6","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":"Q1840460$0DCC4F2A-6B7E-4BDD-A0B5-D434DD3213C5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"01025e4e0db5ed45cddb918946199fe4c9ef64ac","datavalue":{"value":{"time":"+2001-07-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1840460$00762BF3-01D9-40D2-9B0D-F77DCADED3AA","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"a11b85fd71ca6d206e12c92df8dcd8ce4a2b41eb","datavalue":{"value":"This paper can be added to a long list of proofs for the well-known characterizations of -- strongly, weakly, head and weak head -- normalizing terms in the intersection type discipline. Motivated by the fact that Gallier has proven these characterizations in a uniform and semantical way, the author tries to use a syntactic method to prove them in a uniform way.    I wonder whether this proof is correct and hope the wrong statement of Lemma 18 part 1 was a distraction of the author. The bibliography of this paper does not contain references to all original proofs, for instance Pottinger's 1980 paper in the Curry Festschrift is missing [\\textit{G. Pottinger}, ``A type assignment for the strongly normalizable lambda terms'', in: J. P. Seldin et al. (eds.), To H. B. Curry: Essays on combinatory logic, lambda calculus and formalism, Academic Press, London etc., 561-578 (1980; Zbl 0469.03006)]. Moreover other papers that prove strong normalization along similar syntactic lines are not mentioned, like van \\textit{D. T. van Daalen}'s PhD thesis [The language theory of Automath, Techn. Hoegeschool Eindhoven (1980; Zbl 0422.68045)].","type":"string"},"datatype":"string"},"type":"statement","id":"Q1840460$B921A6E6-C8CC-49AA-99C6-340BC3B437CD","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"46e9cef7d36b7ae4173018bf7537ade343bbebe2","datavalue":{"value":{"entity-type":"item","numeric-id":1840459,"id":"Q1840459"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1840460$D51734D1-E9F6-47D3-BB67-E87A3208891F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1840460$58083DF2-1EB1-432B-8DD6-BF537C8F79CD","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5012774f13f3d408dd404c7958de0147a36dfd2f","datavalue":{"value":"1562993","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1840460$4C32B8DC-212C-4688-B56D-FC0CABC4BB34","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":"Q1840460$AE967F7A-7653-404A-AF4E-8FA5399B1DDB","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b13e2c7bf7641da29d842a6ebdecaddddf4b9405","datavalue":{"value":{"entity-type":"item","numeric-id":4222034,"id":"Q4222034"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1840460$71E545E8-CF33-4820-B1DE-8B48398E7865","rank":"normal"},{"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":"Q1840460$C7247C8F-2E6C-4207-B5AC-B5507CCD1684","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c20bbe48a9c127069b4af4be488bed62a03e970e","datavalue":{"value":{"entity-type":"item","numeric-id":3335753,"id":"Q3335753"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1840460$8AC2B653-2BFF-4F46-A769-9E16CAB64D46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e26c523496c35da0e6172865f48b61d150cadb9d","datavalue":{"value":{"entity-type":"item","numeric-id":3208623,"id":"Q3208623"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1840460$158266E9-4B19-4D13-B9E6-784D6C058E31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f434d785ed24cbcd005c3f7acdcb5c12ab96aa52","datavalue":{"value":{"entity-type":"item","numeric-id":3936713,"id":"Q3936713"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1840460$70DE0C84-78E6-4C62-ABC5-E34FF58D9F01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d610cd6a06b6c0401b04d6f90b219240e708af6","datavalue":{"value":{"entity-type":"item","numeric-id":4850465,"id":"Q4850465"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1840460$15E96C50-3AFD-46B0-9E6C-821D73CF36C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e4ba94d8f08c32063f0ed58d67ccdb0c07368fd","datavalue":{"value":{"entity-type":"item","numeric-id":1295368,"id":"Q1295368"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1840460$6C7D3910-85E1-4F5A-A8FA-B83827324B0E","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":"Q1840460$4C1939BC-764A-475D-9145-B7B2ECFF0262","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9f2f195c49df82c9cda56f240abd57e5287f8348","datavalue":{"value":{"entity-type":"item","numeric-id":1819575,"id":"Q1819575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1840460$CD350941-8546-43D6-B546-5CA1B131D3E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"651f3e68212cf82e01b75ca21e84f0e708df24c6","datavalue":{"value":{"entity-type":"item","numeric-id":1193654,"id":"Q1193654"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1840460$E6CBC875-B7F8-4DDC-8E3F-A33F24AD2411","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"ad419c7c281748559306259b5042c1082ed65763","datavalue":{"value":"Q126382660","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1840460$40F02B7B-E774-455F-BF62-B56837E385FC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"db2342ed2c626049bdf31040ee77033b181e8e71","datavalue":{"value":{"entity-type":"item","numeric-id":4457448,"id":"Q4457448"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"06cb8a6c6de605756d8ef075d6a54deac2604e4e","datavalue":{"value":{"amount":"+0.7989673614501953","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":"Q1840460$080DBAF0-78DC-4A3F-82BE-A5456ABF951D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8627593d274c87dfc4fb4d4324791736791db2b2","datavalue":{"value":{"entity-type":"item","numeric-id":1407502,"id":"Q1407502"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b69527db21affa4af57c7d07383bf9cb6c4cdb10","datavalue":{"value":{"amount":"+0.7844506502151489","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":"Q1840460$A43AA5FD-2E22-4CE6-94F5-51A736547583","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0a566b1d6a70d6aeb478a7fbe2b2db3c381d5fcb","datavalue":{"value":{"entity-type":"item","numeric-id":1924327,"id":"Q1924327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f9bb298344a67da4f5e158c8d33434eb3de2957a","datavalue":{"value":{"amount":"+0.7821266055107117","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":"Q1840460$0387E867-90D4-49CE-A3ED-A9C6501947AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2e530fe84338be83e5e1218a266af0666559ac65","datavalue":{"value":{"entity-type":"item","numeric-id":930869,"id":"Q930869"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c2ac15176558102ac9674df274488f8fa22fa7a3","datavalue":{"value":{"amount":"+0.7748050093650818","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":"Q1840460$BAB97A29-4D2E-4864-8242-536B43B1914D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"26a1e95e103b48b2ec9f98a8e4b8a2be4e2bde0b","datavalue":{"value":{"entity-type":"item","numeric-id":3599163,"id":"Q3599163"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bdd7a196322d8d249853833fab13deaebbcab6a6","datavalue":{"value":{"amount":"+0.7662267088890076","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":"Q1840460$3CFABE14-EF51-4D94-B54D-C85BC17716B5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Normalization without reducibility","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Normalization_without_reducibility"}}}}}