{"entities":{"Q514511":{"pageid":516278,"ns":120,"title":"Item:Q514511","lastrevid":52755515,"modified":"2026-01-23T10:43:57Z","type":"item","id":"Q514511","labels":{"en":{"language":"en","value":"Compositional Z: confluence proofs for permutative conversion"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6690918"}},"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":"Q514511$53C8F90C-F291-41AA-9E45-5CA8DF055CBD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f0ec37e153168a2db8e74c4e1065a0c5de69c695","datavalue":{"value":{"text":"Compositional Z: confluence proofs for permutative conversion","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q514511$13F89CE3-BCF1-4CF8-89A2-277A8DD794DB","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"388fb46422677aee3dcab906053ee1170e5b29d1","datavalue":{"value":"1368.03020","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q514511$8575F89D-B8FB-4779-8483-09925DFDA6BA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d3bbd3187d950ecd141481b362fa15a71f8566a6","datavalue":{"value":{"entity-type":"item","numeric-id":514510,"id":"Q514510"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q514511$8F39A7ED-FD13-4474-A28D-645752C1759D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"647c63bfabe2cc5aa72008693495435e80f88915","datavalue":{"value":{"entity-type":"item","numeric-id":402116,"id":"Q402116"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q514511$3F92B2C7-0225-4D26-85DD-E24547E1FA3D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e34236ca73b92c6ee0bc17431d03c3537a7f0792","datavalue":{"value":{"entity-type":"item","numeric-id":195358,"id":"Q195358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q514511$D9155269-DFF8-47B2-B5D3-5483F0005DE2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1a8460bdb64b4b5e4361d553b383ac843f49ee0c","datavalue":{"value":{"time":"+2017-03-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q514511$91914C95-80BB-4E6E-986D-872E7E65C750","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"fdccd6d97f048f41fca3f4baf80095903dc900e1","datavalue":{"value":"The Z-theorem of \\textit{P. Dehorney} and \\textit{Z. van Oostrom} [``Proving confluence by monotonic single-step upperbound functions'', in: Logical models of reasoning and computation (LMRC-08) (2008)] allows the proof of confluence for a number of variants of the \\(\\lambda\\)-calculus. In the current paper, the authors generalise this to a compositional Z-theorem, which is easily proved from the Z-theorem. The new theorem allows, in addition, proofs of confluence for \\(\\lambda\\)-calculi corresponding to intuitionistic and classical natural deduction with disjunction and permutative conversions as well as a \\(\\lambda\\)-calculus with explicit substitution.","type":"string"},"datatype":"string"},"type":"statement","id":"Q514511$4B08C5A5-4BAE-401C-A76F-6F08874708A1","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"376f136d3715d0668145bfef82b652dbeb24818d","datavalue":{"value":{"entity-type":"item","numeric-id":591019,"id":"Q591019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q514511$51BE9D02-36A7-47AD-8EDF-F8BFAF71B5EF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q514511$C5AA66A9-D5B5-406B-86B7-9BDB42F8C997","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"979fceaa054077749fb746a02e271facba8851dd","datavalue":{"value":"6690918","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q514511$E54C2908-AC05-4270-B9D3-26140F326AE9","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b876698d821b50cd7ba02ddb5424ed80f1905d8","datavalue":{"value":"lambda calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q514511$46F56B82-DE7C-471F-8E05-7E1E35D90752","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e377735fef4b0e5d31c97baa26e95cc6323e216f","datavalue":{"value":"lambda-mu calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q514511$DA503487-7447-4C85-9895-B82A04813729","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b38049d159af5d6c62de79db7ea882fef0c299bd","datavalue":{"value":"confluence","type":"string"},"datatype":"string"},"type":"statement","id":"Q514511$A65754E3-5948-4674-8F7F-E2EB4585CA57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"40ee02f0ddc510a82630d2121cf8d03915cbee3f","datavalue":{"value":"permutative conversion","type":"string"},"datatype":"string"},"type":"statement","id":"Q514511$8ADD4A10-A8BB-4B6B-8DDC-5260CBFA0A5C","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":"Q514511$2983BB8A-9FF3-4576-92D9-4A3FF2933E83","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b509ebd75cf9a06cae54e267758b877a63dced89","datavalue":{"value":"https://doi.org/10.1007/s11225-016-9673-0","type":"string"},"datatype":"url"},"type":"statement","id":"Q514511$657CB40E-19B9-4AC9-BC89-17B525960258","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"415a57bd247f261e6c40c1d49fb06d4b1dfd4085","datavalue":{"value":"W2407924833","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q514511$039623BE-F444-4A6A-8A69-6FEA37D6BC58","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"8b16b1ce1df54d07279efc3bc513f7d63a19a0ef","datavalue":{"value":"Q113900501","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q514511$00F1F4B8-4096-4C49-BC5F-328C57B65AED","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"884ff47e3131a2ae77eac9b93d6ec7e48620fea3","datavalue":{"value":{"entity-type":"item","numeric-id":2891437,"id":"Q2891437"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q514511$ED0083D2-9D80-4AD9-A42D-3F55F156698E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"115adf875681b76e6e24dffcf58a246bfd7b0a90","datavalue":{"value":{"entity-type":"item","numeric-id":1861541,"id":"Q1861541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q514511$B1E9C893-A10A-468C-ADEF-DD252A7801E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f14d7967fb21e1684a2efd177087149a79f15644","datavalue":{"value":{"entity-type":"item","numeric-id":2703743,"id":"Q2703743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q514511$E39FC35B-07E6-42A3-890B-E983B602000C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"107eec03b6587e73479808a48d1286903f6903fa","datavalue":{"value":{"entity-type":"item","numeric-id":5763294,"id":"Q5763294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q514511$A3FB5FAC-B341-4CDC-BB1C-54EAB02CE85B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dfa735550c2611795db9bb6e05d804967b1a4644","datavalue":{"value":{"entity-type":"item","numeric-id":2482842,"id":"Q2482842"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q514511$19518B82-1B3C-4414-A32F-B48209F7FCEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9856799bebc3b14cff23d50b4af9f7cda1dbd633","datavalue":{"value":{"entity-type":"item","numeric-id":1575247,"id":"Q1575247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q514511$F86F28A1-469B-4BF6-8B80-9A0ED4D524E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e46d804a5363d847a2e9e54d905ff7e520257179","datavalue":{"value":{"entity-type":"item","numeric-id":2016071,"id":"Q2016071"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q514511$F2FDA4B6-91AB-4E74-8B2B-302AB0C8D9A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba77032c0040be2f70dfa30571b8befbc2b97dc8","datavalue":{"value":{"entity-type":"item","numeric-id":5170828,"id":"Q5170828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q514511$0D4421DE-585E-4C2B-8632-B0297C8E9BB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66257d76632b86525de5e8f5c47c6c6cf781ec1c","datavalue":{"value":{"entity-type":"item","numeric-id":4255509,"id":"Q4255509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q514511$609D6CBA-212A-4EE8-A464-32C7480C94A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8d95625ec9e5b7c46cee42d87256157d982706a","datavalue":{"value":{"entity-type":"item","numeric-id":5559220,"id":"Q5559220"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q514511$B0F8DD9D-8835-4533-A05E-E95801D900DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c382f571059f65c71d7c5267e06c23fa2d98eb72","datavalue":{"value":{"entity-type":"item","numeric-id":5917605,"id":"Q5917605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q514511$2B73F16A-C7B0-45F3-A3D4-E46FDE02D1F1","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"51c89962f551d1fa424841b63e7c68226c8b5c42","datavalue":{"value":"10.1007/S11225-016-9673-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q514511$527567C2-A908-416A-A665-5CADA2645030","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8a63a53c5ca5e830d1d1db942c98c303f685af3d","datavalue":{"value":{"entity-type":"item","numeric-id":5879272,"id":"Q5879272"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"05a6fc276d7065565589640c7a2f394fa5042992","datavalue":{"value":{"amount":"+0.834930956363678","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":"Q514511$FBE51160-BE85-4E17-9AFD-8DED0EF6E172","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bbbdc6542d2cf953da88e7f6b4554d455ec1735e","datavalue":{"value":{"entity-type":"item","numeric-id":2891437,"id":"Q2891437"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9e3618cfad3eb8c4755d9c61506d0ab6423efaa0","datavalue":{"value":{"amount":"+0.8114481568336487","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":"Q514511$0D22482C-D8EC-4850-B76A-D57AB3EBE885","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3a4e92796aa0fc101abca836515f5d0d4e600336","datavalue":{"value":{"entity-type":"item","numeric-id":1275632,"id":"Q1275632"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bfefafbba4256bc0f9dfd0f3217303a21d4420b9","datavalue":{"value":{"amount":"+0.7713627219200134","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":"Q514511$C0F3336C-89F5-4D3A-BDE1-4A80D04E9799","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7e61470031e19b978baad8de644fb73af3dbbd46","datavalue":{"value":{"entity-type":"item","numeric-id":2723897,"id":"Q2723897"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8c06d545135c0a98bd397dcfd818b6056f9c2044","datavalue":{"value":{"amount":"+0.7710283398628235","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":"Q514511$BDCA8A9B-F12D-4509-9FF0-F6E1673C7842","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4741c4be621d9cb1dc206c96fc8a184aeda78935","datavalue":{"value":{"entity-type":"item","numeric-id":732008,"id":"Q732008"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"57bea6570b6e8141817e99e7b2d5612543993e76","datavalue":{"value":{"amount":"+0.7621773481369019","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":"Q514511$C82EA514-8F08-402A-90E9-6DBDC2152641","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:514511","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:514511"}}}}}