Principles and Practice of Unification Factoring

Steven Dawson, C. R. Ramakrishnan, Steven Skiena, Terrance Swift

Research output: Contribution to journalArticle

Abstract

The efficiency of resolution-based logic programming languages, such as Prolog, depends critically on selecting and executing sets of applicable clause heads to resolve against subgoals. Traditional approaches to this problem have focused on using indexing to determine the smallest possible applicable set. Despite their usefulness, these approaches ignore the nondeterminism inherent in many programming languages to the extent that they do not attempt to optimize execution after the applicable set has been determined. Unification factoring seeks to rectify this omission by regarding the indexing and unification phases of clause resolution as a single process. This article formalizes that process through the construction of factoring automata. A polynomial-time algorithm is given for constructing optimal factoring automata that preserve the clause selection strategy of Prolog. More generally, when the clause selection strategy is not fixed, constructing such an optimal automaton is shown to be NP-complete, solving an open trie minimization problem. Unification factoring is implemented through a source code transformation that preserves the full semantics of Prolog. This transformation is specified in the article, and using it, several well-known programs show significant performance improvements across several different systems. A prototype of unification factoring is available by anonymous ftp.

Original languageEnglish (US)
Pages (from-to)528-563
Number of pages36
JournalACM Transactions on Programming Languages and Systems
Volume18
Issue number5
StatePublished - Sep 1996
Externally publishedYes

Fingerprint

Computer programming languages
Logic programming
Semantics
Polynomials

Keywords

  • D.3.4 [Programming Languages]: Processors - compilers; optimization
  • F.1.1 [Computation by Abstract Devices]: Models of Computation - automata

ASJC Scopus subject areas

  • Computer Graphics and Computer-Aided Design
  • Software

Cite this

Dawson, S., Ramakrishnan, C. R., Skiena, S., & Swift, T. (1996). Principles and Practice of Unification Factoring. ACM Transactions on Programming Languages and Systems, 18(5), 528-563.

Principles and Practice of Unification Factoring. / Dawson, Steven; Ramakrishnan, C. R.; Skiena, Steven; Swift, Terrance.

In: ACM Transactions on Programming Languages and Systems, Vol. 18, No. 5, 09.1996, p. 528-563.

Research output: Contribution to journalArticle

Dawson, S, Ramakrishnan, CR, Skiena, S & Swift, T 1996, 'Principles and Practice of Unification Factoring', ACM Transactions on Programming Languages and Systems, vol. 18, no. 5, pp. 528-563.
Dawson S, Ramakrishnan CR, Skiena S, Swift T. Principles and Practice of Unification Factoring. ACM Transactions on Programming Languages and Systems. 1996 Sep;18(5):528-563.
Dawson, Steven ; Ramakrishnan, C. R. ; Skiena, Steven ; Swift, Terrance. / Principles and Practice of Unification Factoring. In: ACM Transactions on Programming Languages and Systems. 1996 ; Vol. 18, No. 5. pp. 528-563.
@article{3afea4b6f7894e67a40719c8c237da87,
title = "Principles and Practice of Unification Factoring",
abstract = "The efficiency of resolution-based logic programming languages, such as Prolog, depends critically on selecting and executing sets of applicable clause heads to resolve against subgoals. Traditional approaches to this problem have focused on using indexing to determine the smallest possible applicable set. Despite their usefulness, these approaches ignore the nondeterminism inherent in many programming languages to the extent that they do not attempt to optimize execution after the applicable set has been determined. Unification factoring seeks to rectify this omission by regarding the indexing and unification phases of clause resolution as a single process. This article formalizes that process through the construction of factoring automata. A polynomial-time algorithm is given for constructing optimal factoring automata that preserve the clause selection strategy of Prolog. More generally, when the clause selection strategy is not fixed, constructing such an optimal automaton is shown to be NP-complete, solving an open trie minimization problem. Unification factoring is implemented through a source code transformation that preserves the full semantics of Prolog. This transformation is specified in the article, and using it, several well-known programs show significant performance improvements across several different systems. A prototype of unification factoring is available by anonymous ftp.",
keywords = "D.3.4 [Programming Languages]: Processors - compilers; optimization, F.1.1 [Computation by Abstract Devices]: Models of Computation - automata",
author = "Steven Dawson and Ramakrishnan, {C. R.} and Steven Skiena and Terrance Swift",
year = "1996",
month = "9",
language = "English (US)",
volume = "18",
pages = "528--563",
journal = "ACM Transactions on Programming Languages and Systems",
issn = "0164-0925",
publisher = "Association for Computing Machinery (ACM)",
number = "5",

}

TY - JOUR

T1 - Principles and Practice of Unification Factoring

AU - Dawson, Steven

AU - Ramakrishnan, C. R.

AU - Skiena, Steven

AU - Swift, Terrance

PY - 1996/9

Y1 - 1996/9

N2 - The efficiency of resolution-based logic programming languages, such as Prolog, depends critically on selecting and executing sets of applicable clause heads to resolve against subgoals. Traditional approaches to this problem have focused on using indexing to determine the smallest possible applicable set. Despite their usefulness, these approaches ignore the nondeterminism inherent in many programming languages to the extent that they do not attempt to optimize execution after the applicable set has been determined. Unification factoring seeks to rectify this omission by regarding the indexing and unification phases of clause resolution as a single process. This article formalizes that process through the construction of factoring automata. A polynomial-time algorithm is given for constructing optimal factoring automata that preserve the clause selection strategy of Prolog. More generally, when the clause selection strategy is not fixed, constructing such an optimal automaton is shown to be NP-complete, solving an open trie minimization problem. Unification factoring is implemented through a source code transformation that preserves the full semantics of Prolog. This transformation is specified in the article, and using it, several well-known programs show significant performance improvements across several different systems. A prototype of unification factoring is available by anonymous ftp.

AB - The efficiency of resolution-based logic programming languages, such as Prolog, depends critically on selecting and executing sets of applicable clause heads to resolve against subgoals. Traditional approaches to this problem have focused on using indexing to determine the smallest possible applicable set. Despite their usefulness, these approaches ignore the nondeterminism inherent in many programming languages to the extent that they do not attempt to optimize execution after the applicable set has been determined. Unification factoring seeks to rectify this omission by regarding the indexing and unification phases of clause resolution as a single process. This article formalizes that process through the construction of factoring automata. A polynomial-time algorithm is given for constructing optimal factoring automata that preserve the clause selection strategy of Prolog. More generally, when the clause selection strategy is not fixed, constructing such an optimal automaton is shown to be NP-complete, solving an open trie minimization problem. Unification factoring is implemented through a source code transformation that preserves the full semantics of Prolog. This transformation is specified in the article, and using it, several well-known programs show significant performance improvements across several different systems. A prototype of unification factoring is available by anonymous ftp.

KW - D.3.4 [Programming Languages]: Processors - compilers; optimization

KW - F.1.1 [Computation by Abstract Devices]: Models of Computation - automata

UR - http://www.scopus.com/inward/record.url?scp=0030246077&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0030246077&partnerID=8YFLogxK

M3 - Article

VL - 18

SP - 528

EP - 563

JO - ACM Transactions on Programming Languages and Systems

JF - ACM Transactions on Programming Languages and Systems

SN - 0164-0925

IS - 5

ER -