{"entities":{"Q792755":{"pageid":794603,"ns":120,"title":"Item:Q792755","lastrevid":64375812,"modified":"2026-04-11T19:26:42Z","type":"item","id":"Q792755","labels":{"en":{"language":"en","value":"The insensitivity theorem for nonreducing reflexive types"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3854408"}},"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":"Q792755$B1902C55-3E28-4374-A6D1-C4C85C10E9CE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d948d49080287f10523a5f9b38b0b7a65c901e7f","datavalue":{"value":{"text":"The insensitivity theorem for nonreducing reflexive types","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q792755$A92BC429-65A6-4FF7-B139-73E2D7C8B941","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"cca1a86f41f661754ca44d6fb09cc8f42c564c81","datavalue":{"value":"0537.68035","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q792755$03A99A3A-06DC-4D13-AB08-97D449FA226E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"fa30c4c8dc81bd11c37452adce00d339879ac189","datavalue":{"value":"10.1016/0022-0000(83)90049-1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q792755$4FD76374-AF6B-4E10-8D61-DEF7EDB1421A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"278d84a31aa4d41905d8d358c66cb65e85593d8f","datavalue":{"value":{"entity-type":"item","numeric-id":673182,"id":"Q673182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q792755$411719EB-D08F-4515-9BBB-4FB682A5F008","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7b97cf78de40b88a7d10e29595ef89d14c9040b2","datavalue":{"value":{"entity-type":"item","numeric-id":760417,"id":"Q760417"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q792755$372610F3-7C2A-40C8-A518-70450E516B1B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3340243f57e05f2265c56423c388055a14b114fa","datavalue":{"value":{"entity-type":"item","numeric-id":107189,"id":"Q107189"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q792755$FA147C30-B34F-4A93-AD77-43AB450087D2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0136733d5dd7d9f4d36f24c87a0b8375ae1cb2fd","datavalue":{"value":{"time":"+1983-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":"Q792755$3A80F2F2-CFC0-403D-9201-07D681C0F886","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"de4150ea86b6da901f0c5834b98fe75412101585","datavalue":{"value":"The paper is concerned to the problem of deciding which are the useful types for typed \\(\\lambda\\)-expression programming languages (ALGOL 68, LISP, etc.). In the first section the authors present the concept of reducing type and their hierarchies of finite and infinite types. In a previous paper by the authors [Lect. Notes Comput. Sci. 85, 38-50 (1980; Zbl 0444.68026)], they showed that the nonreducing types are useless for primitive functions of first order type and for terms having the same meaning if they behave in the same way in any program (fully abstract semantics). This result comes from a more general and stronger syntactic result, obtained in the present paper (Insensitivity Theorem): contexts of finite type and closed with respect to variables of reflexive type are insensitive to differences between terms of nonreducing type. Formally, the theorem is the following: if \\(M^ 1\\), \\(M^ 2\\) are two terms of the same nonreducing type, C[] a context for them and \\(C[M^ 1]\\), \\(C[M^ 2]\\) are i-closed terms of finite type, then \\(val(C[M^ 1])=val(C[M^ 2])\\) (val denoting the ''syntactic'' value of a term). A main consequence is that nonreducing types are useless within a fully abstract semantics. The third section illustrates the role played by the concept of reducing type in applicative language modelling. Semantics (defined by models) and full abstraction concepts are introduced and the insensitivity theorem related to a new programming languages design principle. Finally, hints about further researches on this topic are given.","type":"string"},"datatype":"string"},"type":"statement","id":"Q792755$3A9A66BE-C99B-4F94-8B32-3F13AACBEA25","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q792755$B126987C-495B-44FB-8618-10D0FA520DAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q792755$D8FAA964-3F59-4619-A828-710354D4D808","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"57eee2f313463199e20b9235bce5c88ea02d3389","datavalue":{"value":"03D65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q792755$E7866E58-CFD8-4242-8C90-8A76B7B99D97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q792755$450F8FF2-E44F-4B9E-BCE9-CFDCF4CF058D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3fca415580115e1e0a74c69afb3a7d85b0c01d8d","datavalue":{"value":"03D55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q792755$477D3A3F-E73C-4EE4-82C6-DCC656E4502C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q792755$565B0D81-CAF8-4E50-B205-E99538026157","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9565c312c227d0fea2047cb379b5cdf3b1bf1a49","datavalue":{"value":"3854408","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q792755$A6E1BF73-23B1-47EE-A182-CF5626678FAD","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"01f639a56e1e38a2490c4463ce011c878a3d36ab","datavalue":{"value":"typed lambda calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q792755$0D450D10-65AA-471E-8AFF-2DB553096F67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e852647b6f90075b0d33ce1524c43f82754c1a87","datavalue":{"value":"free continuous algebras","type":"string"},"datatype":"string"},"type":"statement","id":"Q792755$9EEC27CF-AA59-440D-9AA6-97FBFA5E918E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"489560b9b00c44572ad1e0eebe89cce928d6d1f3","datavalue":{"value":"programming languages","type":"string"},"datatype":"string"},"type":"statement","id":"Q792755$57D90652-9AA4-436E-BEC7-EAA3EDC7B616","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d7e7c3ba3d38c19995d7a81e51cf604876d5a12c","datavalue":{"value":"reducing type","type":"string"},"datatype":"string"},"type":"statement","id":"Q792755$5A2C9CFA-1866-444C-B721-1D3F7E6BEF19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7b5ef96e16ad04069a357ef6a98a2823c300d1c3","datavalue":{"value":"abstract semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q792755$AC5FD4D0-AEDE-4DDE-884E-AA2F03ED4166","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6ebbbc010b166d33c067912ff157802a0747eb51","datavalue":{"value":"applicative language modelling","type":"string"},"datatype":"string"},"type":"statement","id":"Q792755$0E3C0A1F-F943-43FD-A8C9-C12D12DED710","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"ddfe26001cac27b44f73ee317c958b41c5d4e225","datavalue":{"value":{"entity-type":"item","numeric-id":585901,"id":"Q585901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q792755$63B0C235-ED4B-485E-A7EA-EAE0871DB27F","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"49eaddd693f0d125ebcbba47522e5639803410e0","datavalue":{"value":{"entity-type":"item","numeric-id":13966,"id":"Q13966"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q792755$B7BA87F9-8FEA-40F0-8861-92763C6AE6AB","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":"Q792755$3DCBDC6E-3B59-4A29-8494-F1C8755506D7","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4e46dcc7d1f5136fbdeb0f6bd8135f158e1c04dd","datavalue":{"value":"https://doi.org/10.1016/0022-0000(83)90049-1","type":"string"},"datatype":"url"},"type":"statement","id":"Q792755$5033342F-DE88-4B28-B70F-75F86F0A8F45","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"199730f3da501bbab619d39c4fe1575440db329b","datavalue":{"value":"W2060254233","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q792755$3ED80A34-5E07-4E88-90CF-28887445EF19","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7c6eb8b3ed75272d1a222dfa4e01e662b05ef011","datavalue":{"value":{"entity-type":"item","numeric-id":4139647,"id":"Q4139647"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q792755$610A4ECF-9A82-420A-810E-F017764ED8B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"08027fefe3663593767227283a15ea83db36efae","datavalue":{"value":{"entity-type":"item","numeric-id":3888521,"id":"Q3888521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q792755$5370A921-96AB-4D4C-8549-F99E11403BE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"409164b0daaac9ded8013ee8c2bffaf560f4c1fc","datavalue":{"value":{"entity-type":"item","numeric-id":3954807,"id":"Q3954807"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q792755$CF2B732B-FED0-44FC-B47F-03D2E2B22146","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0065dc8b5c25773ef1d9719266c7992d0edd4dd5","datavalue":{"value":{"entity-type":"item","numeric-id":4131619,"id":"Q4131619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q792755$6A9689B7-541B-4396-BA53-B9FE8FFC6549","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"437e339c0f52b065b7629f93e04f820bac86e415","datavalue":{"value":{"entity-type":"item","numeric-id":4772711,"id":"Q4772711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q792755$F1B9ED2C-0EB3-48A1-97A8-0EECE49ED147","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c6fe3949a60e4535ad5a0b04a8726d37af9ca0c6","datavalue":{"value":{"entity-type":"item","numeric-id":1249567,"id":"Q1249567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q792755$A11E5D18-D3E3-4CC7-AE67-4C8E2DCF91FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9fde949ec0edc78cafc417dc0d661c3b24c05302","datavalue":{"value":{"entity-type":"item","numeric-id":4103509,"id":"Q4103509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q792755$81A93E32-44F4-44E8-B527-8653156BEBD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d13a074e10182485b0efcf5cf7cfc43a7672c7e","datavalue":{"value":{"entity-type":"item","numeric-id":4115133,"id":"Q4115133"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q792755$38632CA5-D3A7-43FB-B1DF-BBEA42361BEF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2837c5a7f7ede9e8d28d75d01e2a5d59c9368b1b","datavalue":{"value":{"entity-type":"item","numeric-id":3319765,"id":"Q3319765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6dbc78f3da5b5bea276b068cc822ee208aad01ab","datavalue":{"value":{"amount":"+0.8351803421974182","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":"Q792755$E195D4D1-D924-4DCF-91A9-4DBEE7DB8D19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dff7eb1bfcd308ef3f89391bd6d79d1ea9fce910","datavalue":{"value":{"entity-type":"item","numeric-id":3709890,"id":"Q3709890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a7d3ac2f77613c46e31e1be084ddba20b6016929","datavalue":{"value":{"amount":"+0.7110939621925354","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":"Q792755$D8DA6E23-3E94-42AD-BC21-317A5A602D85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"395a3be3ec7a1b2fef13f4186bc303ac5b1d182c","datavalue":{"value":{"entity-type":"item","numeric-id":3972839,"id":"Q3972839"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f643f3448b278eecdb26e258a235be3c9d7c43f9","datavalue":{"value":{"amount":"+0.7019239068031311","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":"Q792755$6B0F5E8F-0E46-4080-ACB1-C46E7AC18638","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d465d27195e9892d22a7f9681fc405b78c0dae16","datavalue":{"value":{"entity-type":"item","numeric-id":365669,"id":"Q365669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"00093c74d2e45d2610634afeadfa2593729a5d90","datavalue":{"value":{"amount":"+0.7005840539932251","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":"Q792755$ACC3EEB4-EB6E-4DA7-8CFD-8D865F86EBA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a0bc1f4262c020a297002138e11c4f957db4662a","datavalue":{"value":{"entity-type":"item","numeric-id":688729,"id":"Q688729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2e45abdb3e55aa5231329d53a88255eff7dcc68d","datavalue":{"value":{"amount":"+0.6966409087181091","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":"Q792755$7C672C94-5BDD-4DE5-ACFA-4C1B39B4172F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The insensitivity theorem for nonreducing reflexive types","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_insensitivity_theorem_for_nonreducing_reflexive_types"}}}}}