Searching for just a few words should be enough to get started. If you need to make more complex queries, use the tips below to guide you.
Issue title: Types, terms and reductions: A special issue dedicated to Paweł Urzyczyn for his 65th birthday
Guest editors: Thorsten Altenkirch and Aleksy Schubert
Article type: Research Article
Authors: Santo, José Espíritoa | Matthes, Ralphb; * | Pinto, Luísc
Affiliations: [a] Centro de Matemática, Universidade do Minho, Portugal. jes@math.uminho.pt | [b] Institut de Recherche en Informatique de Toulouse (IRIT), CNRS and University of Toulouse, France. ralph.matthes@irit.fr | [c] Centro de Matemática, Universidade do Minho, Portugal. luis@math.uminho.pt
Correspondence: [*] Address for correspondence: IRIT - Université Paul Sabatier, 118 route de Narbonne, F-31062 Toulouse Cedex 9, France
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 König’s lemma for simple types: a simple type has an infinite member exactly when the pruned search space is infinite.
Keywords: lambda-calculus, proof search, coinduction, decision procedure
DOI: 10.3233/FI-2019-1857
Journal: Fundamenta Informaticae, vol. 170, no. 1-3, pp. 111-138, 2019
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
USA
Tel: +1 703 830 6300
Fax: +1 703 830 2300
sales@iospress.com
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
IOS Press
Nieuwe Hemweg 6B
1013 BG Amsterdam
The Netherlands
Tel: +31 20 688 3355
Fax: +31 20 687 0091
info@iospress.nl
For editorial issues, permissions, book requests, submissions and proceedings, contact the Amsterdam office info@iospress.nl
Inspirees International (China Office)
Ciyunsi Beili 207(CapitaLand), Bld 1, 7-901
100025, Beijing
China
Free service line: 400 661 8717
Fax: +86 10 8446 7947
china@iospress.cn
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
如果您在出版方面需要帮助或有任何建, 件至: editorial@iospress.nl