Decidability of several concepts of finiteness for simple types
| Autor: | Luís Pinto, José Espírito Santo, Ralph Matthes |
|---|---|
| Přispěvatelé: | University of Minho [Braga], Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, Centre National de la Recherche Scientifique (CNRS), 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. Concerning the second author, 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., ANR-11-BS02-0016,CLIMT,Méthodes catégoriques et logiques en transformations de modèles(2011), European Project: COST Action CA15123 ,COST - European Cooperation in Science and Technology,EUTYPES(2016), Universidade do Minho, Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT)-Toulouse Mind & Brain Institut (TMBI), Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT) |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
Decision procedure
Proof search Parameterized complexity 0102 computer and information sciences Type (model theory) Space (mathematics) 01 natural sciences Theoretical Computer Science Combinatorics Lemma (logic) Lambda-calculus 0101 mathematics Ciências Naturais::Matemáticas Simple (philosophy) Mathematics computer.programming_language Science & Technology Algebra and Number Theory 010102 general mathematics [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] lambda-calculus decision procedure proof search Outcome (probability) Decidability [MATH.MATH-LO]Mathematics [math]/Logic [math.LO] Computational Theory and Mathematics 010201 computation theory & mathematics Coinduction Lambda calculus computer coinduction Matemáticas [Ciências Naturais] Information Systems |
| Zdroj: | Fundamenta Informaticae Fundamenta Informaticae, IOS Press, 2019, 170 (1-3), pp.111-138. ⟨10.3233/FI-2019-1857⟩ Repositório Científico de Acesso Aberto de Portugal Repositório Científico de Acesso Aberto de Portugal (RCAAP) instacron:RCAAP Fundamenta Informaticae, 2019, 170 (1-3), pp.111-138. ⟨10.3233/FI-2019-1857⟩ |
| DOI: | 10.3233/FI-2019-1857⟩ |
| Popis: | 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. 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|