View Related Documents

Abstract

A lambda term is k-duplicating if every occurrence of a lambda abstractor binds at most k variable occurrences. We prove that the problem of higher order matching where solutions are required to be k-duplicating (but with no constraints on the problem instance itself) is decidable. We also show that the problem of higher order matching in the affine lambda calculus (where both the problem instance and the solutions are constrained to be 1-duplicating) is in NP, generalizing de Groote’s result for the linear lambda calculus [4].
Supported by KBN grant 8T 11C 04319

Fulltext Preview

Image of the first page of the fulltext document