{"entities":{"Q53725":{"pageid":53781,"ns":120,"title":"Item:Q53725","lastrevid":105428843,"modified":"2026-10-09T10:10:43Z","type":"item","id":"Q53725","labels":{"en":{"language":"en","value":"Monad normalisation"}},"descriptions":{"en":{"language":"en","value":"AFP entry Monad_Normalisation"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"7b9c69fd454f7ce9a4294c7843e22d5fc4398f67","datavalue":{"value":"38025","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q53725$A0AFA5C2-01D5-40F2-B2E3-EEF150712962","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53725$79CAF8A6-05C8-4E70-9878-CF7E8FBB0C4C","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"e56118f13a007728a9af922c5327e76ee3c27ab7","datavalue":{"value":"https://www.isa-afp.org/entries/Monad_Normalisation.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q53725$B4231FEF-2D43-47C6-99EC-560EA0ADFBE2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q53725$B67E778D-1E2E-4419-86C4-4E24EB155814","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"74afd8a3b10bf054bf31ff15012404c74fd8d4f2","datavalue":{"value":{"entity-type":"item","numeric-id":53726,"id":"Q53726"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53725$63C4F1CE-27EA-44EC-AAE2-46D6F7CF1524","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"244ebbac6461f60bed6d50e50ce8194b0e233968","datavalue":{"value":{"entity-type":"item","numeric-id":40296,"id":"Q40296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53725$9633E552-D4D6-4ED3-ADD1-9027A5B26488","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"3a073d1e3162db58b1a890386d8dbe9eebb4637c","datavalue":{"value":{"entity-type":"item","numeric-id":40373,"id":"Q40373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53725$F8653191-9482-49BA-BA56-C8D9D24E30EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"b74075817e632ca235b8b1333580f4f12e29f9fd","datavalue":{"value":{"entity-type":"item","numeric-id":40372,"id":"Q40372"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53725$32FBB22F-A852-4C7E-8E14-B22EAAF7F38C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"868d665ea0607bf8bd28ea3e3872eb2ea87bd3d3","datavalue":{"value":{"entity-type":"item","numeric-id":40371,"id":"Q40371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53725$8D43FA66-86AB-45DE-93B3-E73AE280D7BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53725$F180D9D8-514C-419D-8610-CAD59F4A7DD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"246d8bcd4bf1600a7c6d2b07f9f11f8689d33486","datavalue":{"value":{"entity-type":"item","numeric-id":40320,"id":"Q40320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53725$BD083137-FAFB-42A0-B8E3-73F47AE7B671","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"6bbc316d4497e097d8fb3e48fd57f7643b44826c","datavalue":{"value":{"entity-type":"item","numeric-id":40246,"id":"Q40246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53725$159232A1-C00C-42A6-82E8-C39352E3E4E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"03bedb439d5ea402bd9603d3cdfe1813f9fa06ca","datavalue":{"value":{"entity-type":"item","numeric-id":40356,"id":"Q40356"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53725$92591F92-56F5-402D-9210-8F5C36BD811F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"0777df209460f6d453f13a63edbbd60cf656f2b5","datavalue":{"value":{"entity-type":"item","numeric-id":40355,"id":"Q40355"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53725$5EEADB74-65D1-4FD3-B687-A2DE3865EB15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"dd25ad249c2b0bfc0ae57f791baa0d6fded59cb3","datavalue":{"value":{"entity-type":"item","numeric-id":32511,"id":"Q32511"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53725$0EF913D2-740E-412B-8300-CEDB0BB7D20F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53725$80882F58-C5B8-41C9-A790-4034044C55AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53725$9D40EC37-91AA-47A0-8D9A-AD047ABD6DBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53725$D03DDF9D-ABB5-401F-8AC1-1B3667E7045F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7b91d8aa721d2d387d4f0ce3416150798f495a4e","datavalue":{"value":"https://isa-afp.org/entries/Monad_Normalisation.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q53725$7385906B-44BF-45AE-95C7-497CFDDB9627","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"c80b4b2e0add38e8530cb24c3a877ff0cb92104c","datavalue":{"value":"Joshua Schneider","type":"string"},"datatype":"string"},"type":"statement","id":"Q53725$921329CF-3930-4EBF-B6D3-5FD455C6F894","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"85859c7ab42dcb8b36208f2902b7ce0d86423a6f","datavalue":{"value":"Manuel Eberl","type":"string"},"datatype":"string"},"type":"statement","id":"Q53725$BBF2B1D4-51D9-4AB2-B6BA-8DC98E76612E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"480a99c095fd0e6e30ce40dd951da46a627a2bb9","datavalue":{"value":"Andreas Lochbihler","type":"string"},"datatype":"string"},"type":"statement","id":"Q53725$913D9C78-9D06-4F03-A0D1-90C84027AE70","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"689695aac021cfeb95f1a9e52db239aaae2ce1e7","datavalue":{"value":"The usual monad laws can directly be used as rewrite rules for Isabelle\u2019s simplifier to normalise monadic HOL terms and decide equivalences. In a commutative monad, however, the commutativity law is a higher-order permutative rewrite rule that makes the simplifier loop. This AFP entry implements a simproc that normalises monadic expressions in commutative monads using ordered rewriting. The simproc can also permute computations across control operators like if and case.","type":"string"},"datatype":"string"},"type":"statement","id":"Q53725$6E20D3CB-F61B-4C66-9DED-A891457AB9BD","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac263bfef6149f05e56a58b596a06010298db53f","datavalue":{"value":{"entity-type":"item","numeric-id":1332775,"id":"Q1332775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53725$54308EF6-740B-44CD-894A-A1AF75AB5EA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dfc2d8ca19d9bb1cc0552ab960dd9d1b399bad24","datavalue":{"value":{"entity-type":"item","numeric-id":2829262,"id":"Q2829262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53725$82E0A0C5-4D63-4041-8367-A7DB833A33B5","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"7a918ca57cbef7417c708001c9499e7e295238c0","datavalue":{"value":{"entity-type":"item","numeric-id":7360836,"id":"Q7360836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53725$0B6296DF-D4E3-41F1-A652-E2CEFF11841F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P2651","hash":"edf8a8949edec3767dd80b6d3acecc92e5d25f1c","datavalue":{"value":{"entity-type":"item","numeric-id":7360818,"id":"Q7360818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53725$AC9C725B-ECFE-4C4E-A99B-B16BBCC29D5D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2521123b5dbe8709daed0db214711d9c66f9f8cf","datavalue":{"value":{"time":"+2017-05-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q53725$CB090E64-8F5C-4AAB-A912-830C4D1FAACE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"68a112d6b37aa30062c47fbad93f86b7ae9dedb9","datavalue":{"value":{"text":"Monad normalisation","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q53725$67E68F46-9961-41D7-AA0D-571FB9F67310","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53725$AEC4D414-00A2-4C4D-9CBF-694D09730206","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Monad normalisation","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Monad_normalisation"}}}}}