{"entities":{"Q5958752":{"pageid":8135554,"ns":120,"title":"Item:Q5958752","lastrevid":55972417,"modified":"2026-02-21T15:48:45Z","type":"item","id":"Q5958752","labels":{"en":{"language":"en","value":"Primitive recursion for higher-order abstract syntax"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1715797"}},"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":"Q5958752$6D31BE0B-C8F0-4E7F-9D54-0B7F59D79B08","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"67e80504e31838548f7b50dd56a336f655d41732","datavalue":{"value":{"text":"Primitive recursion for higher-order abstract syntax","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5958752$E740D217-2CFD-4A58-852A-0395375A2831","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c14baa3591daa013a11ec1a3289003278e99eaa0","datavalue":{"value":"0994.68028","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5958752$4B3FF608-ED6D-460F-A744-F18389C1DE50","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"98923cced7180f023a6b6c8d6e0ed5fed5b0faeb","datavalue":{"value":"10.1016/S0304-3975(00)00418-7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5958752$1D0638DD-DE7B-4516-B5E2-A4CE8F7B246C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e1024ad51fb0c89617301d9b58c1789ce603d4d1","datavalue":{"value":{"entity-type":"item","numeric-id":2092486,"id":"Q2092486"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958752$97F4EBE3-152F-4443-BD4C-A8469C900CEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7e18514c052906fdc7b4ca4d0942d5aaa597b9ba","datavalue":{"value":{"entity-type":"item","numeric-id":688726,"id":"Q688726"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958752$634D7601-07DE-4CAF-B622-0FF5E256AFA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1a33736bad804e6a530176061e0a43d6da42cd52","datavalue":{"value":{"entity-type":"item","numeric-id":476188,"id":"Q476188"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958752$72F836CD-C0C3-4893-88BF-DAA3BA46D3BF","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":"Q5958752$98473889-EBFE-4557-A033-65A3956E02A2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"de0bbc1f0efc0eda52d8a37720ec217ae66c93cd","datavalue":{"value":{"time":"+2002-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":"Q5958752$55CEE8C1-6C1F-4881-88B1-F534F28582C4","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"d8fe780716aa92ecc21a4f4a1599cd8ac6882aa2","datavalue":{"value":"Higher-order abstract syntax is a central representation technique in logical frameworks which maps variables of the object language into variables of the meta-language. It leads to concise encodings, but is incompatible with functions defined by primitive recursion or proofs by induction. In this paper we propose an extension of the simply typed lambda-calculus with iteration and case constructs which preserves the adequacy of higher-order abstract syntax encodings. The well-known paradoxes are avoided through the use of a modal operator which obeys the laws of \\(S_{4}\\). In the resulting calculus many functions over higher-order representations can be expressed elegantly. Our central technical result, namely that our calculus is conservative over the simply typed lambda-calculus, is proved by a rather complex argument using logical relations. We view our system as an important first step towards allowing the methodology of LF to be employed effectively in systems based on induction principles such as ALF, Coq, or NuPrl, leading to a synthesis of currently incompatible paradigms.","type":"string"},"datatype":"string"},"type":"statement","id":"Q5958752$06E3D579-106E-4D02-A921-F2B14F644D68","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5958752$2391E264-56E1-47C9-B3BB-A778F90FA1ED","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b455f16ed75b62234b46c1a4bfe0b2142610dee9","datavalue":{"value":"1715797","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5958752$3003FE42-E137-4D0D-B91D-2D12DE2F445E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"01f639a56e1e38a2490c4463ce011c878a3d36ab","datavalue":{"value":"typed lambda calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q5958752$C832E347-A28B-49B4-886A-251F82528158","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8026960d6f36428821b4502bc1641829b1806e7e","datavalue":{"value":"higher-order abstract syntax","type":"string"},"datatype":"string"},"type":"statement","id":"Q5958752$FA18435B-E786-4317-B298-FEC213869A2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ac91c497e5a12b747663afac74f58bf2ab28eb97","datavalue":{"value":"primitive recursion","type":"string"},"datatype":"string"},"type":"statement","id":"Q5958752$D7C83468-CF55-48DA-AEBD-5A73F9C1A838","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f1dda010537b7b36bd45151721146f720815706e","datavalue":{"value":"modal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5958752$7C60B131-2124-4903-80D7-5D10BC7668AA","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6111489034643139b6436054b44d6250e7c1756c","datavalue":{"value":{"entity-type":"item","numeric-id":41339,"id":"Q41339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958752$98307D55-1317-4CDB-A6AC-2C807107F989","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"05e19126d9e9907924a4600d0a5598afdc2c5f70","datavalue":{"value":{"entity-type":"item","numeric-id":20609,"id":"Q20609"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958752$D6F629C3-7962-4407-921C-157668487C31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"666b9a47dc68ef552d799234146196fb61f3c743","datavalue":{"value":{"entity-type":"item","numeric-id":33169,"id":"Q33169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958752$45965C8C-1BBE-4321-8B1E-EDFDE39E733C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27b6ae20da44d6f09b655d9481cc0df08a8ffcdf","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958752$CE0DE320-1345-41D0-AC19-A7C168823F17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958752$3D34E6DD-AB91-4A26-BD56-96A2B59D90CE","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":"Q5958752$0E39604B-E1E9-43B4-BBF6-204383A64854","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ebad1ec32f84aea32b38859e9c126afe144df8b","datavalue":{"value":{"entity-type":"item","numeric-id":4289277,"id":"Q4289277"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958752$5576966F-BB7F-4A3E-97AA-CC4B08316557","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05618bc94dd537d3034b233a45ab1cb0906c9164","datavalue":{"value":{"entity-type":"item","numeric-id":3196622,"id":"Q3196622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958752$9E79EE2A-25EE-4AF5-BD79-E7D75B276AE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e723c31e56f2487bba3b93f0d7637a4943535187","datavalue":{"value":{"entity-type":"item","numeric-id":3024831,"id":"Q3024831"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958752$3C2D3D5D-DFC0-4252-BC4D-D5A206A2344B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3bbda4d5d2fa3599cf321b083730ba47f18179a2","datavalue":{"value":{"entity-type":"item","numeric-id":3024905,"id":"Q3024905"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958752$4F2FE940-62DB-4D92-A429-9E576A4975D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"021e6e2184fd3d7f831680d56b426b95217eac7a","datavalue":{"value":{"entity-type":"item","numeric-id":4033837,"id":"Q4033837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958752$B5114E8C-565D-499C-BDCB-6E670E2CE4B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ab5d7b35f67f940445411fa45c1b02bcb40d39f","datavalue":{"value":{"entity-type":"item","numeric-id":3999860,"id":"Q3999860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958752$6992727C-DE80-4CAD-A75A-B1A2ED7432CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9579a4ebc8fc362938d3ee4c1626b4dbb8862f2","datavalue":{"value":{"entity-type":"item","numeric-id":4281483,"id":"Q4281483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958752$DB73CD6F-364E-4C89-8A72-19D52F2E51E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5333f404cb1c5a483ee97a9aa8db2143fb09170b","datavalue":{"value":{"entity-type":"item","numeric-id":4012879,"id":"Q4012879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958752$7C29DBAB-FBCF-4F21-AF2F-1CC043A5E9FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"33b4386780d936c0f81519e2931efa7025f3ef92","datavalue":{"value":{"entity-type":"item","numeric-id":4222777,"id":"Q4222777"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958752$2C2743F5-BF52-4F76-8D99-8F5E18AECB57","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"50cba2f7ff378d313a9a94ad6d6c129f25bdbb4f","datavalue":{"value":{"entity-type":"item","numeric-id":3024905,"id":"Q3024905"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b8550900687c702b342ece73642ce7dc629933d2","datavalue":{"value":{"amount":"+0.99999964","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5958752$AAF1241D-EA8A-4E0A-94E7-7B28251C633E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fb6a428810b63d9a8e9b31e51db48c75b9d37e25","datavalue":{"value":{"entity-type":"item","numeric-id":5220181,"id":"Q5220181"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"10977f7a92ff4dfad164c32407300c9e91f99f97","datavalue":{"value":{"amount":"+0.9289403","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5958752$7C541512-473F-46F8-ABAA-742CB5227AE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"43124411404d2318453998b106d7509bd2b1ddf0","datavalue":{"value":{"entity-type":"item","numeric-id":4934286,"id":"Q4934286"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1a82a63274a543ee634b5ccb7e24e49924fee6d4","datavalue":{"value":{"amount":"+0.88412416","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5958752$578F159E-7AC8-402E-9B68-FFB1565549D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a8800deab900094331a81eee100155fc5a422912","datavalue":{"value":{"entity-type":"item","numeric-id":5176985,"id":"Q5176985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"52b8a2447e44e3fa1a71b5e81478a6859c62f5b2","datavalue":{"value":{"amount":"+0.88012034","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5958752$68060238-BBB8-4EFE-BE28-478577B5F945","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3d45600584020335a72c3ddc443a298a60bc6978","datavalue":{"value":{"entity-type":"item","numeric-id":3142168,"id":"Q3142168"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d7b8ebb5f6ddd699a6aa794c5eb1cc991a27ea17","datavalue":{"value":{"amount":"+0.8788381","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5958752$2B83EBD3-02A4-4DBF-8ED3-78E6A92181E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"92e2dcdd0f509f9cffeec1bfe5b04951df141f44","datavalue":{"value":{"entity-type":"item","numeric-id":5493373,"id":"Q5493373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e617991bf0003af2643ce2c8eff078797f00ecf1","datavalue":{"value":{"amount":"+0.8729795","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5958752$E4B5120F-7153-4065-A8EA-9EEC167F829C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bfa699000a64677631072625f1ff24c948ef9db8","datavalue":{"value":{"entity-type":"item","numeric-id":674412,"id":"Q674412"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a30858393b362a0e45f945a0ac8d9f4c8899d149","datavalue":{"value":{"amount":"+0.87229216","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5958752$39D68371-3614-412B-A341-1426FA364857","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5958752","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5958752"}}}}}