We argue that it is high time that types had a beneficial impact in the field of Answer Set Programming and in particular Disjunctive Datalog as exemplified by the DLV system. Things become immediately more challenging, as we wish to present a type system for DLV-Complex, an extension of DLV with uninterpreted function symbols, external implemented predicates and types. Our type system owes to the seminal polymorphic type system for Prolog introduced by Mycroft and O'Keefe, in the formulation by Lakshman and Reddy. The most innovative part of the paper is developing a declarative grounding procedure which is at the same time appropriate for the operational semantics of ASP and able to handle the new features provided by DLV-Complex. We discuss the soundness of the procedure and evaluate informally its success in reducing, as expected, the set of ground terms. This yields an automatic reduction in size and numbers of (non isomorphic) models. Similar results could have only been achieved in the current untyped version by careful use of generator predicates in lieu of types.
Towards a type discipline for answer set programming / C. Fiorentini, A. Momigliano, M. Ornaghi (LECTURE NOTES IN COMPUTER SCIENCE). - In: Types for Proofs and Programs / [a cura di] S. Berardi, F. Damiani, U. de' Liguoro. - Berlin : Springer, 2009. - ISBN 9783642024436. - pp. 117-135 (( convegno TYPES tenutosi a Torino nel 2008.
Towards a type discipline for answer set programming
C. FiorentiniPrimo
;A. MomiglianoSecondo
;M. OrnaghiUltimo
2009
Abstract
We argue that it is high time that types had a beneficial impact in the field of Answer Set Programming and in particular Disjunctive Datalog as exemplified by the DLV system. Things become immediately more challenging, as we wish to present a type system for DLV-Complex, an extension of DLV with uninterpreted function symbols, external implemented predicates and types. Our type system owes to the seminal polymorphic type system for Prolog introduced by Mycroft and O'Keefe, in the formulation by Lakshman and Reddy. The most innovative part of the paper is developing a declarative grounding procedure which is at the same time appropriate for the operational semantics of ASP and able to handle the new features provided by DLV-Complex. We discuss the soundness of the procedure and evaluate informally its success in reducing, as expected, the set of ground terms. This yields an automatic reduction in size and numbers of (non isomorphic) models. Similar results could have only been achieved in the current untyped version by careful use of generator predicates in lieu of types.File | Dimensione | Formato | |
---|---|---|---|
TYPE.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
316.75 kB
Formato
Adobe PDF
|
316.75 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.