The paper presents a nondeterministic algorithm for unifying pairs of terms in equational theories consisting of a confluent and terminating set of rewrite rules. The algorithm, which can be considered a generalization of the standard unification algorithm by Martelli and Montanari, is described by means of transformations applied to sets of equations and is shown to be correct and complete. Another version of the algorithm, accepting also cyclic terms, is given for sets of multiequations. This algorithm is characterized by an outermost reduction strategy which permits dealing with infinite data structures. The algorithm can also be used as an interpreter for logic languages, thus providing a framework for trying to achieve the amalgamation of logic and functional languages.

ALGORITHM FOR UNIFICATION IN EQUATIONAL THEORIES / Martelli, A.; Moiso, C.; Rossi, G. F.. - In: TECHNICAL REPORTS - CSELT. - ISSN 0393-2648. - 14:6(1986), pp. 459-465.

ALGORITHM FOR UNIFICATION IN EQUATIONAL THEORIES

Rossi G. F.
1986

Abstract

The paper presents a nondeterministic algorithm for unifying pairs of terms in equational theories consisting of a confluent and terminating set of rewrite rules. The algorithm, which can be considered a generalization of the standard unification algorithm by Martelli and Montanari, is described by means of transformations applied to sets of equations and is shown to be correct and complete. Another version of the algorithm, accepting also cyclic terms, is given for sets of multiequations. This algorithm is characterized by an outermost reduction strategy which permits dealing with infinite data structures. The algorithm can also be used as an interpreter for logic languages, thus providing a framework for trying to achieve the amalgamation of logic and functional languages.
ALGORITHM FOR UNIFICATION IN EQUATIONAL THEORIES / Martelli, A.; Moiso, C.; Rossi, G. F.. - In: TECHNICAL REPORTS - CSELT. - ISSN 0393-2648. - 14:6(1986), pp. 459-465.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11381/2886320
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact