{"entities":{"Q1314360":{"pageid":1325110,"ns":120,"title":"Item:Q1314360","lastrevid":46301520,"modified":"2025-12-24T12:55:41Z","type":"item","id":"Q1314360","labels":{"en":{"language":"en","value":"The genericity theorem and parametricity in the polymorphic \\(\\lambda\\)- calculus"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 501173"}},"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":"Q1314360$2FF4CA7F-EA35-4789-84E4-9584BE28FC71","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f311bd3e7078fd96d63ef268a47f6b9b29a941a2","datavalue":{"value":{"text":"The genericity theorem and parametricity in the polymorphic \\(\\lambda\\)- calculus","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1314360$BA68A67D-2561-48AB-A08E-B926748F2887","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4a7df5c244125c4a2d04f91905a90358d9459d74","datavalue":{"value":"0793.03008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1314360$C36033B1-B496-4833-A403-FE5BF43FE701","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8d1f184f55bbb6e6c0200fb0680f5767dc0a24db","datavalue":{"value":"10.1016/0304-3975(93)90093-9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1314360$BB3ECB30-E702-4B43-B553-C3B50B110B11","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d696672123bc34b920816efa7ac95e985dce1194","datavalue":{"value":{"entity-type":"item","numeric-id":1314358,"id":"Q1314358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$B0993EAD-CB9C-4160-9A47-CD9E663295AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9b243572f25465f3ae7a32f2d3b06ae2073b8520","datavalue":{"value":{"entity-type":"item","numeric-id":590478,"id":"Q590478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$172A0ECF-5A1F-4D4C-8F7A-D1AFA2B90DC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"03c3b74ff26c086a7988af4846b84322637129ef","datavalue":{"value":{"entity-type":"item","numeric-id":1868461,"id":"Q1868461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$19898DAA-81F6-4DCA-8226-E472CB578E6F","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":"Q1314360$8D5FBFF6-FA83-433A-848A-D1336D66AFC4","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"297502fa3af7a8f9b84cb38ff3ab4793fd121189","datavalue":{"value":{"time":"+1994-03-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1314360$074F9164-81D2-4A56-990C-2762957CC4C7","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b6165f935492e5a3f10035a0167c2cdcdd89d089","datavalue":{"value":"The starting point of the paper is the observation (due to J.-Y. Girard) that no term of System F (also called polymorphic, or second-order \\(\\lambda\\)-calculus) can discriminate over types. Indeed, in all the intended models, terms are understood as essentially constant functions on input types. It follows that it is consistent to add to \\(F\\) the following axiom (C): If \\(M:\\;\\forall X\\sigma\\) and \\(X\\not\\in FV(\\sigma)\\), then \\(M\\tau= M\\tau'\\) for any pair of types \\(\\tau\\), \\(\\tau'\\). The paper studies the system Fc=F+C and proves that, in Fc, any type acts as a generic input (that is, as a variable). Formally, it is proved that, for any two terms \\(M,M':\\;\\forall X\\sigma\\) (no restriction on \\(\\sigma\\)), if \\(M\\tau=N\\tau\\) for all type \\(\\tau\\), then \\(M=N\\) (genericity theorem). The proof is syntactic and difficult. Since in Fc two terms can be equal without their subterms being equal, the paper introduces the crucial notion of generalizer of two Fc-equal terms: roughly put, a term can be instantiated to the two terms by type substitutions and then proved equal to them via axiom C. The paper ends with a discussion on models, showing that both PER, dl-based, and ``dinatural'' models satisfy axiom C.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1314360$309F1F5C-C6C1-4B89-A5A4-16CC27EF3878","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1314360$5BBE8F96-FECD-4A77-9442-43B73F16A908","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1314360$7D87EE99-04DA-4C75-B610-720371D8CE97","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"90e5174c7df86eba6fa5cff058428736e9b5b5b0","datavalue":{"value":"501173","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1314360$157DF933-DE46-45B3-8852-663FABDD4B58","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"530eb471449c092403ef82fcef8249c03fb2c62f","datavalue":{"value":"polymorphic lambda-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1314360$D86E7289-B301-49CD-9DF1-70B60413017C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8fe810434f585fa0203aea78467c3725c30107f8","datavalue":{"value":"parametricity","type":"string"},"datatype":"string"},"type":"statement","id":"Q1314360$2520C097-66BF-4DF5-83F6-5BC78ECB4A24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"83d5dcaa7aef3dc9ddc3eab92a7db35d53442c07","datavalue":{"value":"proof theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1314360$06D5E72B-70FA-4101-82CB-EE2BCCFD83FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1314360$EC17A3E7-5273-4C8F-9506-E9305F2D36CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"33fd81627acd56a240fde0d4d7060d89e19d0782","datavalue":{"value":"System F","type":"string"},"datatype":"string"},"type":"statement","id":"Q1314360$4EF8C4BA-F36C-4026-9096-45D6DFD0AB6E","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"00ea4a5ed8879c1a6adc0802c8c4ce48d27b9055","datavalue":{"value":{"entity-type":"item","numeric-id":596036,"id":"Q596036"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$27E1C9BD-C70F-4632-A528-63F8E9073CDA","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":"Q1314360$6A84B5BA-F3C8-487C-9568-9834764F9676","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"505171d534e8156f1194ca39d6ed63e8614fb17a","datavalue":{"value":"https://doi.org/10.1016/0304-3975(93)90093-9","type":"string"},"datatype":"url"},"type":"statement","id":"Q1314360$1D769DB4-C77F-4932-AB68-9B9A01A8C401","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"49f4820241426d635f2c2a66651364ddce68597c","datavalue":{"value":"W2042577486","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1314360$509D0E80-C00B-41A8-B20A-E6559EA80325","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b1146bbc5e086759e31519ce524dbf829161b6f","datavalue":{"value":{"entity-type":"item","numeric-id":1314344,"id":"Q1314344"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$174327E4-3A41-484E-AB5F-9793B9E30C67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"005537799f3a85442d3ad04f80b3b2e785727979","datavalue":{"value":{"entity-type":"item","numeric-id":3999603,"id":"Q3999603"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$7A6BB5C6-8A17-48CC-821C-D72402E6D9B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"956c663a8c65ca7a493106b21f9b04a9a741383f","datavalue":{"value":{"entity-type":"item","numeric-id":1155602,"id":"Q1155602"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$8D3D1161-16FF-4B31-A81C-C4827353E791","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d7a531083726a145d8fccd94df1a0b11326845f6","datavalue":{"value":{"entity-type":"item","numeric-id":4943310,"id":"Q4943310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$566B7C0A-007D-4C7F-AACB-9B71FC5065CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0a4ac9496c42e23fd254aa24e5eda39806cc4a9e","datavalue":{"value":{"entity-type":"item","numeric-id":4939689,"id":"Q4939689"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$220FB440-91D0-4323-9DF3-82C0772DA3D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"270134eb666efe341cad63c19635ac163dd4347a","datavalue":{"value":{"entity-type":"item","numeric-id":5096247,"id":"Q5096247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$6F13825E-9024-45C6-A1B8-BF228F57B6A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"81f1fc2c53f8489c262229a49273407a2a8e9cca","datavalue":{"value":{"entity-type":"item","numeric-id":3787462,"id":"Q3787462"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$9FEC76A4-FC3B-4284-A538-0B4CD761B94C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ee716641fb5a9980d86c550478f92d959242ffa0","datavalue":{"value":{"entity-type":"item","numeric-id":4010353,"id":"Q4010353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$A6F74AFC-7CB3-4B43-8D2D-E24CD3CC6CFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"897b983090a7e7931ca4c3b1f285f76249983ba1","datavalue":{"value":{"entity-type":"item","numeric-id":2524062,"id":"Q2524062"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$14493652-D44C-40E1-A1F0-67D361387F85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5cb3fb1f5163c51d21987992526ad7f1b03bc113","datavalue":{"value":{"entity-type":"item","numeric-id":5625124,"id":"Q5625124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$ABECF5C3-D916-4D1E-B777-1F1D682D2BC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22ee85ee408ceb2acfb30c438cac3496a36c4200","datavalue":{"value":{"entity-type":"item","numeric-id":1091379,"id":"Q1091379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$ADA378BC-A5CE-43BE-8AB4-58F3BB7FCF2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99c6176bcb92cea3bde43c51d54f8875f446d09c","datavalue":{"value":{"entity-type":"item","numeric-id":3994895,"id":"Q3994895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$E4FDA1D9-B367-438A-AB2A-4ECC33D33008","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d910458719fa4b8b6b194265f13642c414193620","datavalue":{"value":{"entity-type":"item","numeric-id":4010357,"id":"Q4010357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$ED248793-BC35-42D1-BBDB-8166083CE141","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a2bcd4ae2579c74a21d7451a3e9068802bcce70c","datavalue":{"value":{"entity-type":"item","numeric-id":4286531,"id":"Q4286531"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$1D23BBD5-7073-4BE4-99D9-68AF3B5F6B66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e6ecd315aede1159b901d05a2b312181be4e2315","datavalue":{"value":{"entity-type":"item","numeric-id":1112159,"id":"Q1112159"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$74B418DD-94F7-4C23-868B-CCEEC48334DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d82b227295c10b6c3c9289b01dc8016d6c611441","datavalue":{"value":{"entity-type":"item","numeric-id":3727946,"id":"Q3727946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$3D44F78F-0A73-4528-9CFC-DE63EC964547","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4411aad98b29f9e9b8ef38bccdd1f93a7a72fa40","datavalue":{"value":{"entity-type":"item","numeric-id":4327831,"id":"Q4327831"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$542BBCE1-6910-4376-A3F3-E8E0C44668B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b94cf9631c9e91afb0e168451174422010e0452e","datavalue":{"value":{"entity-type":"item","numeric-id":4006232,"id":"Q4006232"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$8391BD97-25A2-43A9-A9DD-9C823379915B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"534480bfab7acfeee5d80ae4528655224ebda578","datavalue":{"value":{"entity-type":"item","numeric-id":5639839,"id":"Q5639839"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$FF3EB5A2-EA3B-4763-BB6B-08F754F1130A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ad36ee1e9b536ba43cedd35d7459acb4e4a8d4b","datavalue":{"value":{"entity-type":"item","numeric-id":4281485,"id":"Q4281485"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$17F6177C-7E85-49D3-AB66-854BBA35C22F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f3d307a31d75ce205d43f99746df1f049e810792","datavalue":{"value":{"entity-type":"item","numeric-id":5624680,"id":"Q5624680"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$20CD8EED-1FB5-4096-85B3-32CC93548E7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bf701c74ef07eac6f191b34254e528b70e4494ba","datavalue":{"value":{"entity-type":"item","numeric-id":5649639,"id":"Q5649639"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$1FF90099-AC59-47EF-BEF9-EC42791A1491","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"11369978efa15dc62da89d10bfe437030b4aa86d","datavalue":{"value":{"entity-type":"item","numeric-id":3956379,"id":"Q3956379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1314360$5397D100-38E3-4EE8-BE22-1190F03F2C3A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f4116d7bb7083b191bc72e76ece0f0ff01486a31","datavalue":{"value":{"entity-type":"item","numeric-id":1314344,"id":"Q1314344"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b05fddc975cacb6f8173b74aa163aaec9c0f004a","datavalue":{"value":{"amount":"+0.7807358503341675","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":"Q1314360$47E18051-46F0-4A2E-8225-08DE210EE4D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0f18797958507bb2e43a1c60582934bf69c5d06a","datavalue":{"value":{"entity-type":"item","numeric-id":4327831,"id":"Q4327831"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"94c4dce8a616fd5aa6c54d733536ec0d9ca60d55","datavalue":{"value":{"amount":"+0.7791103720664978","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":"Q1314360$15F148AC-1E83-4D20-9088-020797631E2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2d9e5dc2968041f4cb2517716fd874284e3ab330","datavalue":{"value":{"entity-type":"item","numeric-id":3483291,"id":"Q3483291"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c8128a42db42199672b27bfb3459376be9b2c783","datavalue":{"value":{"amount":"+0.7763921618461609","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":"Q1314360$93242F47-AF71-471C-ABD5-058C27CB9D99","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1314360","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1314360"}}}}}