{"entities":{"Q365669":{"pageid":367436,"ns":120,"title":"Item:Q365669","lastrevid":61278447,"modified":"2026-04-10T22:19:50Z","type":"item","id":"Q365669","labels":{"en":{"language":"en","value":"A decidable theory of type assignment"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6206979"}},"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":"Q365669$B4EF42F0-8055-413C-8FC1-56D1E21D8408","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"aeac50c5bb12d2673cd2953d6b96f69eb7ba4aab","datavalue":{"value":{"text":"A decidable theory of type assignment","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q365669$6B37F0CC-DE44-421A-B30F-D514103EF281","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"fd891b15d6f29b549d57c5b33c1fb2bc2b6b0d61","datavalue":{"value":"1303.03036","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q365669$F8664622-E49E-4F6E-B30E-DBA17023EE71","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e5dca68ae3ca1ab5ffee6b36b5daf704bfd3e306","datavalue":{"value":{"entity-type":"item","numeric-id":365668,"id":"Q365668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365669$215F40F6-2241-45D7-BFA2-741BB5F3A4BF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a0a7cd28a9f85b9c6ad57bd5bb1ae477bfe37846","datavalue":{"value":{"entity-type":"item","numeric-id":114337,"id":"Q114337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365669$4A4DE2FD-9EB7-4CD4-8B9C-706E6BCFC0DE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6e8c017497806797f217f1d658e3d224a2498206","datavalue":{"value":{"time":"+2013-09-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q365669$DB33F78E-2CDF-4ABF-83FC-1F634E72734A","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"2657b6fa49aacd7e7bd95cb28e5641952e2dad11","datavalue":{"value":"This is an important, interesting and well written paper. It's contents are well described in the author's abstract which I quote:   This article investigates a theory of type assignment (assigning types to lambda terms) called ETA which is intermediate in strength between the simple theory of type assignment and strong polymorphic theories like Girard's F [\\textit{J.-Y. Girard} et al., Proofs and types. Cambridge etc.: Univ. Press (1989; Zbl 0671.68002)]. It is like the simple type theory and unlike F in that the typability and type-checking problems are solvable with respect to ETA. This is proved in the article along with three other main results: (1) all primitive recusive functionals of finite type are representable in ETA; (2) every term typable in ETA has a unique normal form; (3) there is a function defined by \\(\\epsilon_0\\)-recursion which takes every typable term to a natural number which is an upper bound to the lengths of all \\(\\beta \\eta\\)-reduction sequences starting with that term.","type":"string"},"datatype":"string"},"type":"statement","id":"Q365669$EED988E6-C3B8-4E48-BB52-43F4A416B47A","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":"Q365669$2CCAECD4-7BC8-4887-9F26-424C396AAF44","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q365669$315FCE4C-9015-49E6-8ED4-203FB271CC55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"53a6dd9f6671ef90670f5c57fd3a10f9dadfeea8","datavalue":{"value":"03F10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q365669$45ABE793-2E9F-4B31-BB4D-C61612AAC36F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0fe54e63f18f963fab69457d7bb2e301bf5670ff","datavalue":{"value":"6206979","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q365669$2C102C20-51FF-4F66-A666-086B0B64AC08","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d06af1624b3b6a9c55a9019bd3b375b252a9fd85","datavalue":{"value":"type assignment","type":"string"},"datatype":"string"},"type":"statement","id":"Q365669$2E1C6FBD-C467-4448-9442-9BA65320B51D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b876698d821b50cd7ba02ddb5424ed80f1905d8","datavalue":{"value":"lambda calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q365669$17BD1BBD-E4F3-408C-A333-12A99299B81F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f903de259f92ddc007f9ac8964ddbe2d55fa9ae1","datavalue":{"value":"primitive recursive functionals","type":"string"},"datatype":"string"},"type":"statement","id":"Q365669$F92C251B-F62C-4A55-9BD2-B69887B20A4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"648a8b1a4ff287794c82684371a13fd38f951633","datavalue":{"value":"type reconstruction","type":"string"},"datatype":"string"},"type":"statement","id":"Q365669$579C9D08-98D6-4E67-BF3E-BE5C17B0F35C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3a4c07935a385e2ff679b7b381dad17af9f0ec4d","datavalue":{"value":"typability","type":"string"},"datatype":"string"},"type":"statement","id":"Q365669$88D677FD-2A44-44DE-B96B-ABFD63830517","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ba5620c65b3b1616ab8ae31e5468b0e08272974","datavalue":{"value":"type checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q365669$CCC4AA24-47A6-4506-A12D-35974A420E83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"51b336acc1a2a9943c1b7597223af4ac6fdba76c","datavalue":{"value":"reduction sequences","type":"string"},"datatype":"string"},"type":"statement","id":"Q365669$54C0C31F-F1D1-45C4-8E27-B05B072918F7","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9301974fbdbf3896f705a4c8ed840f169a9b63f","datavalue":{"value":{"entity-type":"item","numeric-id":19182,"id":"Q19182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365669$CA467CB0-452B-4AF1-BC3A-C77839052318","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":"Q365669$1257AC43-FA88-4285-A6DA-E91E4A0F8273","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ca3d05514231f1a0e3de40e0981a1e103df940bc","datavalue":{"value":"https://doi.org/10.1007/s00153-013-0335-x","type":"string"},"datatype":"url"},"type":"statement","id":"Q365669$46ACA682-AB72-460C-8324-242E2326DA6A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"321d8ee2e99c5af74bdcef817db31e371a272eb0","datavalue":{"value":"W1972202041","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q365669$36BE252C-9621-4C5D-ABB5-AEEB81326B6B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ddf4b357a0a94978ac349e24753f1162ff858b41","datavalue":{"value":{"entity-type":"item","numeric-id":2778814,"id":"Q2778814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365669$3028A5B1-0C4B-4C30-AF07-242B43CEC85C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"787e8787fc0800d23d78fddfd9bf35254e758553","datavalue":{"value":{"entity-type":"item","numeric-id":801050,"id":"Q801050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365669$E49CAD96-8CFF-4192-BF79-0F640807FBDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"367db641df6040a1f12d84299126da223d00ffc4","datavalue":{"value":{"entity-type":"item","numeric-id":2758058,"id":"Q2758058"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365669$67BB4777-B11D-4802-9A8A-60E685C0D9BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ae542aa49195da2f0564220c3e6d6c6c5762344","datavalue":{"value":{"entity-type":"item","numeric-id":769601,"id":"Q769601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365669$5A4C2D3F-15A1-4391-9D21-21032BE961BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77f473aa08523f9a9a313b9aaded66a723dd75c9","datavalue":{"value":{"entity-type":"item","numeric-id":2553958,"id":"Q2553958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365669$EA19EC48-C2BA-484E-A704-156822522FA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99c6176bcb92cea3bde43c51d54f8875f446d09c","datavalue":{"value":{"entity-type":"item","numeric-id":3994895,"id":"Q3994895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365669$3AF6B82D-C51C-4862-8948-2818D6994B2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d357a47c04e8c031646a6927518ecdcc37982e0","datavalue":{"value":{"entity-type":"item","numeric-id":3262780,"id":"Q3262780"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365669$9E06EB4D-75D3-4740-80F0-3C13C5500AF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cd22f0cc6d347d0883b044bb9468db1ab7dd5a3b","datavalue":{"value":{"entity-type":"item","numeric-id":4346206,"id":"Q4346206"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365669$444282E4-8725-4696-94BA-B852CB997A3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad9b6c837d9448bc2b136325c331db8629ab4909","datavalue":{"value":{"entity-type":"item","numeric-id":3522248,"id":"Q3522248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365669$119F9839-E53C-4F7D-ABF6-043C86C27D5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6629326274d1895876e66168171702b70b52bfc8","datavalue":{"value":{"entity-type":"item","numeric-id":4934564,"id":"Q4934564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365669$150AC7FA-939D-494F-BCB0-DA71B876E294","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3961712aa73d0d7e49904f6e1571dab96fdf8ac4","datavalue":{"value":{"entity-type":"item","numeric-id":3325707,"id":"Q3325707"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365669$4721DD40-E370-414A-8208-69A8C400867C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e085c4847c227118c61fb798400661bb25f4681f","datavalue":{"value":{"entity-type":"item","numeric-id":2639840,"id":"Q2639840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365669$978E6DFC-FADC-4A17-A9DB-54CD327503A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b7c3e6815cd921fc7767de9db6783bde242a686c","datavalue":{"value":{"entity-type":"item","numeric-id":4143279,"id":"Q4143279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365669$B5790319-C26E-42A6-BF8C-E5ABE7AEBAEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"377df7fa514ff36a47a0015fa9a23a509210ce4e","datavalue":{"value":{"entity-type":"item","numeric-id":453195,"id":"Q453195"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365669$5919BB2A-6DEB-40DB-915E-67FEE2024768","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"56327724d8101cacc3d4e5b36700dc86a7feb472","datavalue":{"value":{"entity-type":"item","numeric-id":4499084,"id":"Q4499084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365669$05B80EA1-C9CA-469E-A686-04E81B6549FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cac0238542245b8dba16f4222440bcd83dd0e8d5","datavalue":{"value":{"entity-type":"item","numeric-id":1302292,"id":"Q1302292"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365669$98E337D0-8C77-4DE3-89DB-09297BFBD14D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0536c7f714847d737e225c0d6ecfa3bc849700d3","datavalue":{"value":"10.1007/S00153-013-0335-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q365669$9AA82F3A-7470-4D65-8727-1A585EC0752E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3f6753be00154def372d1205039c03b3a9387227","datavalue":{"value":{"entity-type":"item","numeric-id":3988840,"id":"Q3988840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"771eee1b9b1b7cfe31e9b92e87edb0770e13ae3f","datavalue":{"value":{"amount":"+0.7769330143928528","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":"Q365669$56967E5F-8BA5-45EB-B638-5D4D9F72A8A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f2d809c196c39f2e163ea8fcf30b346cc6e52b3f","datavalue":{"value":{"entity-type":"item","numeric-id":4855295,"id":"Q4855295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2169718f53f06141ce353baa755ddffa35577556","datavalue":{"value":{"amount":"+0.7768160700798035","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":"Q365669$97EE4679-27DC-43B8-B6B1-3E3825A73F8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6df12bd06441d1e1b378440f506f98d13c164188","datavalue":{"value":{"entity-type":"item","numeric-id":1295368,"id":"Q1295368"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"47a716f94a721ff7e89d05b90e1928f9462200e2","datavalue":{"value":{"amount":"+0.7740082740783691","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":"Q365669$D7519E76-05AF-4BAB-B3EC-032FB73B8985","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e3f32cdd7b5e4ac2c40e2e965e295fc3f752a473","datavalue":{"value":{"entity-type":"item","numeric-id":3569027,"id":"Q3569027"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7a653179e928b338b8a98c62fcacf06038160f07","datavalue":{"value":{"amount":"+0.7727345824241638","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":"Q365669$83533D87-7F66-449B-8279-5D5749BBFF1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cedc5fc02249d7fe072d2dfa32926af06efc19c9","datavalue":{"value":{"entity-type":"item","numeric-id":1302292,"id":"Q1302292"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f5676005363dec32cd5fc58f41b767e4eaee56a8","datavalue":{"value":{"amount":"+0.7701323628425598","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":"Q365669$FEE3E671-3FC0-44DE-B03C-5EBD3C8BED8C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A decidable theory of type assignment","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_decidable_theory_of_type_assignment"}}}}}