{"entities":{"Q809071":{"pageid":810919,"ns":120,"title":"Item:Q809071","lastrevid":49527736,"modified":"2026-01-07T12:24:44Z","type":"item","id":"Q809071","labels":{"en":{"language":"en","value":"Normalising the associative law: An experiment with Martin-L\u00f6f's type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4210117"}},"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":"Q809071$381DA39A-4E73-486B-AC30-F60A79FD54B4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1131b46c0e1aefff95132d8caf47f05589a60007","datavalue":{"value":{"text":"Normalising the associative law: An experiment with Martin-L\u00f6f's type theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q809071$32E3921E-1647-4296-ABA3-70A3C8C5BC6C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0de79176051ddfbc4d0bdcdaa90da7f76192bb65","datavalue":{"value":"0732.03023","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q809071$1C783D29-BF0A-47C1-AD24-1A1B5F056574","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"95cdd942c447e3bff3c51fa72817e0857b109c13","datavalue":{"value":"10.1007/BF01245632","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q809071$1723D295-7148-4DE3-A39D-A5B2916F7EAB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fa4fb3cd46cffa39aa0cc6ac06f9b61e1de70017","datavalue":{"value":{"entity-type":"item","numeric-id":809070,"id":"Q809070"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809071$4E05E598-BB10-43A5-A824-FBB059440292","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d9925518446645d219093152a820aba790417b61","datavalue":{"value":{"entity-type":"item","numeric-id":164203,"id":"Q164203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809071$BC2F8634-F437-4ACF-9C35-6B112BB62D2B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"391107ffc7a24346d69c573e292e4ff4587e3aaa","datavalue":{"value":{"time":"+1991-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q809071$FD0E97A7-06CB-44B2-BD42-CF35A6D5649E","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"844ff26e635ec3f5d750fd8c152e6653ce7aade3","datavalue":{"value":"In the wide class of programming logics, which can be ``external'' or ``integrated'', constructive or classical, with partial or total objects, based on primitive or general recursion, etc., Martin-L\u00f6f's type theory has an integrated constructive logic, total objects, and general recursion. The purpose of the present paper is to show how Martin-L\u00f6f's type theory, despite of its initial characteristics mentioned, can also be successfully used: (1) as an external logic for verifying the correctness of an external program; (2) to integrate different proof techniques, such as measure functions, well-founded recursion, or the separation of correctness into termination and partial correctness, in order to obtain a correct type theory program; (3) to perform program derivations on the basis of C. Paulson's proof checker ISABELLE, splitting the programming problem into a computational part and a logical part; (4) to illustrate the use of inductively defined types and predicates in connection with Martin-L\u00f6f's type theory, viewed as an open system, for giving a more direct problem representation (e.g., an external program represented as a graph) than encodings using well- orderings. The concrete problem to which these ideas are applied is that of normalizing semigroup expressions with respect to the associative law.","type":"string"},"datatype":"string"},"type":"statement","id":"Q809071$7F5C222C-7EA3-42C6-9188-D3C09AEF5066","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q809071$D9C9691C-8BB2-4EE6-A45D-481B6429E33A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q809071$EF6DB490-7048-4EDA-9334-CDD5A550E072","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8e3f40e3cc87753c4e0b7d7ce4bdc00805f626f","datavalue":{"value":"68N01","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q809071$1EA64F30-E770-480A-AD27-7A8DF9B205C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q809071$42C83340-5CD1-444F-B9E4-1DCC0EC7B7DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d8724ac1f861fd4485a474d1844744a1ace24834","datavalue":{"value":"03-04","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q809071$7689CD8F-D82E-4DAD-885E-C5BBFE53573E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q809071$67083CEE-245D-46D9-8CE1-D87E2BF2E5F1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d4178564d018348e391999398e1dea8933117c8c","datavalue":{"value":"4210117","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q809071$23ED4AE9-BE91-4A2F-947F-F0A2A3141A96","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"33775f26030d071074f6e677c78b2fdd4159a0c9","datavalue":{"value":"Martin-L\u00f6f's type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q809071$BA3CEC80-3038-41F1-9684-C4B35E99A1FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"af31523ac2adb05ca7a31f8f15a404f9e40f1d47","datavalue":{"value":"external logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q809071$35D8BBE5-F0D6-490D-9311-2213BC163FE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"297f3dafef9f073f382823168daaa5409e06b3fe","datavalue":{"value":"external program","type":"string"},"datatype":"string"},"type":"statement","id":"Q809071$AA86B20C-80D4-4ABF-97C9-BF279109E066","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"93e8b03c160cc7390eda9b9ee4f340ccdf8f41a8","datavalue":{"value":"measure functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q809071$4BCAD299-9657-4181-830B-3A17A2AFE75B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7b4d00175c26fd4259ca4fbd95fb41b33b7426b4","datavalue":{"value":"well-founded recursion","type":"string"},"datatype":"string"},"type":"statement","id":"Q809071$11543656-0B85-482B-BF4A-13DD858A5280","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f9ac4ef6ef6c5f8856ee80195276e724e0b6225a","datavalue":{"value":"correctness","type":"string"},"datatype":"string"},"type":"statement","id":"Q809071$573E6D78-04A0-4E23-959A-158F41457F52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9a544a5e05c05feee3d020879fbc561f7aa9f8c6","datavalue":{"value":"proof checker ISABELLE","type":"string"},"datatype":"string"},"type":"statement","id":"Q809071$919CAAEA-7033-4590-860A-51BBB63EF0AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e4811b1526aa16eb76a6d8564023eab9278416ac","datavalue":{"value":"inductively defined types","type":"string"},"datatype":"string"},"type":"statement","id":"Q809071$93D3DC30-1A79-4226-95A3-4B34AEC19886","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b8a3c5f3386d71a2dd235bedc48425de386f9558","datavalue":{"value":"normalizing semigroup expressions with respect to the associative law","type":"string"},"datatype":"string"},"type":"statement","id":"Q809071$07465080-3EE2-4B4D-B8B5-22037FDF10F4","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"ddfe26001cac27b44f73ee317c958b41c5d4e225","datavalue":{"value":{"entity-type":"item","numeric-id":585901,"id":"Q585901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809071$D9BBDF47-1B7B-4787-AF69-C6F8A7BF6461","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":"Q809071$114B22D4-2ECF-4EB6-A829-AAFF906BE383","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7931dc29f3e5a2a167917b66423fa0388ae2206f","datavalue":{"value":{"entity-type":"item","numeric-id":911744,"id":"Q911744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809071$1B42AC00-18F2-46CA-A879-8B2DD7EC98C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8124e2aa86067094dab23bb14b8dadf2e19d522b","datavalue":{"value":{"entity-type":"item","numeric-id":3894958,"id":"Q3894958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809071$0CA45930-CC1D-4EF0-8B7F-339C8CF7F248","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d592f87e8857ff4d106dd1dd178161f50c9229b","datavalue":{"value":{"entity-type":"item","numeric-id":1108266,"id":"Q1108266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809071$CBB23114-8675-47FA-9654-F26B966AADB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b6a55f23c5a67c2c9fd627d4bf85d3851ca0b09e","datavalue":{"value":{"entity-type":"item","numeric-id":913479,"id":"Q913479"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809071$39C01A44-D2CC-4A50-91C7-786FD603A76B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1420eb5b183c580e3eaa2025b4097787d860ff45","datavalue":{"value":{"entity-type":"item","numeric-id":1112584,"id":"Q1112584"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809071$078AA467-9A59-4190-9490-B6005B79D707","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":"Q809071$A861E227-DAE8-4C74-9EB2-967D12473B63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8849ca4e4f24816e3df0784725f3c70f4a983b0","datavalue":{"value":{"entity-type":"item","numeric-id":1101251,"id":"Q1101251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q809071$B7271FF4-1895-46FE-9E18-8BB8D6B562F4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dafebfd5e58bb74a87b62c1042cc11c64f5d7479","datavalue":{"value":{"entity-type":"item","numeric-id":5096234,"id":"Q5096234"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3610a2a170c9d6d7915f0f8992e3f5d16699ae4d","datavalue":{"value":{"amount":"+0.8093243837356567","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":"Q809071$D81B3249-EFDD-4353-95A4-0912B56EAF29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"318d6fb99941ebfef40dbeca7b4f5afc2330dae1","datavalue":{"value":{"entity-type":"item","numeric-id":3740203,"id":"Q3740203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c8da88e4096314b76dd9208cb141c34ca0b44ffd","datavalue":{"value":{"amount":"+0.7640635967254639","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":"Q809071$C47C0193-D01B-436E-B439-470A38F32251","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"803440e0a5d49c8240e6d385608a9346914ef6ca","datavalue":{"value":{"entity-type":"item","numeric-id":3512649,"id":"Q3512649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"65e142aed9048e595d825eeb54b8225676cb1614","datavalue":{"value":{"amount":"+0.759901762008667","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":"Q809071$FBAD3B6C-C32F-49B5-A63B-174D4CECFF7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cab0084298e0ce631281ff22039b1b13fafb24e3","datavalue":{"value":{"entity-type":"item","numeric-id":913479,"id":"Q913479"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5bf652efe76b8bb4b5f265bcc2c166743f6fd786","datavalue":{"value":{"amount":"+0.7489078044891357","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":"Q809071$2ED2DDB4-3E58-445D-B779-B3166BAB2B70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1783853632f9745006cbf567077c11a2f58c3648","datavalue":{"value":{"entity-type":"item","numeric-id":1097045,"id":"Q1097045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f00a7c716a8877641dd6e4104a077692b9dc7c54","datavalue":{"value":{"amount":"+0.7477611303329468","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":"Q809071$B624CCCD-4D36-4C53-8B36-AE12CF4FC722","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:809071","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:809071"}}}}}