We address the problem of complementing higher-order patterns without repetitions of existential variables. Differently from the first-order case, the complement of a pattern cannot, in general, be described by a pattern, or even by a finite set of patterns. We therefore generalize the simply-typed-calculus to include an internal notion of strict function so that we can directly express that a term must depend on a given variable.We show that, in this more expressive calculus, finite sets of patterns without repeated variables are closed under complement and intersection. Our principal application is the transformational approach to negation in higher-order logic programs.
Higher-order pattern complement and the strict lambda-calculus / A. Momigliano, F. Pfenning. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - 4:4(2003), pp. 493-529. [10.1145/937555.937559]
Higher-order pattern complement and the strict lambda-calculus
A. MomiglianoPrimo
;
2003
Abstract
We address the problem of complementing higher-order patterns without repetitions of existential variables. Differently from the first-order case, the complement of a pattern cannot, in general, be described by a pattern, or even by a finite set of patterns. We therefore generalize the simply-typed-calculus to include an internal notion of strict function so that we can directly express that a term must depend on a given variable.We show that, in this more expressive calculus, finite sets of patterns without repeated variables are closed under complement and intersection. Our principal application is the transformational approach to negation in higher-order logic programs.File | Dimensione | Formato | |
---|---|---|---|
HOPC.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
325.87 kB
Formato
Adobe PDF
|
325.87 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.