Third-order matching in the presence of type constructors

Autor:	Jan Springintveld
Rok vydání:	1995
Předmět:	Discrete mathematics TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Simply typed lambda calculus Computer science TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS System F Dependent type Typed lambda calculus Type constructor Lambda cube Pure type system Normalisation by evaluation
Zdroj:	Lecture Notes in Computer Science ISBN: 9783540590484 TLCA
DOI:	10.1007/bfb0014069
Popis:	We show that it is decidable whether a third-order matching problem in λω (an extension of the simply typed lambda calculus with type constructors) has a solution or not. We present an algorithm which, given such a problem, returns a solution for this problem if the problem has a solution and returns fail otherwise.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::d1512fb5daf0f087c29564ffa2d8ac40 https://doi.org/10.1007/bfb0014069 Zobrazit plný text záznamu