{"entities":{"Q1362341":{"pageid":1373080,"ns":120,"title":"Item:Q1362341","lastrevid":46502310,"modified":"2025-12-24T22:26:37Z","type":"item","id":"Q1362341","labels":{"en":{"language":"en","value":"A completeness theorem for the expressive power of higher-order algebraic specifications"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1042935"}},"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":"Q1362341$D75CDF3A-E6F2-4739-A819-B4324D4C951C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c682d8cd0c8a8d98f5ea8414d7473cb5d0ae95bf","datavalue":{"value":{"text":"A completeness theorem for the expressive power of higher-order algebraic specifications","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1362341$231751AE-25FE-4B65-9AEF-84D10EC23ED0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5eb0dbeb694172ba7d88418b1a74ee2a1d4ac349","datavalue":{"value":"0906.68095","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1362341$E33512E6-A51F-4271-B59B-E3F852DF4154","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ac0321a6b6d5d899ea1927f671b46847c41412c0","datavalue":{"value":{"entity-type":"item","numeric-id":671656,"id":"Q671656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1362341$1E7502CC-4DFD-4655-AD7D-3A268011FFE6","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3340243f57e05f2265c56423c388055a14b114fa","datavalue":{"value":{"entity-type":"item","numeric-id":107189,"id":"Q107189"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1362341$B18CE97D-C957-4068-BABB-DD16EB69BDC9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"451eaac90d556e3bb1fbaacc54883bdf2eca0280","datavalue":{"value":{"time":"+1999-02-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":"Q1362341$D1ABFD44-7C72-4655-839E-662D81C41E2E","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b2384683c0c27969e02c31f1f6a2c8e162d0536b","datavalue":{"value":"This paper is dedicated to a significant section of universal algebra. This section is related to a research of the expressive power of a general form of higher-order algebraic specification which allows constructors and hidden sorts and operations. It is possible to summarize the situation for first-order algebraic specifications as follows:   (i) recursive or recursively enumerable sets of first-order equations, together with first-order initial semantics, can specify precisely the countable minimal algebras of complexity \\(\\Sigma^0_1\\);   (ii) recursive or recursively enumerable sets of first-order equations, together with first-order final semantics, can specify precisely the countable minimal algebras of complexity \\(\\Pi^0_1\\).   The results of this paper deal with higher-order equational specifications which allow a subsignature of constructors, as well as hidden sorts and operations. Since any partial recursive function is recursively first-order axiomatizable and the quantifier functional is finitely second-order axiomatizable we obtain the main result of this paper.   Completeness Theorem. For any countable \\(S\\)-sorted signature \\(\\Sigma\\) and any minimal algebra \\(A\\), \\(A\\) has complexity \\(\\Pi^1_1\\) if and only if, there exists a recursive second-order equational specification Spec with constructors and hidden sorts and operations such that Spec specifies \\(A\\) under higher-order initial semantics. This theorem precisely characterizes the expressive power of a very general form of higher-order algebraic specification. Its proof also gives deeper insight into the role of the quantifier functional and, thus, into the relationship between constructive and nonconstructive higher-order specifications. This theme forms one of the cornerstones of the theory of higher-order algebraic specification and is taken up by the author in Higher-order equational logic for specification, simulation and testing [Proc. Second Int. Workshop on Higher-order Algebra, Logic and Term rewriting, HOA '95 (1995)].","type":"string"},"datatype":"string"},"type":"statement","id":"Q1362341$55BF8CDE-D47E-4278-8E3F-F714B3D3E219","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1362341$452E7115-3EB0-442F-ADFB-4FC0155BBD72","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"243020a419ce8fd74acac783f1fbe621230529f1","datavalue":{"value":"1042935","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1362341$CA39BA85-5B2C-4192-813F-59C5E21A25EC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09a188bc590546995974b55a3f2f84f00e08b2a9","datavalue":{"value":"universal algebra","type":"string"},"datatype":"string"},"type":"statement","id":"Q1362341$A96A3059-D173-4771-904F-FEE948F9E2DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66b2276908255ab0fe38e919717094768bd78cb3","datavalue":{"value":"equational specifications","type":"string"},"datatype":"string"},"type":"statement","id":"Q1362341$869181ED-9B34-4FCF-915F-CFAC7C0BAA6D","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"3859f4276ff033961b0a9f9512659b83adf9ab34","datavalue":{"value":{"entity-type":"item","numeric-id":1251890,"id":"Q1251890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1362341$FAEBA1CB-1CA6-45B7-9158-060CE9210215","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":"Q1362341$E3064255-3C14-4DCF-9D22-FCDED231036B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"498dc9fed3b68adac1c6a681dc42fee7f5dd01c0","datavalue":{"value":"https://doi.org/10.1006/jcss.1997.1489","type":"string"},"datatype":"url"},"type":"statement","id":"Q1362341$EB0B3161-8A82-4570-A354-9DEA0FC252A7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5dca54661fb253a30c4df362becf7aa9a9289410","datavalue":{"value":"W2047222889","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1362341$53A84A62-E55B-47F5-B290-329CDFB89839","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4cc88c84e5f2f7ead4bb196346ee40f80dd92c9","datavalue":{"value":{"entity-type":"item","numeric-id":3854601,"id":"Q3854601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1362341$3D31E9CB-A913-4F34-851B-C5BDD53AAC03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"062e6b60e77749216114d35202f5ce2c55314034","datavalue":{"value":{"entity-type":"item","numeric-id":3659115,"id":"Q3659115"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1362341$B0AB606F-D957-473E-9D7F-AABDBA1B6447","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c6162a47706be814c34042fd00c7c48b95d112be","datavalue":{"value":{"entity-type":"item","numeric-id":3662597,"id":"Q3662597"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1362341$DCF8BAE4-601D-4838-9BF8-07A4BF294FC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3744dcf2bce65710124275d29816dcca108a9baf","datavalue":{"value":{"entity-type":"item","numeric-id":1098613,"id":"Q1098613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1362341$46771BFC-5CD7-4156-BB4F-8785964A21EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"35f820e9c2b45f8f035a710ad26c0ff0e5c7ae48","datavalue":{"value":{"entity-type":"item","numeric-id":3221381,"id":"Q3221381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1362341$6FA0F3CC-5ABD-469D-B883-A7AAEE4AB947","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9c583b65c7819a91d7f03c50f27e11283eee826","datavalue":{"value":{"entity-type":"item","numeric-id":3962973,"id":"Q3962973"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1362341$31FBD570-D2A0-43A6-8CC6-B806E7722FCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f170d1bf622491cb6b4b793c7af31a789e14e59","datavalue":{"value":{"entity-type":"item","numeric-id":3687683,"id":"Q3687683"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1362341$D763AF4E-C612-45E9-8035-6CE5273965B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"287785aa8651b26f912f2bcca2b2a743939d591e","datavalue":{"value":{"entity-type":"item","numeric-id":4146722,"id":"Q4146722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1362341$95E8548E-533C-4C57-9176-7B79B5C9704E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"59dd6707e2d45afafa6c2faf7d6f9346e75471bc","datavalue":{"value":{"entity-type":"item","numeric-id":1908358,"id":"Q1908358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1362341$DF5D301E-A8FC-4013-832A-5538E066B8F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9e6164d85c4694c71a8983f1c45bf387f665fdff","datavalue":{"value":{"entity-type":"item","numeric-id":1199827,"id":"Q1199827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1362341$4020EC2D-63AD-4265-912D-0315942D6D83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"24550d4771f4bba1e3d8f7c78145cbc8cd2d8a5b","datavalue":{"value":{"entity-type":"item","numeric-id":4693763,"id":"Q4693763"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1362341$0F9D9205-BE24-4298-8EDC-9A3BF70A76C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c5bcd491d9610072b36fb1c41ffbbd04da04e521","datavalue":{"value":{"entity-type":"item","numeric-id":1338890,"id":"Q1338890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1362341$A3AA7C3E-11E2-4C42-BEF0-2BC01A19F1B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"73ab258ce3a93d04948c8705462f3fcde707422c","datavalue":{"value":{"entity-type":"item","numeric-id":5950718,"id":"Q5950718"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1362341$D87EB904-9DEB-4279-AF81-46E4E303F3FC","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"35aef9888885674e21de0a2f9fb13e252256aa89","datavalue":{"value":"10.1006/JCSS.1997.1489","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1362341$8FB3309C-6627-49FD-873A-AA8DA83E27D5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bf478011c9e08dd09f491ddb07a93553038cfffa","datavalue":{"value":{"entity-type":"item","numeric-id":1908358,"id":"Q1908358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8eb50833f8093fc810ae067421b6c836b99d77d6","datavalue":{"value":{"amount":"+0.849857747554779","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":"Q1362341$0544297A-ED35-4A70-BA5D-291CC02FC06E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"de29032dda050c9cc902761205606afae50eeb17","datavalue":{"value":{"entity-type":"item","numeric-id":3976053,"id":"Q3976053"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"54ae4b34bd26aa827bf5bd593c793569e7463d96","datavalue":{"value":{"amount":"+0.8060335516929626","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":"Q1362341$15BFA9C0-04D5-420F-95A7-29A33952F2B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"26dbdf6a93ec5578639b6f20165eaf60a81f4554","datavalue":{"value":{"entity-type":"item","numeric-id":1338890,"id":"Q1338890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fdc7383e2fd8016e91193b82f33aa40c460d8dbd","datavalue":{"value":{"amount":"+0.7982077598571777","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":"Q1362341$5BD23B2F-29D1-4003-B3E1-C64FE9D3ED89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0a7eba7b04dd5f01cda67c9197e6febeb9fa4a63","datavalue":{"value":{"entity-type":"item","numeric-id":3028333,"id":"Q3028333"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5005fdc3576939940033fda13cd6deefd46fb393","datavalue":{"value":{"amount":"+0.7724139094352722","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":"Q1362341$448F2C36-2BD1-4910-8B2F-DBBDD4C09F61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2c076049921ba69fdc841933c89532c018c305b6","datavalue":{"value":{"entity-type":"item","numeric-id":3809236,"id":"Q3809236"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a7b1053a8f2e43943b4f95665601b3ea510e9958","datavalue":{"value":{"amount":"+0.7708390355110168","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":"Q1362341$216DFA5C-873A-4E88-A02D-F5C16479E9F9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1362341","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1362341"}}}}}