Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/62972
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Espírito Santo, José | por |
dc.contributor.author | Matthes, Ralph | por |
dc.contributor.author | Pinto, Luís F. | por |
dc.date.accessioned | 2020-01-07T09:35:50Z | - |
dc.date.available | 2020-01-07T09:35:50Z | - |
dc.date.issued | 2019-10 | - |
dc.identifier.issn | 0169-2968 | por |
dc.identifier.uri | https://hdl.handle.net/1822/62972 | - |
dc.description.abstract | If we consider as "member" of a simple type the outcome of any successful (possibly infinite) run of bottom-up proof search that starts from the type, then several concepts of "finiteness" for simple types are possible: the finiteness of the search space, the finiteness of any member, or the finiteness of the number of finite members (in other words, the inhabitants). In this paper we show that these three concepts are instances of the same parameterized notion of finiteness, and that a single, parameterized proof shows the decidability of all of them. One instance of this result means that termination of proof search is decidable. A separate result is that emptiness is also decidable (where emptiness is absence of "members" as above, not just absence of inhabitants). This fact is an ingredient of the main decidability result, but it also has a different application, the definition of the pruned search space - the one where branches leading to failure are chopped off. We conclude with our version of Konig's lemma for simple types: a simple type has an infinite member exactly when the pruned search space is infinite. | por |
dc.description.sponsorship | The first and third authors were partially financed by Portuguese Funds through FCT (Fundação para a Ciência e a Tecnologia) within the Project UID/MAT/00013/2013. The three authors were partially financed by COST action CA15123 EUTYPES. An early phase of the reported work was partially financed by the project Climt, ANR-11-BS02-016, of the French Agence Nationale de la Recherche. | por |
dc.language.iso | eng | por |
dc.publisher | IOS Press | por |
dc.relation | info:eu-repo/grantAgreement/FCT/5876/147370/PT | por |
dc.rights | openAccess | por |
dc.subject | Lambda-calculus | por |
dc.subject | Proof search | por |
dc.subject | Coinduction | por |
dc.subject | Decision procedure | por |
dc.title | Decidability of several concepts of finiteness for simple types | por |
dc.type | article | por |
dc.peerreviewed | yes | por |
dc.relation.publisherversion | https://content.iospress.com/articles/fundamenta-informaticae/fi1857 | por |
oaire.citationStartPage | 111 | por |
oaire.citationEndPage | 138 | por |
oaire.citationIssue | 1-3 | por |
oaire.citationVolume | 170 | por |
dc.identifier.eissn | 1875-8681 | por |
dc.identifier.doi | 10.3233/FI-2019-1857 | por |
dc.subject.fos | Ciências Naturais::Matemáticas | por |
dc.subject.wos | Science & Technology | por |
sdum.journal | Fundamenta Informaticae | por |
oaire.version | AM | por |
Aparece nas coleções: | CMAT - Artigos em revistas com arbitragem / Papers in peer review journals |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
DecidabilitySeveralConceptsFiniteness_Accepted.pdf | 379,91 kB | Adobe PDF | Ver/Abrir |