In the version of logic programming (LP) based on interpretations where variables occur in atoms, a goal reduction via unification can be seen as a transition labelled by the most general unifier. Categorically, it is thus natural to model a logic program as a coalgebra. In the paper we represent: (i) goals as the substitutive monoid freely generated by the predicate symbols; (ii) the LTS as the structured coalgebra defined by the SOS rules implicit in the LP semantics; (iii) the bisimulation semantics of a logic program as its image on the final coalgebra.
A coalgebraic approach to unification semantics of logic programming
Bruni R.
;Montanari U.
;
2019-01-01
Abstract
In the version of logic programming (LP) based on interpretations where variables occur in atoms, a goal reduction via unification can be seen as a transition labelled by the most general unifier. Categorically, it is thus natural to model a logic program as a coalgebra. In the paper we represent: (i) goals as the substitutive monoid freely generated by the predicate symbols; (ii) the LTS as the structured coalgebra defined by the SOS rules implicit in the LP semantics; (iii) the bisimulation semantics of a logic program as its image on the final coalgebra.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
main.pdf
Open Access dal 01/12/2020
Descrizione: Articolo Principale
Tipologia:
Documento in Post-print
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
364.4 kB
Formato
Adobe PDF
|
364.4 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.