{"entities":{"Q7361353":{"pageid":31519598,"ns":120,"title":"Item:Q7361353","lastrevid":105365144,"modified":"2026-10-07T13:35:44Z","type":"item","id":"Q7361353","labels":{"en":{"language":"en","value":"Shallow Expressions"}},"descriptions":{"en":{"language":"en","value":"AFP entry Shallow_Expressions"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"dfa7e56eb33d5d3851cee7bfd85df279242136ee","datavalue":{"value":"https://isa-afp.org/entries/Shallow_Expressions.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361353$88320440-A081-4DC8-8DAD-403AAC2371C7","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9e38b2634e305e231552e36caaa08079db34ce75","datavalue":{"value":{"time":"+2025-05-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361353$9509B35A-2384-4E23-9AF3-6C167B7D08C8","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"c9ddb9cb8edac3e4e3079ad62f4b03206fa5cc4b","datavalue":{"value":"Simon Foster","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361353$66E9F4C1-C219-4453-B649-3875C5620B0D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"39170305db6b715309e1343e9fedec93f402003a","datavalue":{"value":{"text":"Shallow Expressions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361353$8FB5D7DA-9178-46A0-BB14-805768045F85","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"0b4184c9eaa2989c2f5d2d880a2257791a2c1223","datavalue":{"value":"Most verification techniques use expressions, for example when assigning to variables or forming assertions over the state. Deep embeddings provide such expressions using a datatype, which allows queries over the syntax, such as calculating the free variables, and performing substitutions. Shallow embeddings, in contrast, model expressions as query functions over the state type, and are more amenable to automating verification tasks. The goal of this library is provide an intuitive implementation of shallow expressions, which nevertheless provides many of the benefits of a deep embedding. We harness the Optics library to provide an algebraic semantics for state variables, and use syntax translations to provide an intuitive lifted expression syntax. Furthermore, we provide a variety of meta-logic-style queries on expressions, such as dependencies on a state variable, and substitution of a variable for an expression. We also provide proof methods, based on the simplifier, to automate the associated proof tasks.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361353$8BC9EB86-4C81-4B75-9C31-C626CDD2516B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"13b2e611a60bbb1cbb1ab23d8301e40dbbe2b3c5","datavalue":{"value":{"entity-type":"item","numeric-id":2915136,"id":"Q2915136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361353$DD997405-054C-47A8-B712-EB1E6684E0E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cad5dbbae1e8a09daaaad27474e686d1687d9ae4","datavalue":{"value":{"entity-type":"item","numeric-id":5327345,"id":"Q5327345"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361353$E4DAD3F9-69FF-48CF-B085-8894A496468A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fc62f32ebe5f2c566c09500f98ee202c262830a","datavalue":{"value":{"entity-type":"item","numeric-id":736461,"id":"Q736461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361353$013B5750-3CB7-461B-BF08-73CEB049E882","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad5469f72b3d14e0a040a00af8c98b8e5cf4cb2b","datavalue":{"value":{"entity-type":"item","numeric-id":3172879,"id":"Q3172879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361353$FAAD8D3E-A984-48EE-B752-B4946222E779","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc2ebcfc9e03f9a578c2b1e9422c73be36fc4a17","datavalue":{"value":{"entity-type":"item","numeric-id":2176678,"id":"Q2176678"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361353$66FB829F-2D9E-439D-8510-EFBDCA132C73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42767904ec698e77bf5ad5a5ca09192ebfa305eb","datavalue":{"value":{"entity-type":"item","numeric-id":2941173,"id":"Q2941173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361353$87067C39-1B3C-4510-9467-18F2DF18C99B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42e8700434177609e5f649d1f5a0b31b34ec0771","datavalue":{"value":{"entity-type":"item","numeric-id":3055747,"id":"Q3055747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361353$82D0B5BA-2AA1-4FD3-AFE6-D5AF3E1DF0DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ea00f9571a2f3eb35a08ae82329dd711da0dc8b","datavalue":{"value":{"entity-type":"item","numeric-id":2814613,"id":"Q2814613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361353$3B0FED3E-3DE3-4F55-AA9B-0F2FBA4DB94C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e0bbb1d8cfb9b91bd41f05780d54a53310b43ff","datavalue":{"value":{"entity-type":"item","numeric-id":2352506,"id":"Q2352506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361353$B8EE3EEA-B42A-4E84-AAAC-F8163A2CE4A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5981e1168811f3b1a276d506216532fa05a55595","datavalue":{"value":{"entity-type":"item","numeric-id":3179407,"id":"Q3179407"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361353$AA6F8CEB-1C14-4340-AE22-0F7A3F5ED33F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c3587daf8b7bb37c28a02a6be9585e6348d1d132","datavalue":{"value":{"entity-type":"item","numeric-id":2971175,"id":"Q2971175"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361353$CFC52A42-1021-44BE-8551-52A163C90180","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"23a4f79d5a209fbc2d0b0773de40c58b9c966c61","datavalue":{"value":{"entity-type":"item","numeric-id":2971180,"id":"Q2971180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361353$0C23026A-2486-4DD6-A74F-7E2296E7CC7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f86b973e3b901484f98039b484118a2d2770aaf6","datavalue":{"value":{"entity-type":"item","numeric-id":1708268,"id":"Q1708268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361353$4D281006-A734-4B4E-B33F-0F63A785ABE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"10d3aec833cdd3cd581a6940d6e98f1f489fd75a","datavalue":{"value":{"entity-type":"item","numeric-id":5098716,"id":"Q5098716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361353$576E5EDF-5C88-4F01-A270-6458B95D5AFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d8e0ff8a7d0c4fc199c213531e4694eacc1d9f6","datavalue":{"value":{"entity-type":"item","numeric-id":2938044,"id":"Q2938044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361353$F0B0C29D-BEC5-402E-867F-EB4DC979AFBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88fbfcea2166cf55628dc74bb062db5b5b011195","datavalue":{"value":{"entity-type":"item","numeric-id":2914753,"id":"Q2914753"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361353$660DD4E7-42B7-4AE5-AB0E-0B1B86CC83DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e8576dc8df0d7857399ab718724b601efc6d9d7d","datavalue":{"value":{"entity-type":"item","numeric-id":3996918,"id":"Q3996918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361353$47E1588D-B594-4A91-9A47-A03387B59080","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9e0c5a0606b38fe0c68c2b912ea6ff4cb19476ec","datavalue":{"value":{"entity-type":"item","numeric-id":6653093,"id":"Q6653093"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361353$A44F90EC-6DB4-4955-B713-FDEAC8732FD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"deb9865b9ec7d75ea6408f7463449ba93e2c161e","datavalue":{"value":{"entity-type":"item","numeric-id":5307478,"id":"Q5307478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361353$3D14FDAE-AD0A-413D-88DB-EE8E5EAD249E","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":"Q7361353$FFBF3D83-4B9F-4A3D-A2F7-055A619EBEF6","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"38013d195453d9de6ec304fa06493915c9a40199","datavalue":{"value":{"entity-type":"item","numeric-id":7361308,"id":"Q7361308"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361353$5486CF19-AFAD-4B54-9B47-ABDD65067EA2","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"65dbfb47d0b5da65bd2cdfbc8cab28721a9f7690","datavalue":{"value":{"entity-type":"item","numeric-id":7360803,"id":"Q7360803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361353$0BA64842-BEF0-4B15-8FE7-A3EB432E4C85","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":"Q7361353$5B47F7EE-CC84-4486-9176-7AC4AC7CA464","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Shallow Expressions","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Shallow_Expressions"}}}}}