Please use this identifier to cite or link to this item: http://hdl.handle.net/1822/62948

TitleInhabitation in simply typed lambda-calculus through a lambda-calculus for proof search
Author(s)Espírito Santo, José
Matthes, Ralph
Pinto, Luís F.
Issue date2019
PublisherCambridge University Press
JournalMathematical Structures in Computer Science
Abstract(s)A new approach to inhabitation problems in simply typed lambda-calculus is shown, dealing with both decision and counting problems. This approach works by exploiting a representation of the search space generated by a given inhabitation problem, which is in terms of a lambda-calculus for proof search that the authors developed recently. The representation may be seen as extending the Curry-Howard representation of proofs by lambda terms. Our methodology reveals inductive descriptions of the decision problems, driven by the syntax of the proof-search expressions, and produces simple, recursive decision procedures and counting functions. These allow to predict the number of inhabitants by testing the given type for syntactic criteria. This new approach is comprehensive and robust: based on the same syntactic representation, we also derive the state-of-the-art coherence theorems ensuring uniqueness of inhabitants.
TypeArticle
URIhttp://hdl.handle.net/1822/62948
DOI10.1017/S0960129518000099
ISSN0960-1295
e-ISSN1469-8072
Peer-Reviewedyes
AccessOpen access
Appears in Collections:CMAT - Artigos em revistas com arbitragem / Papers in peer review journals

Files in This Item:
File Description SizeFormat 
InhabitationThroughALambdaCalculusForProofSearch_Accepted.pdf425,48 kBAdobe PDFView/Open

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID