Decidability of Several Concepts of Finiteness for Simple Types

• Autorzy: Santo José Espírito , Matthes Ralph , Pinto Luís

Identyfikatory

DOI

10.3233/FI-2019-1857

• Języki publikacji: EN

Abstrakty

EN

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 König’s lemma for simple types: a simple type has an infinite member exactly when the pruned search space is infinite.

Słowa kluczowe

EN

lambda calculus; proof search; coinduction; decision procedure

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2019
• Tom: Vol. 170, nr 1-3
• Strony: 111--138
• Opis fizyczny: Bibliogr. 10 poz., rys.

Twórcy

autor

Santo José Espírito

• Centro de Matemática, Universidade do Minho, Portugal

autor

Matthes Ralph

• Institut de Recherche en Informatique de Toulouse (IRIT), CNRS and University of Toulouse, France

autor

Pinto Luís

• Centro de Matemática, Universidade do Minho, Portugal

Bibliografia

• [1] Ben-Yelles CB. Type assignment in the lambda-calculus: syntax & semantics. Ph.D. thesis, University of College of Swansea, 1979. URL https://www.worldcat.org/oclc/59728610.
• [2] Hirokawa S. Infiniteness of proof(α) is polynomial-space complete. Theor. Comput. Sci., 1998. 206 (1-2):331-339. doi: 10.1016/S0304-3975(97)00168-0.
• [3] Espírito Santo J, Matthes R, Pinto L. A Coinductive Approach to Proof Search. In: Baelde D, Carayol A (eds.), Proc. of FICS 2013, volume 126 of EPTCS. 2013 pp. 28-43. doi:10.4204/EPTCS.126.3.
• [4] Espírito Santo J, Matthes R, Pinto L. A Coinductive Approach to Proof Search through Typed Lambda-Calculi, 2016. Only published online at URL http://arxiv.org/abs/1602.04382v2.
• [5] Espírito Santo J, Matthes R, Pinto L. Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search. Mathematical Structures in Computer Science, 2018. pp. 1-33. First View - volume not yet known. doi:10.1017/S0960129518000099.
• [6] Hindley JR. Basic Simple Type Theory, volume 42 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1997. ISBN:9780511608865.
• [7] Alves S, Broda S. A Unifying Framework for Type Inhabitation. In: Kirchner H (ed.), 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK, volume 108 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. ISBN 978-3-95977-077-4, 2018 pp. 5:1-5:16. doi:10.4230/LIPIcs.FSCD.2018.5.
• [8] Broda S, Damas L. On Long Normal Inhabitants of a Type. J. Log. Comput., 2005. 15(3):353-390. doi:10.1093/ logcom/exi016.
• [9] Takahashi M, Akama Y, Hirokawa S. Normal Proofs and Their Grammar. Inf. Comput., 1996. 125(2):144-153. doi:10.1006/inco.1996.0027.
• [10] Dudenhefner A, Rehof J. The Complexity of Principal Inhabitation. In: Miller D (ed.), 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK, volume 84 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. ISBN 978-3-95977-047-7, 2017 pp. 15:1-15:14. doi:10.4230/LIPIcs.FSCD.2017.15.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).