Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search
作者： José Espírito Santo , Luís Pinto , Ralph Matthes
DOI:
关键词: Representation (systemics) 、 Simply typed lambda calculus 、 Mathematical proof 、 Counting problem 、 Decision problem 、 Discrete mathematics 、 Calculus 、 Simple (abstract algebra) 、 Mathematics 、 Lambda calculus 、 Syntax (programming languages)
摘要: A new, comprehensive approach to inhabitation problems in simply-typed lambda-calculus is shown, dealing with both decision and counting problems. This works by exploiting a representation of the search space generated given problem, which terms for proof that authors developed recently. The may be seen as extending Curry-Howard proofs lambda-terms, staying within methods type systems. Our methodology reveals inductive descriptions problems, driven syntax proof-search expressions, end products are simple, recursive procedures functions.
arxiv.org
harvard.edu参考文章(10)
Pierre Bourreau, Sylvain Salvati, Game semantics and uniqueness of type inhabitance in the simply-typed λ-calculus international conference on typed lambda calculi and applications. ,vol. 6878, pp. 61- 75 ,(2011) , 10.1007/978-3-642-21691-6_8
S. Alves, S. Broda, A short note on type-inhabitation Information Processing Letters. ,vol. 115, pp. 908- 911 ,(2015) , 10.1016/J.IPL.2015.05.004
Sachio Hirokawa, Infiniteness of proof (a) is polynomial-space complete Theoretical Computer Science. ,vol. 206, pp. 331- 339 ,(1998) , 10.1016/S0304-3975(97)00168-0
Richard Statman, Intuitionistic propositional logic is polynomial-space complete Theoretical Computer Science. ,vol. 9, pp. 67- 72 ,(1979) , 10.1016/0304-3975(79)90006-9
Sabine Broda, Luís Damas, On Long Normal Inhabitants of a Type Journal of Logic and Computation. ,vol. 15, pp. 353- 390 ,(2005) , 10.1093/LOGCOM/EXI016
Masako Takahashi, Yohji Akama, Sachio Hirokawa, Normal Proofs and Their Grammar international conference on theoretical aspects of computer software. ,vol. 125, pp. 144- 153 ,(1994) , 10.1006/INCO.1996.0027
José Espírito Santo, Ralph Matthes, Luís Pinto, A Coinductive Approach to Proof Search arXiv: Logic in Computer Science. ,(2013) , 10.4204/EPTCS.126.3
Aleksy Andrzej Schubert, Wil Dekkers, Hendrik Pieter Barendregt, Automata Theoretic Account of Proof Search computer science logic. pp. 128- 143 ,(2015) , 10.4230/LIPICS.CSL.2015.128
José Espírito Santo, Luís Pinto, Ralph Matthes, A Calculus for a Coinductive Analysis of Proof Search ,(2016)
José Espírito Santo, Luís Pinto, Ralph Matthes, A Coinductive Approach to Proof Search through Typed Lambda-Calculi arXiv: Logic in Computer Science. ,(2016)