1: \documentclass{tlp}

2: \usepackage{eepic}

3: \usepackage{epic}

4: \usepackage{latexsym}

5: 

6: %\newcommand{\subs}[3]{[#1/#2]#3}

7: 

8: \long\def\ignore#1{}

9: 

10: \newcommand{\ra}{\rightarrow}

11: \newcommand{\lra}{\longrightarrow}

12: \newcommand{\sep}{\;\vert\;}

13: \newcommand{\app}{{\ }}

14: \newcommand{\lambdax}[1]{\lambda #1 \, }

15: \newcommand{\allx}[1]{\forall #1 \,}

16: \newcommand{\somex}[1]{\exists #1 \,}

17: 

18: \newcommand{\subfor}[3]{#3[#2 := #1]}

19: \newcommand{\tup}[1]{{\langle#1\rangle}}

20: 

21: \newcommand{\dum}[1]{@ #1}

22: \newcommand{\lenv}{{\lbrack\!\lbrack}}

23: \newcommand{\renv}{{\rbrack\!\rbrack}}

24: \newcommand{\env}[1]{{\lenv #1 \renv}}

25: 

26: \newcommand{\pderivation}{{$\cal P$}\kern -.1em\hbox{-derivation}}

27: \newcommand{\pderivable}{{$\cal P$}\kern -.1em\hbox{-derivable}}

28: \newcommand{\simpl}{{\it SIMPL}}

29: \newcommand{\match}{{\it MATCH}}

30: \newcommand{\failed}{{\bf F}}

31: \newcommand{\Pscr}{{\cal P}}

32: \newcommand{\Gscr}{{\cal G}}

33: \newcommand{\Dscr}{{\cal D}}

34: 

35: \newcommand{\ie}{{\em i.e.}}

36: \newcommand{\eg}{{\em e.g.}}

37: 

38: 

39: \newtheorem{exno}{Example}[section]

40: 

41: \newenvironment{example}{\refstepcounter{exno}\medskip \noindent {\bf

42: Example \theexno.\ }}{\hspace*{\fill}$\Box$\medskip} 

43: 

44: \newtheorem{defno}{Definition}[section]

45: 

46: \newenvironment{defn}{\refstepcounter{defno}\medskip \noindent {\bf

47: Definition \thedefno.\ }}{\hspace*{\fill}$\Box$\medskip}

48: 

49: %\newcommand{\all}{\forall}

50: %\newcommand{\some}{\exists}

51: %\newcommand{\somex}[1]{\exists #1 \,}

52: %\renewcommand{\neg}{\mathord\sim}

53: 

54: \newcommand{\etc}{{\em etc}}

55: 

56: 

57: \begin{document}

58: 

59: %\bibliographystyle{acmtrans}

60: 

61: \title[A Treatment of Higher-Order Features in Logic Programming]

62: {A Treatment of Higher-Order\\ Features in Logic Programming}

63: 

64: \author[G. Nadathur]

65: {GOPALAN NADATHUR\thanks{This work has been partially supported by the

66:     National Science Foundation under Grants CCR-9803849 and

67:     CCR-0096322. Support was also received from the Digital Technology

68:     Center and the Department of Computer Science and Engineering at

69:     the University of Minnesota. The final version of the paper was

70:     prepared during a sabbatical visit to the Protheo

71:     group at LORIA and INRIA, Nancy.}\\

72: Digital Technology Center and Department of Computer Science and Engineering\\

73: University of Minnesota\\

74: 4-192 EE/CS Building, 200 Union Street S.E.\\

75: Minneapolis, MN 55455\\

76: E-mail: gopalan@cs.umn.edu

77: }

78: 

79: 

80: \maketitle

81: 

82: \begin{abstract}

83: 

84: The logic programming paradigm provides the basis for a new

85: intensional view of higher-order notions. This view is realized

86: primarily by employing the terms of a typed lambda calculus as

87: representational devices and by using a richer form of unification

88: for probing their structures.  These additions have important

89: meta-programming applications but they also pose non-trivial

90: implementation problems. One issue concerns the machine representation

91: of lambda terms suitable to their intended use: an adequate encoding

92: must facilitate comparison operations over terms in addition to

93: supporting the usual reduction computation. Another aspect relates to

94: the treatment of a unification operation that has a branching

95: character and that sometimes calls for the delaying of the solution of

96: unification problems. A final issue concerns the execution of goals

97: whose structures become apparent only in the course of computation.

98: These various problems are exposed in this paper and solutions to them

99: are described. A satisfactory representation for lambda terms is

100: developed by exploiting the nameless notation of de Bruijn as well as

101: explicit encodings of substitutions. Special mechanisms are

102: molded into the structure of traditional Prolog implementations to

103: support branching in unification and carrying of unification

104: problems over other computation steps; a premium is placed in this

105: context on exploiting determinism and on emulating usual first-order

106: behaviour. An extended compilation model is presented that

107: treats higher-order unification and also handles dynamically emergent

108: goals. The ideas described here have been employed in the {\it Teyjus}

109: implementation of the $\lambda$Prolog language, a fact that is used to

110: obtain a preliminary assessment of their efficacy.

111: 

112: \end{abstract}

113: 

114: \begin{keywords}

115: lambda calculus, intensional higher-order

116: programming, higher-order unification, abstract machine, compilation

117: \end{keywords}

118: 

119: \section{Introduction}\label{sec:intro}

120: 

121: Customary acquaintance with higher-order notions in programming

122: relates to the imperative or functional programming paradigms. Within

123: these frameworks, functions are equated with the methods for computing

124: that are embodied in procedures. Higher-orderness then consists of the

125: ability to objectify such functions and, thereby, to embed them in

126: data or pass them as arguments to other functions. Many interesting

127: applications have been found for such capabilities. However, all of

128: these are dependent on a uniform {\it extensional} view of functions.

129: In particular, the only observable aspect of such objects is their

130: ability to transform given arguments into result values.

131: 

132: Logic programming has the potential for supporting a different and

133: more sophisticated understanding of higher-order notions

134: \cite{NM98}. Functions are used within this paradigm as a means for

135: constructing descriptions of objects. Such descriptions can be

136: examined by means of unification, an operation that is useful in the

137: analysis of {\it intensions}. Traditional logic programming languages

138: manifest a weak exploitation of this capability because they

139: permit only individual, non-function, objects as values. However, it

140: is possible to support the probing of function structure in genuinely

141: higher-order ways by introducing a mechanism such as the terms of a

142: lambda calculus for encoding function objects and by complementing

143: this with richer notions of variables and unification.  The usual form

144: of higher-order programming can be realized simply by using the

145: ability to represent function valued objects and the extensional

146: interpretation built into logic programming of one kind of function,

147: namely, predicates. The richer intensional view of functions offers,

148: in addition, many possibilities that have not been systematically

149: supported by any previous programming paradigm. To consider one 

150: important direction, the ability to use lambda terms as

151: representational devices lends itself well to an abstract view of

152: syntax that treats binding notions explicitly \cite{MN87slp,PE88pldi},

153: leading thereby to many novel metalanguage applications for logic

154: programming (\eg, see 

155: \cite{AppFel99,Felty93jar,hannan92lics,Pfe88,HM92mscs}). 

156: 

157: While there is considerable application potential for higher-order

158: features in logic programming, the addition of such features also

159: raises significant implementation problems.  One category of problems

160: arises from the use that is made of the terms of a lambda calculus

161: essentially as data structures. This is a truly novel role for such

162: terms in programming, and a representation must be developed for them

163: that supports their use in this capacity. A satisfactory representation

164: should permit the examination of term structure and must facilitate

165: the comparison of terms in a situation where the particular names of

166: bound variables are unimportant, in addition to efficiently supporting

167: the usual reduction operation on terms. Another class of problems

168: relates to the fact that the unification computation on lambda terms,

169: known as higher-order unification \cite{Huet75}, possesses

170: characteristics that are distinct from those of the customary

171: first-order unification. In particular, performing this operation may

172: involve a branching search and it may also be necessary to temporarily

173: `suspend' the computation before a unifier is found. 

174: Suitable dynamic support must be described for both facets. 

175: A third aspect that needs special consideration is the mixing of

176: intensional and extensional views of predicate objects. There is a

177: distinction between examining the structure of an object and using

178: this structure to determine the invocation of code.  A satisfactory

179: method must be provided for realizing the switch between these

180: roles. Finally, any machinery that is designed for supporting the new

181: features 

182: must be interwoven into the run-time devices and approaches to

183: compilation that are commonly used in logic programming

184: implementation. The proper combination of all these mechanisms in one

185: system is itself a non-trivial issue.  

186: 

187: We consider all these problems in this paper and we develop

188: methods for addressing them. For the sake of concreteness, we describe

189: our new implementation ideas within the

190: framework of the Warren Abstract Machine (WAM) \cite{War83}, a popular

191: vehicle for realizing logic programming languages.  One of our

192: contributions relates to the representation of lambda

193: terms. We carefully identify the different issues that

194: become relevant where these terms are used intensionally and we

195: develop an encoding for them that utilizes mechanisms for eliminating

196: bound variable names \cite{debruijn72} and for capturing substitutions

197: in terms \cite{NW98tcs} towards addressing these issues. We also

198: outline a low-level realization of such an encoding and we discuss

199: the integration of operations on these terms into an abstract machine

200: structure.  Another contribution is the development of machinery for

201: supporting the special needs of higher-order unification.  In this

202: direction we, first of all, describe an explicit encoding of

203: unification problems that exploits the manner in which these evolve to

204: foster sharing in their representation.  We also propose mechanisms

205: that are suitable for realizing branching in unification through a

206: depth-first search regimen with the possibility of backtracking.

207: Finally, recognizing that branching search is, in general,

208: computationally expensive, we describe a processing structure that

209: facilitates the application of special deterministic steps and that

210: delays the consideration of branching until after such steps. Using

211: this approach it is possible to treat first-order

212: unification almost exactly as it would be treated in a Prolog

213: implementation, a facet recognized to be important even in

214: higher-order programs \cite{MP92}. The final contribution of this

215: paper relates to compilation. We propose enhancements to the structure

216: of the WAM and modifications to its instruction set that together

217: realize a compiled execution of programs in a higher-order

218: language. We also outline in this context a treatment of the 

219: transition between intensional and extensional roles of predicates. 

220: 

221: The ideas that we develop in this paper have a special practical

222: relevance: they are useful to the implementation of the logic

223: programming language $\lambda$Prolog \cite{NM88}. This language

224: actually embodies two extensions to a Prolog-like language in addition

225: to the higher-order features considered here. In one direction, it

226: makes richer use of logical connectives and quantifiers to introduce

227: notions of scoping \cite{MNPS91}. In another direction, it includes a

228: polymorphic typing regimen \cite{NP91}. Both aspects raise new

229: questions for implementation that we have addressed elsewhere

230: \cite{KNW92,NJK94}. The machinery that we describe here blends well

231: with these other mechanisms and all our ideas have, in fact, been

232: amalgamated in a new implementation of $\lambda$Prolog called {\it

233: Teyjus} \cite{NM99cade}.

234: 

235: The rest of this paper is structured as follows.  In the next section

236: we identify a logic programming language that embodies the

237: higher-order features that are presently of interest and we

238: characterize computation in this language. 

239: In Section~\ref{sec:interp}, we refine the description of computation

240: into one that provides the basis for implementation by outlining the

241: structure of the higher-order unification operation and using

242: this to develop an abstract interpreter for the language.

243: The remainder of this paper concerns a low-level

244: realization of this interpreter. In Section~\ref{sec:terms}, we

245: discuss issues relevant to the representation of lambda terms and

246: distill from this an encoding for them that can be used in an actual

247: implementation. The following section integrates our term

248: representation into an overall computational model and proposes new

249: machinery for the realization of higher-order unification.

250: Section~\ref{sec:abstmachine} makes explicit an extended abstract

251: machine structure and considers the compilation of first-order

252: like unification as well as the treatment of higher-order aspects

253: relative to  

254: this machine. Section~\ref{sec:conc} discusses related work and

255: concludes the paper.

256: 

257: \section{A Higher-Order Language}\label{sec:hohc}

258: 

259: The logical language whose implementation we consider in this paper is

260: an analogue within Church's Simple Theory of Types

261: \cite{Church40} of the Horn clause language that underlies

262: Prolog. Church's 

263: logic is one that builds on a typed lambda calculus. In the

264: interpretation we use here, the types are constructed from given sets

265: of sorts and type constructors, each element of the latter set being

266: attributed a specific arity. The set of sorts initially contains $o$,

267: the type of propositions, and others such as $int$, $real$, \etc, with

268: obvious interpretations. We also assume the availability of at least

269: the unary list type constructor $list$. Both these sets must be

270: augmentable dynamically in a programming situation, a fact that we

271: will utilize implicitly.  The full collection of types is the smallest

272: set satisfying the following properties: (i)~each sort is a type,

273: (ii)~if $\alpha_1,\ldots,\alpha_n$ are types and $c$ is a type

274: constructor of arity $n$, then $(c\app \alpha_1\app\ldots\app

275: \alpha_n)$ is a type, and (iii)~if $\alpha$ and $\beta$ are types,

276: then so is $(\alpha 

277: \ra \beta)$. A function type is one whose top-level structure

278: has the form $(\alpha \ra \beta)$. All other types are considered to

279: be atomic. We minimize the use of parentheses by assuming that the

280: application of a type constructor has highest 

281: priority and that $\ra$ is right associative. The latter

282: convention allows any function type to be written in the form

283: $\alpha_1 \ra 

284: \ldots \ra \alpha_n \ra \beta$ where $\beta$ is an atomic type. The

285: target type of such a type is $\beta$ and

286: $\alpha_1,\ldots,\alpha_n$ are its argument types. This notation

287: and terminology is extended to atomic types by permitting the argument

288: types to be an empty sequence. 

289: 

290: Starting from typed collections of constants and variables, the terms

291: in the language are identified together with their types via the

292: following rules:

293: (i)~each constant and variable of type $\alpha$ is a term of type

294: $\alpha$, (ii)~if $x$ is a variable of type $\alpha$ and $t$ is a term

295: of type $\beta$, then $(\lambdax {x} t)$ is a term of type $\alpha

296: \ra \beta$ and is called an abstraction that binds $x$ and has scope

297: $t$, and (iii)~if $t_1$ and $t_2$ are terms of type $\alpha \ra \beta$

298: and $\alpha$ respectively, then $(t_1 \app t_2)$ is a term of type

299: $\beta$ and is called an application of $t_1$ to $t_2$. We

300: reduce the use of parentheses in writing terms by assuming that

301: application is left associative and that an abstraction has as its

302: scope the largest well-formed term to the right of the variable it

303: binds.

304: 

305: The constants in the language are partitioned into {\it non-logical}

306: and {\it logical} ones. The former set contains an initial

307: collection of elements such as those representing the integers and

308: is augmentable in some manner that we, once again, leave

309: implicit. The set of logical constants consists of the symbols $\top$

310: of type $o$ denoting the tautologous proposition, $\neg$ of type $o

311: \ra o$ denoting negation, $\land$, $\lor$ and $\supset$ of type $o \ra

312: o \ra o$ denoting conjunction, disjunction and implication,

313: respectively, and, for each $\alpha$, $\Sigma_\alpha$ and $\Pi_\alpha$

314: of type $(\alpha \ra o) \ra o$.  The last two `families' of constants

315: represent generalized existential and universal quantifiers: formulas

316: usually written as $\somex {x} P$ and $\allx {x} P$ are rendered in

317: this logic as $\Sigma_\alpha\app

318: \lambdax {x} P$ and $\Pi_\alpha\app \lambdax {x} P$ for an appropriate

319: type $\alpha$. We will, in 

320: fact, use the former as abbreviations of the latter. Although type

321: subscripts are strictly necessary with $\Sigma$ and $\Pi$, we will

322: omit these when their identity is obvious or irrelevant to the

323: discussion at hand. We will also adopt the customary infix notation

324: for the application of $\land$, $\lor$ and $\supset$ to two

325: arguments in succession.

326: 

327: We assume the usual notions of free and bound variables and of

328: subterms of a term. Equality between terms incorporates the rules of

329: lambda conversion. Let us say that a term $s$ is free for the variable

330: $x$ in the term $t$ if $x$ does not appear free in $t$ in the  

331: scope of an abstraction that binds a free variable of $s$. Further,

332: let $\subfor{s}{x}{t}$ denote the result of replacing all

333: the free occurrences of $x$ in $t$ by $s$. The lambda conversion rules

334: that we use are then the following:

335: 

336: \begin{enumerate}

337: 

338: \item ($\alpha$-conversion) Replacing a subterm of the form $\lambdax

339: {x} t$ in a given term by $\lambdax {y} (\subfor{y}{x}{t})$, provided

340: $y$ is a variable of the same type as $x$ that is neither free for $x$

341: in $t$ nor free in $t$. 

342: 

343: \item ($\beta$-conversion) Replacing a subterm of the form $(\lambdax

344: {x} t_1)\app t_2$ in a given term by $\subfor {t_2} {x} {t_1}$ or

345: vice versa, provided $t_2$ is free for $x$ in $t_1$. 

346: 

347: \item ($\eta$-conversion) Replacing a subterm of the form $t$ in a

348: given term by $\lambdax {x} t \app x$ and vice versa, provided $t$

349: is of type $\alpha \ra \beta$ and $x$ is a variable of type $\alpha$

350: that is not free in $t$. 

351: 

352: \end{enumerate}

353: 

354: \noindent Two terms are considered to be equal if one can be

355: obtained from the other by using a sequence of these rules. In

356: determining such equality, it is often necessary to consider directed

357: applications of these conversion rules. Of particular importance is an

358: oriented form of the $\beta$-conversion rule that is made precise as

359: follows. First, we identify a term of the form $(\lambdax

360: {x} t_1)\app t_2$ as a {\it $\beta$-redex}; in the sequel, we shall

361: also refer to such a term more simply as just a redex and shall

362: call $t_1$ its body and $t_2$ its argument. Now, the condition

363: permitting the replacement of a subterm 

364: of this kind as per the $\beta$-conversion rule may

365: not be satisfied in general, but this can be corrected by using a

366: sequence of $\alpha$-conversion steps. We call such a sequence

367: followed by the desired application of the $\beta$-conversion rule a

368: $\beta$-contraction.

369: 

370: We will need to consider the idea of unifying two lambda terms. The

371: interest here is in substituting terms of matching types for free

372: variables so that the two terms become equal. This substitution

373: operation must be performed with care to 

374: ensure that free variables in the substituted terms do not get

375: accidentally bound in the result. A correct characterization of this

376: operation can, in fact, be provided using equality modulo the lambda

377: conversion rules. Thus, suppose that, for $1 \leq i \leq n$, $t_i$ and

378: $x_i$ are a term and a variable of identical type. Then, the set

379: $\{\langle x_i, t_i\rangle \vert 1 \leq i \leq n \}$ represents a

380: substitution and the application of this substitution to $t$ is

381: equal to the term $(\lambdax {x_1} \ldots \lambdax {x_n} t)\app t_1

382: \app \ldots \app t_n$.

383: 

384: A central part of generalizing Horn clauses to higher-order logic is

385: describing a suitable notion of atomic formulas. Towards this end, we

386: first identify the class of {\it positive} terms as those lambda terms

387: in which the only logical constants that appear are

388: $\land$, $\lor$ and $\Sigma_\alpha$. Our atomic formulas or atoms are

389: then all the terms of type $o$ of the form $P\app t_1 \app \ldots \app

390: t_n$ where $P$ is a (predicate) variable or non-logical constant and,

391: for $1 \leq i \leq n$, each $t_i$ is a positive term. Such a formula

392: is said to be {\it rigid} 

393: just in case $P$, its predicate head, is a non-logical constant and is

394: said to be {\it flexible} otherwise. We denote arbitrary atoms

395: by $A$ and rigid ones by $A_r$ below. {\it Goal formulas} or

396: simply {\it goals} are then the propositional terms that are denoted

397: by $G$ in the syntax rule 

398: \[G ::= \top \sep A \sep G\land G \sep G\lor G \sep \somex {x} G.\]

399: These formulas are higher-order versions of queries or goals in

400: Prolog; notice, in particular, that the arguments of atomic goals are

401: lambda terms as opposed to first-order terms and predicate and

402: function variables  are permitted in goals. A higher-order Horn clause

403: or program clause is the universal closure of a term of the form $A_r$

404: or $G \supset A_r$. Program clauses are intended to

405: be interpreted in a computational setting as (partial) definitions of

406: procedures and from this perspective the restriction to rigid atoms

407: is well-motivated: such an interpretation is meaningful only

408: if the `procedure' has a definite name. 

409: 

410: A multiset of higher-order program clauses constitute a program in our

411: logic programming language. Computation is engendered by a

412: goal formula being presented relative to a given program.  Such a goal

413: formula typically has existential quantifiers at its head and the

414: programming task is to find instantiations for the quantified

415: variables that permit the resulting goal to be solved from the

416: program. 

417: 

418: \begin{example}\label{ex:mapfun}

419: Let $i$ be a sort representing individuals and let the set of

420: nonlogical constants contain the following: 

421: \begin{tabbing}

422: \qquad\=${\it mapfun}$\quad\=\kill

423: \>${\it nil}$\>of type $list\app i$\\

424: \>$::$\> of type $i \ra list\app i \ra list \app i$, and\\

425: \>${\it mapfun}$\> of type $list \app i\ra (i \ra i) \ra list \app i\ra

426: o$

427: \end{tabbing}

428: \noindent Further, assume that $::$ can be written as an infix, right

429: associative operator. Then the

430: clauses

431: \begin{tabbing}

432: \qquad\=\kill

433: \>$\allx {f}({\it mapfun}\app {\it nil}\app f\app {\it nil})$\ and\\

434: \>$\allx {x} \allx {f} \allx {l_1} \allx {l_2}({\it mapfun}\app l_1\app f\app

435: l_2) \supset ({\it mapfun}\app (x \app ::\app l_1)\app f\app ((f \app x) \app

436: :: \app l_2))$

437: \end{tabbing}

438: \noindent constitute a program.\footnote{The omission of types with

439: the quantifiers in these clauses illustrates the convention alluded to

440: earlier. Here, the type of ${\it mapfun}$ uniquely

441: determines the types of the quantified variables.} Adopting Prolog's

442: suggestive manner of writing implications, its convention of making

443: quantifiers 

444: implicit by using names beginning with uppercase letters for

445: quantified variables and its method for depicting each program clause,

446: this program can be rendered into the following `friendlier' syntax:  

447: \begin{tabbing}

448: \qquad\=\kill

449: \>${\it mapfun} \app {\it nil}\app F\app {\it nil}.$\\

450: \>${\it mapfun}\app (X :: L1)\app F\app ((F\app X) :: L2)$ {\tt :-}

451: ${\it mapfun}\app L1\app F\app L2.$ 

452: \end{tabbing}

453: \noindent Letting $g$ be a constant of type $i \ra i \ra i$ and $a$

454: and $b$ be constants of type $i$, the

455: formula $\somex {l} {\it mapfun}\app (a :: b :: {\it nil})\app (\lambdax {x} g

456: \app a\app x) \app l$ 

457: constitutes a query. Using Prolog's conventions for making

458: quantifiers implicit, this query may be rewritten as 

459: \begin{tabbing}

460: \qquad\=\kill

461: \> ${\it mapfun}\app (a :: b :: {\it nil})\app (\lambdax {x} g \app

462: a\app x) \app L$.

463: \end{tabbing}

464: \noindent There is exactly one solution to this query, this being

465: given by the `answer' substitution $\{\langle L,(g\app a\app a) ::

466: (g\app a \app b) :: {\it nil}\rangle\}.$ 

467: Notice that generating this answer substitution requires, amongst

468: other things, the application of a lambda term to two different

469: arguments and the subsequent reduction of these terms to normal

470: form. An alternative query is the following:

471: \begin{tabbing}

472: \qquad\=\kill

473: \> ${\it mapfun}\app (a :: b :: {\it nil})\app F \app ((g\app a \app

474: a) :: (g \app a \app b) :: {\it nil})$.

475: \end{tabbing}

476: \noindent This query also has a unique solution, this being the

477: substitution $\{\langle F, \lambdax {x} g \app a \app x \rangle \}$.

478: Computing this answer involves unifying two pairs of terms containing a

479: function variable, these being $F\app a$ and $g\app a \app a$ on the

480: one hand and $F\app b$ and $g\app a \app b$ on the other. We discuss

481: in the next section a process by which such unification

482: problems may be solved. For the moment, we note that the first of the

483: pairs of terms has four distinct most general unifiers given by the

484: following substitutions for $F$: 

485: \begin{tabbing}

486: \qquad\=\kill

487: \>$\{\langle F,\lambdax {x} g\app a\app a \rangle \}$, $\{\langle F,

488: \lambdax {x} g\app x\app a\rangle \}$, $\{\langle F, \lambdax {x}

489: g\app x \app x\rangle \}$, and $\{\langle F,\lambdax {x} g\app a\app x

490: \rangle \}$.

491: \end{tabbing}

492: \noindent If the two pairs of terms in question are unified sequentially

493: and any but the last solution is chosen initially for the first pair,

494: then it will be necessary to backtrack to find a solution for the

495: composite problem.

496: \end{example}

497: 

498: We shall employ the conventions used for depicting formulas

499: in the above example freely in the rest of the paper. The predicate

500: ${\it mapfun}$ considered in this example relates a function and two lists

501: just in case the second list is obtained by applying the function to

502: each element of the first list. The notion of function application is,

503: however, relatively weak, being given by reduction in a typed lambda

504: calculus with no interpreted constants. A stronger form of function

505: application, one that invokes the ability of solving goals in the

506: underlying language, can be realized by using a predicate version of

507: ${\it mapfun}$ as described in the following example.

508: 

509: \begin{example}\label{ex:mappred}

510: In addition to the constants and types of Example~\ref{ex:mapfun},

511: assume that ${\it mappred}$ is a constant of type  

512: $list\app i \ra (i \ra i \ra o) \ra list\app i \ra o$.

513: Then, using the Prolog convention of depicting conjunctions

514: by commas, the following clauses correspond to a program:

515: \begin{tabbing}

516: \qquad\=\kill

517: \>${\it mappred}\app {\it nil}\app P\app {\it nil}$.\\

518: \>${\it mappred}\app (X :: L1)\app P\app (Y :: L2)$ {\tt :-}

519: $(P\app X\app Y),({\it mappred}\app L1\app P\app L2).$

520: \end{tabbing}

521: \noindent Let ${\it bob}$, ${\it john}$, ${\it mary}$, ${\it sue}$, ${\it dick}$ and ${\it kate}$ be

522: constants of type $i$ and let ${\it parent}$ be a constant of type $i \ra i

523: \ra o$. Then the following additional clauses define a `parent'

524: relationship between different individuals:

525: \begin{tabbing}

526: \qquad\=\kill

527: \> ${\it parent} \app {\it bob}\app {\it john}$.\\

528: \> ${\it parent} \app {\it john} \app {\it mary}$.\\

529: \> ${\it parent} \app {\it sue} \app {\it dick}$.\\

530: \> ${\it parent} \app {\it dick} \app {\it kate}$.

531: \end{tabbing}

532: \noindent In this context, the following term constitutes a query:

533: \begin{tabbing}

534: \qquad\=\kill

535: \> ${\it mappred}\app ({\it bob} :: {\it sue} :: {\it nil}) \app {\it parent} \app L$.

536: \end{tabbing}

537: \noindent The sole answer to this query is the substitution

538: $\{\langle L, {\it john} :: {\it dick} :: {\it nil}\rangle \}$. 

539: In solving this query, two new goals of the form

540: $({\it parent}\app {\it bob} \app Y1)$ and $({\it parent} \app {\it

541:   sue} \app Y2)$ will have to be dynamically formed and

542: solved. Another example of a query is 

543: \begin{tabbing}

544: \qquad\=\kill

545: \> ${\it mappred} \app ({\it bob} :: {\it sue} :: {\it nil}) \app (\lambdax {x} \lambdax {y}

546: \somex {z} ({\it parent} \app x \app z) \land ({\it parent} \app z \app y))\app L$.

547: \end{tabbing}

548: \noindent This goal asks for the grandparents of ${\it bob}$

549: and ${\it sue}$ and has as its solution the substitution $\{\langle L,

550: {\it mary} :: {\it kate} :: {\it nil}\rangle \}$. 

551: \ignore{

552: } Finding this answer requires two new goals with complex

553: structures---each with an embedded conjunction and 

554: existential quantifier---to be constructed at runtime and then solved.

555: \end{example}

556: 

557: Example~\ref{ex:mappred} motivates the particular structure chosen for

558: atomic formulas in the definition of our higher-order logic

559: programming language. Logical constants that appear in the arguments of

560: predicate expressions can become top-level symbols in a goal

561: constructed at runtime. These constants must, therefore, be limited

562: to ones that can legitimately appear in such a position, a requirement

563: that is achieved by the restriction to positive terms. In a

564: different direction, in contrasting this example with

565: Example~\ref{ex:mapfun}, a question that arises is whether or

566: not the ${\it mappred}$ predicate can be run in `reverse'. For example, is

567: the query

568: \begin{tabbing}

569: \qquad\=\kill

570: \> ${\it mappred}\app ({\it bob} :: {\it sue} :: {\it nil}) \app P \app ({\it john} :: {\it dick} :: {\it nil})$

571: \end{tabbing}

572: \noindent computationally meaningful? It is tempting to decide that

573: it is and that it has $\{\langle P, {\it parent}\rangle \}$ as an

574: answer substitution. However, a little thought reveals that there are

575: too many relations that are 

576: true of ${\it bob}$ and ${\it john}$ on the one hand and ${\it sue}$

577: and ${\it dick}$ on the 

578: other and so this query is, in a sense, an ill-formed one. We note that

579: the `solution' $\{\langle P,\lambdax {x} \lambdax {y} \top\rangle \}$

580: actually subsumes all others in a logical sense and, consistent with

581: the present viewpoint, we may treat this as the {\it only} legitimate

582: answer to the posed query.

583: 

584: The idea of solving a goal that we have discussed only intuitively

585: thus far can be made logically precise using the notion of provability

586: in classical logic \cite{NM90}. Operationally, this sanctions a recipe

587: for solving a {\it closed} goal from a program $\Pscr$ that is based

588: on the structure of the goal: 

589: 

590: \begin{enumerate}

591: \item The goal $\top$ is solved immediately. 

592: 

593: \item The goal $G_1 \land G_2$ is solved by solving both $G_1$ and

594:   $G_2$. 

595: 

596: \item The goal $G_1 \lor G_2$ is solved by solving one of $G_1$ and

597:   $G_2$. 

598: 

599: \item The goal $\somex {x} G$ is solved by solving $\subfor{t}{x}{G}$

600:   for some closed positive term $t$.

601: 

602: \item A rigid atomic goal $A_r$ is solved either (a)~by determining

603:   that it is equal to a ground instance of a clause in $\cal P$, or

604:   (b)~by finding a ground instance $G \supset A'_r$ of a clause in

605:   $\cal P$ such that $A_r$ and $A'_r$ are equal and then solving $G$. 

606: \end{enumerate}

607: 

608: \noindent In this description, a ground instance of a program clause

609: is generated by substituting closed positive terms for the universally

610: quantified variables in the clauses. 

611: 

612: The recipe described above clarifies the operational semantics

613: of our language, but needs refinement to become the basis for

614: implementation. In particular, it is necessary to eliminate from it

615: the oracle used for picking an appropriate instance of an

616: existentially quantified goal and to embed in it some method for

617: treating the choices that have to be made concerning the disjunct of a

618: disjunctive goal that is to be solved and the clause that is to be

619: used to solve an atomic formula. These kinds of issues have 

620: actually to be dealt with already in a first-order language. In that

621: context, existential goals are treated by delaying the choice of

622: specific instantiations till such time that information is available

623: for making the `right' choices. Thus, the goal $\somex {x} G$ is

624: transformed into one of the form $\subfor{X}{x}G$ where $X$ is a new

625: variable that  may be instantiated in the course  

626: of computation. Actual instantiations for such variables are

627: determined at the time of solving atomic goals.  Given the atomic goal

628: $A$, we look for a clause of the form $\allx {y_1}

629: \ldots \allx {y_n} A'$ or $\allx {y_1} \ldots \allx {y_n} (G' \supset

630: A')$ that is such that $A$ unifies with the formula that results from

631: $A'$ by replacing the universally quantified variables with new

632: variables.  If a clause of this kind is found, then, depending on its

633: form, either the atomic goal succeeds immediately or the next task

634: becomes that of solving the resulting instance of $G'$.  With regard

635: to nondeterminism, the usual solution is to make choices in a

636: predetermined manner and to reconsider these in case of

637: subsequent failure. Now, the treatment of the logical

638: connectives, the sequencing through program clauses and much of the

639: unification computation can, in fact, be compiled and this

640: is what is actually done within machine models such as the WAM.

641: 

642: The ideas discussed above have obvious applicability in the

643: implementation of our language as well. However, their precise

644: deployment must take into account the higher-order nature of this

645: language. A detailed exposition of the new problems posed by this

646: aspect and an integration of their treatment into the basic framework

647: described above is the subject of the rest of this paper.

648: 

649: Before concluding this section, we comment briefly on the rigidity of

650: the typing regimen used in our language. The predicates 

651: ${\it mapfun}$ and ${\it mappred}$ as we have defined them here are,

652: for instance, 

653: restricted to apply to lists of individuals and 

654: cannot be used with lists of integers, lists of lists or lists of

655: function objects. This inflexibility can be alleviated by injecting a

656: form of polymorphism through the use of type variables.  Thus, with an

657: appropriate change to the underlying typing scheme, ${\it mapfun}$ may have

658: been defined to be of type $list\app A \ra (A \ra B) \ra list\app B

659: \ra o$, where $A$ and $B$ can be instantiated by arbitrary types. A

660: polymorphism of this kind is, in reality, supported by

661: $\lambda$Prolog. However, we elide this polymorphism here

662: because it poses additional implementation problems

663: that we presently do not wish to consider. For the interested

664: reader, these problems are discussed for a first-order language in

665: \cite{KNW92}. The solutions provided therein are entirely

666: compatible with the implementation methods we develop here for our

667: simply typed language.  

668: 

669: \section{An Abstract Interpreter}\label{sec:interp}

670: 

671: The desired refinement of our recipe for solving goal formulas

672: requires an understanding of higher-order unification problems and of

673: a procedure for their 

674: solution. Problems of this kind are defined by finite multisets of

675: pairs of terms in which the two terms in each pair have identical

676: types. We will refer to a collection of this sort as a {\it

677: disagreement set}. A solution to, or a unifier for, such a problem

678: is a substitution whose application to the terms in each pair makes

679: them equal. Higher-order unification problems are, in the general

680: case, undecidable ones and also do not admit of finite sets of most

681: general unifiers. There is, nevertheless, a systematic way to check for

682: unifiability and to enumerate non-redundant sets of preunifiers in

683: the process. This method, that is due to Huet \cite{Huet75}, has been

684: used in several programming systems and has demonstrated a practical

685: usefulness to higher-order unification despite the theoretical

686: characteristics of the problem.

687: 

688: Huet's method relies on what is known as a {\it head normal form}

689: for a term. A term is in this form if it has the structure

690: $\lambdax {x_1} \ldots \lambdax {x_n} (A\app t_1\app \ldots\app t_m)$

691: where $A$ is either a constant or a variable. Given such a

692: term, $A$ 

693: is called its {\it head}, the abstractions at the front of the term

694: are collectively called its {\it binder}, $t_1, \ldots t_m$ are called

695: its arguments, $(A\app t_1\app \ldots\app t_m)$ is called its body and

696: the term is said to be {\it rigid} if $A$ is a constant or an element

697: of $\{x_1,\ldots,x_n\}$, and {\it flexible} otherwise. Every

698: term in  our 

699: typed language can be transformed into such a form modulo the lambda

700: conversion rules \cite{Andrews71}. Moreover, the results of applying a 

701: substitution to  a term and to any one of its head normal forms

702: are equal under these rules. Thus, we may restrict our attention to

703: terms in such a form as we henceforth do. 

704: 

705: The unification procedure consists of the repetitive use of two

706: phases for transforming a given disagreement set into a form for which

707: it can be decided no unifiers exist or for which unifiability is

708: evident.  The first of these phases is akin to the term simplification

709: that is an intrinsic part of first-order unification. Consider two

710: head normal forms that are of the same type. The binders of

711: these terms may be distinct both in the choice of variable names and in

712: length at the outset, but these can be arranged to be identical

713: through the use of the $\alpha$- and $\eta$- conversion rules. We may

714: therefore assume that the terms in question are, in fact, of the form

715: $\lambdax {x_1} \ldots \lambdax {x_n} (A_1\app s_1 \app

716: \ldots \app s_i)$ and $\lambdax {x_1}\app \ldots\app \lambdax {x_n}

717: (A_2\app r_1 \app\ldots \app r_j)$ respectively. Now, if both terms

718: are rigid, it can be seen that they are unifiable only if $A_1$ and 

719: $A_2$ are identical and, in this case, they have the same unifiers as

720: the set 

721: \begin{tabbing}

722: \qquad\=\kill

723: \>$\{\langle \lambdax {x_1} \ldots \lambdax {x_n} s_1,

724: \lambdax {x_1} \ldots \lambdax {x_n} r_1 \rangle, \ldots,\langle

725: \lambdax {x_1} \ldots \lambdax {x_n} s_i, \lambdax {x_1} \ldots

726: \lambdax {x_n} r_i \rangle \}$;

727: \end{tabbing}

728: \noindent note that the identity of types ensure that $i = j$ if $A_1

729: = A_2$. Thus, given an arbitrary disagreement set, this observation

730: can be used either to conclude that it has no unifiers or to reduce it

731: to another disagreement set with the same unifiers and in which each

732: pair has at least one flexible term. We assume below that this kind of  

733: simplification is carried out by a function called \simpl\ that

734: returns a distinguished value \failed\ in the case that it detects the

735: impossibility of unification.

736: 

737: One of the possibilities for the value returned by \simpl\ is that it

738: is a disagreement set that has only `flexible-flexible' pairs.

739: A set of this kind is known to be unifiable but, in the case that it 

740: is non-empty, a complete search for its unifiers can be unconstrained

741: \cite{Huet75}. The best strategy for these sets is 

742: therefore to treat them as constraints on any further processing or,

743: if computation is at an end, to present them as such on computed

744: answers.  

745: 

746: The second phase in unification becomes relevant when \simpl\ returns

747: a set that has at least one `flexible-rigid' pair. A substitution may be

748: posited for reducing the difference between the terms in the pair in

749: this case. Two kinds of elementary substitutions completely cover all

750: the possible ways of doing this. In

751: particular, let $t_1$ 

752: be the flexible term with $F$ as its head and let $t_2$ be the rigid

753: term with $c$ as its head.  Further, let the types of $F$ and $c$ be

754: $\alpha_1 \ra \cdots \ra \alpha_k

755: \ra \beta$ and $\gamma_1 \ra \cdots \ra \gamma_j \ra \beta$

756: respectively, where $\beta$ is an atomic type. Then

757: \begin{enumerate}

758: \item the {\it imitation substitution} is defined only when $c$ is a

759: constant and is

760: \begin{tabbing}

761: \qquad\=\kill

762: \>$\{ \langle F, \lambdax {w_1} \ldots \lambdax {w_k} (c\app (H_1\app

763: w_1 \app \ldots \app w_k)\app \ldots \app (H_j\app w_1 \app \ldots

764: \app w_k)) \rangle \}$,

765: \end{tabbing}

766: \noindent assuming that $H_1,\ldots,H_j$ are new free

767: variables of appropriate types, and 

768: 

769: \item for $1 \leq i \leq k$, the {\it $i^{th}$ projection

770: substitution} is defined only when $\alpha_i$ is of the form $\beta_1

771: \ra \cdots \ra \beta_l \ra \beta$ and is

772: \begin{tabbing}

773: \qquad\=\kill

774: \>$\{ \langle F, \lambdax {w_1} \ldots \lambdax {w_k}

775: (w_i\app (H_1\app w_1 \app \ldots \app w_k)\app \ldots \app (H_l\app 

776: w_1 \app \ldots \app w_k)) \rangle \}$,

777: \end{tabbing}

778: \noindent assuming $H_1,\ldots,H_l$ are new free variables of appropriate

779: types. 

780: \end{enumerate}

781: Notice that these substitutions are determined entirely by the

782: heads of the flexible and rigid terms in question and they are finite

783: in number.

784: 

785: The iterative use of the two described phases in unification naturally

786: involves a search whose structure can be visualized through a {\it

787:   matching tree} \cite{Huet75}. Figure~\ref{fig:match}

788: presents such a tree for the unification problem $\{\langle F\app a,

789: g\app a \app a \rangle \}$ encountered in

790: Example~\ref{ex:mapfun}.  The arcs in this tree are labelled with the

791: relevant imitation and projection substitutions and the nodes

792: represent the result of transforming the set on the prior node by

793: first applying the substitution on the incoming arc and then carrying

794: out the simplification embodied in \simpl. The leaves of a matching

795: tree are labelled either with \failed\ or with a multiset of

796: flexible-flexible pairs. A solution to the original unification

797: problem can be obtained by composing the substitutions on the path to

798: the latter kind of leaf with a unifier for that leaf. In the example

799: presented, observing that an empty disagreement set has the empty

800: substitution as its most general unifier, these solutions involve

801: substituting $\lambdax {x} g\app a\app a$, $\lambdax {x} g \app a\app

802: x$, $\lambdax {x} g \app x \app a$  and $\lambdax {x}g \app x \app x$

803: for $F$. A matching tree is exhaustive in that the unifiers

804: of the leaves of a completely expanded tree can be used in this

805: fashion to produce all the unifiers of the original set. However,

806: such a tree can, in principle, include nonterminating branches and

807: can also have an infinite number of `success' nodes.

808: 

809: \begin{figure}

810: \begin{center}

811: 

812: \setlength{\unitlength}{0.00070833in}

813: %

814: \begingroup\makeatletter\ifx\SetFigFont\undefined%

815: \gdef\SetFigFont#1#2#3#4#5{%

816:   \reset@font\fontsize{#1}{#2pt}%

817:   \fontfamily{#3}\fontseries{#4}\fontshape{#5}%

818:   \selectfont}%

819: \fi\endgroup%

820: {\renewcommand{\dashlinestretch}{30}

821: \begin{picture}(6849,3363)(0,-10)

822: \path(4875,2979)(4050,2454)

823: \path(4135.133,2543.735)(4050.000,2454.000)(4167.346,2493.115)

824: \path(5175,2979)(6150,2454)

825: \path(6030.120,2484.478)(6150.000,2454.000)(6058.566,2537.306)

826: \path(3450,2004)(2250,1404)

827: \path(2343.915,1484.498)(2250.000,1404.000)(2370.748,1430.833)

828: \path(3675,2004)(4800,1404)

829: \path(4680.000,1434.000)(4800.000,1404.000)(4708.235,1486.941)

830: \path(1800,879)(2775,354)

831: \path(2655.120,384.478)(2775.000,354.000)(2683.566,437.306)

832: \path(5100,879)(4200,354)

833: \path(4288.537,440.378)(4200.000,354.000)(4318.770,388.551)

834: \path(5400,879)(6300,354)

835: \path(6181.230,388.551)(6300.000,354.000)(6211.463,440.378)

836: \drawline(5175,2979)(5175,2979)

837: \drawline(5175,2979)(5175,2979)

838: \path(1500,879)(450,354)

839: \path(543.915,434.498)(450.000,354.000)(570.748,380.833)

840: \put(4425,3204){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\{\langle

841: F\app a,g\app a\app a\rangle\}$}}}}}

842: \put(2850,2154){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\{\langle

843: H_1\app a, a\rangle,\langle H_2 \app a,a\rangle\}$}}}}}

844: \put(1275,1104){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\{\langle

845: H_2\app a, a\rangle \}$}}}}}

846: \put(4800,1104){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\{\langle

847: H_2\app a,a\rangle\}$}}}}}

848: \put(2250,729){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\{\langle

849: H_2,\lambdax{x}x\rangle\}$}}}}}

850: \put(2700,54){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\{\}$}}}}}

851: \put(300,54){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\{\}$}}}}}

852: \put(4050,54){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\{\}$}}}}}

853: \put(6225,54){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\{\}$}}}}}

854: \put(5850,729){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\{\langle

855: H_2,\lambdax{x}x\rangle\}$}}}}}

856: \put(6225,2154){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}\failed}}}}}

857: \put(3600,729){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\{\langle

858: H_2,\lambdax{x}a\rangle\}$}}}}}

859: \put(0,729){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\{\langle

860: H_2,\lambdax{x}a\rangle\}$}}}}}

861: \put(5700,2829){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\{\langle

862: F,\lambdax{x}x\rangle\}$}}}}}

863: \put(2175,2829){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\{\langle

864: F,\lambdax{x}g\app (H_1\app x)\app (H_2\app x)\rangle\}$}}}}}

865: \put(1650,1779){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\{\langle

866: H_1,\lambdax{x}a\rangle\}$}}}}}

867: \put(4425,1779){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\{\langle

868: H_1,\lambdax{x}x\rangle\}$}}}}}

869: \end{picture}

870: }

871: 

872: \end{center}

873: \caption{A matching tree for $\{\langle (F\app a),(g\app a \app a)

874: \rangle \}$}

875: \label{fig:match}

876: \end{figure}

877: 

878: Our refinement to the earlier model for solving goal formulas consists

879: of viewing a state in the process as a composite of a collection of

880: goals and a disagreement set, the latter component arising from the

881: attempt to solve atomic goals. Progress through this state space is

882: made by simplification steps applied either to the goals or to the

883: disagreement set. In any given case, these steps must be relativized

884: to a particular program ${\cal P}$. The notion of a \pderivation\

885: \cite{NM90} that generalizes  SLD derivations described in

886: \cite{AvE82} for first-order Horn clause logic makes this idea

887: precise.  

888: 

889: \begin{defn} Let $\Pscr$ be a program, let $\Gscr$ be a symbol for

890:   multisets of goal formulas that we refer to also as {\it goal sets},

891:   and let $\theta$ be a symbol for substitutions.

892:  Further, let $\Dscr$ be a symbol for a disagreement set

893: or the special value \failed. Finally, let \match\ be a 

894: function on flexible-rigid disagreement pairs that produces the set of

895: imitation and projection substitutions for any given pair. 

896: Then a tuple $\tup{{\Gscr} _2,{\Dscr} _2,\theta _2}$ is said to be 

897: \pderivable\ from a tuple  

898: $\tup{{\Gscr} _1,{\Dscr} _1,\theta _1}$ in which $\Dscr_1 \ne \failed$

899: if it is obtainable from the latter by one of the following

900: steps:\footnote{We intend $\cup$ and $-$ to be interpreted as multiset 

901:   operations in these clauses.}

902: 

903: \begin{enumerate}

904: 

905: \item {\it Goal simplification step}: $\theta_2 = \emptyset$,

906: $\Dscr_2 = \Dscr_1$, and for some $G \in \Gscr_1$ it is the case that

907: 

908: \begin{enumerate}

909: 

910: \item $G$ is $\top$ and $\Gscr_2 = \Gscr_1 - \{G\}$, or

911: 

912: \item $G$ is $G_1 \land G_2$ and $\Gscr_2 = (\Gscr_1 -

913: \{G\}) \cup \{G_1,G_2\}$, or

914: 

915: \item $G$ is $G_1 \lor G_2$ and, for $i = 1$ or $i = 2$,

916: $\Gscr_2 = (\Gscr_1 - \{G\}) \cup \{G_i\}$, or

917: 

918: \item $G$ is $\Sigma\app P$ and $\Gscr_2 = (\Gscr_1 - \{G\})

919: \cup \{P\app Y\}$ where $Y$ is a new variable.

920: 

921: \end{enumerate}

922: 

923: \item {\it Backchaining step:} $\theta_2 = \emptyset$ and, for

924: some rigid atom $G \in \Gscr_1$ either

925: 

926: \begin{enumerate}

927: 

928: \item $A$ is an atom obtained by instantiating the universal

929: quantifiers in a clause in $\cal P$ with new variables and $\Gscr_2

930: = \Gscr_1 -\{G\}$ and $\Dscr_2 =\simpl(\Dscr_1 \cup \{\tup{G,A}\})$, or

931: 

932: \item $G' \supset A$ is obtained by instantiating the universal

933: quantifiers in a clause in $\cal P$ with new variables and

934: $\Gscr_2 = (\Gscr_1 -\{G\}) \cup \{G'\}$, and $\Dscr_2 =\simpl(\Dscr_1

935: \cup \{\tup{G,A}\})$. 

936: 

937: \end{enumerate}

938: 

939: \item {\it Flexible goal solution step:} $G \in \Gscr_1$ is an atomic

940: goal formula that has the (free) variable $Y$ of type $\alpha_1 \ra

941: \cdots \ra \alpha_n \ra o$ as its head, and $\theta_2 = \{\langle Y,

942: \lambdax   {x_1} \ldots \lambdax {x_n}  \top \rangle\}$, $\Gscr_2 =

943: \theta_2(\Gscr_1 - \{G\})$ and $\Dscr_2 = \simpl(\theta_2(\Dscr_1))$;

944: the application of a substitution to a goal set and a disagreement set

945: here and below corresponds to its application to the component terms

946: of these sets.

947: 

948: \item {\it Unification step:} For some flexible-rigid pair

949: $\chi \in \Dscr_1$, either $\match(\chi) = \emptyset$ and $\Dscr_2 =

950: \failed$, or $\theta_2 \in \match(\chi)$ and $\Gscr_2 =

951: \theta_2(\Gscr_1)$ and $\Dscr_2 = \simpl(\theta_2( \Dscr_1))$.

952: 

953: \end{enumerate}

954: A sequence of the form $\tup{\Gscr_i,\Dscr_i,\theta_i}_{1 \leq i \leq

955: n}$ is a \pderivation\ sequence for a goal formula $G$ if 

956: $\Gscr_1 = \{G\}$, $\Dscr_1 = \emptyset$ and $\theta_1 =

957: \emptyset$, and for $1 \leq j < n$,

958: $\tup{\Gscr_{j+1},\Dscr_{j+1},\theta_{j+1}}$ 

959: is \pderivable\ from $\tup{\Gscr_{j},\Dscr_{j},\theta_{j}}$. Such a

960: sequence terminates in failure if $\Dscr_n = 

961: \failed$ and with success if $\Gscr_n = \emptyset$ and $\Dscr_n$ is

962: either empty or contains only flexible-flexible pairs. In the latter

963: case, we say that the sequence is a \pderivation\ of $G$. Such a

964: sequence embodies in it a solution to the query $G$ in the context of

965: the program $\Pscr$ and the {\it answer substitution} corresponding to

966: it is obtained by composing

967: $\theta_n \circ \cdots \circ \theta_1$ with any unifier for $\Dscr_n$

968: and restricting the resulting substitution to the free variables of

969: $G$.

970: \end{defn}

971: 

972: An abstract interpreter for our language may be thought of as a

973: procedure that, given a program $\Pscr$, attempts to construct a

974: \pderivation\ for goal formulas. Such an interpreter would function by

975: trying to extend an existing \pderivation\ and will typically be faced

976: with alternatives in this process. This interpreter can without loss

977: of completeness choose to use a unification step whenever one is

978: applicable. The only choices that are critical are, in fact, those of

979: the disjunct to use when simplifying a disjunctive goal, the clause to

980: use in a backchaining step, the substitution to use in a unification

981: step and the point at which to solve a flexible goal. We assume a

982: depth-first approach with the possibility of backtracking in the

983: treatment of the first three aspects. The first two kinds of choices

984: are present in a first-order language as well and similar methods can

985: be used for treating them here. In particular, we use a left-to-right

986: processing order in the treatment of disjunctive goals and we base the

987: selection of  clauses in a backchaining step on an ordering on the

988: multiset determined by their presentation sequence. Moreover, the

989: cases with a potential of success can be considerably narrowed down

990: by techniques such as indexing on predicate names and the structure of

991: arguments, a fact that we utilize in

992: Section~\ref{sec:abstmachine}. The treatment of choices in the

993: unification step and the bookkeeping mechanisms for realizing

994: backtracking relative to these is a matter we discuss in a later

995: section. Finally, we assume an initial ordering on goals that we

996: maintain through an ordered, `in-place' insertion of the subgoals

997: produced by a goal 

998: simplification or backchaining step and we use this ordering to drive

999: their selection. This eventually determines the point at which

1000: flexible goals are processed. This choice may, on occasion, lead to a

1001: loss of completeness but we believe this to be pragmatically

1002: justifiable. 

1003: 

1004: \section{The Representation of Lambda Terms}\label{sec:terms}

1005: 

1006: The abstract interpreter described in the previous section assumes a ready

1007: availability of head normal forms and an immediate access to their

1008: components. In reality, these forms must be

1009: computed. The efficiency of this computation and of the access to the

1010: structures of terms is mediated eventually by the representation

1011: chosen for terms. We discuss the various factors influencing

1012: this choice below, thereby motivating the encoding that

1013: has been used in the {\it Teyjus} system.  Our discussion also

1014: highlights the tradeoffs that are relevant to the representation

1015: question. Lambda terms evolve during computation in a manner that is

1016: difficult to predict statically, making experimentation with actual

1017: implementations a necessary component to quantifying the tradeoffs. An

1018: instrumented version of the {\it Teyjus} system is currently being

1019: used to obtain such an assessment. We indicate some of the

1020: observations from these studies here, leaving a

1021: detailed exposition to other papers \cite{LN02,NX03,LNX03}.

1022: 

1023: \subsection{The Representation of Bound Variables}\label{ssec:debruijn}

1024: Presentations of lambda terms usually employ a name-based rendition of 

1025: bound variables. When such a representation is used also in an

1026: implementation, it becomes necessary to 

1027: consider the $\alpha$-conversion rule in comparison operations. For

1028: example, a common calculation within higher-order unification is

1029: determining whether the heads of two rigid terms are identical. Thus,

1030: suppose that we desire to unify the terms $\lambdax {y_1}\ldots

1031: \lambdax {y_n} (y_i\app t_1\app \ldots\app t_m)$ and $\lambdax

1032: {z_1}\ldots \lambdax {z_n} (z_i\app s_1\app \ldots\app s_m)$. Term

1033: simplification reduces this task to that of unifying the set

1034: \begin{tabbing}

1035: \qquad\=\kill

1036: \>$\{\langle \lambdax {y_1} \ldots \lambdax {y_n} t_1,

1037: \lambdax {z_1} \ldots \lambdax {z_n} s_1 \rangle, \ldots,\langle

1038: \lambdax {y_1} \ldots \lambdax {y_n} t_m, \lambdax {z_1} \ldots

1039: \lambdax {z_n} s_m \rangle \}$.

1040: \end{tabbing}

1041: \noindent However, a prelude to effecting this transformation is

1042: recognizing that the heads of the two terms match and this clearly

1043: involves a renaming operation under the chosen representation.

1044: 

1045: If the kind of comparison described above arises often in computation,

1046: it is desirable to use a representation for terms that eliminates the

1047: need for bound variable renaming. A scheme that is suitable from this

1048: perspective is that of de Bruijn \cite{debruijn72}.  Under this

1049: scheme, the connection between binding and bound occurrences of

1050: variables in lambda terms is manifest not 

1051: through names but by using indices at the bound occurrences that count

1052: the number of abstractions in a parse structure of the term up to the

1053: one binding the occurrence. Thus, the term $\lambdax {x}

1054: ((\lambdax {y} \lambdax {z} y \app x)\app (\lambdax {w} x))$ is denoted

1055: using the de Bruijn approach by the expression $\lambda\, ((\lambda\,

1056: \lambda\, \#2\app \# 3) \app (\lambda\, \# 2))$, where $\# i$ is the

1057: representation of index $i$. Subterms of a term may have bound

1058: variable occurrences that are free in the local context. An occurrence

1059: of this kind is indicated by an index whose value exceeds the number

1060: of abstractions it is embedded under, as happens in the subterm $(\lambda\,

1061: \# 2)$ of the term considered above. The original de Bruijn

1062: encoding describes also a translation of globally free variable

1063: occurrences to indices. This part of the scheme is, however, not

1064: useful in our context. Globally free variables correspond in our

1065: computational model to variables that can be instantiated. A

1066: characteristic of all the substitutions that we consider for such

1067: variables is that the only unbound variables they contain are ones

1068: that are once again globally free; this property holds, for instance,

1069: of the imitation and projection substitutions discussed in the

1070: previous section. Given this, these variables are best treated, in the

1071: usual logic programming style, as pointers to cells in memory that are

1072: tagged as unbound variables with instantiations being realized

1073: immediately by changing the contents of these cells.

1074: 

1075: The above discussion indicates a difference in representation and

1076: treatment at a pragmatic level between two kinds of variables that are

1077: similar in the underlying logic. Terminology that distinguishes

1078: between these variables will also be convenient in exposition. We

1079: henceforth use the expression `logic variable' for a  

1080: variable that is globally free, \ie, is not bound by

1081: any explicit abstraction, reserving the terms `bound variable' and

1082: `free variable' for those variables that may be bound or free in a

1083: local context but that are ultimately captured by an abstraction and

1084: hence represented by a de Bruijn index.

1085: 

1086: The de Bruijn representation solves the problem mentioned at the

1087: outset. The two terms considered there translate under this scheme

1088: into $\lambda\, \ldots \lambda\, (\# i\app \hat{t}_1\app \ldots\app

1089: \hat{t}_m)$ and $\lambda\, \ldots \lambda\, (\# i\app \hat{s}_1\app

1090: \ldots\app \hat{s}_m$), where, for $1 \leq i \leq m$,

1091: $\hat{t}_i$ and $\hat{s}_i$ are the de Bruijn representations of $t_i$

1092: and $s_i$ respectively.  The heads of the two terms are identical

1093: under this representation and, in general, the check for compatibility

1094: of the heads of two rigid terms in the term simplification phase of

1095: unification becomes a simple identity test.

1096: 

1097: The de Bruijn notation has another significant benefit in that it

1098: allows the abstractions that appear at the front of terms to be

1099: dispensed with in several situations. Such abstractions are often used

1100: in the unification process to encode the contexts in which to view the

1101: two terms that are to be unified.  When these contexts are identical,

1102: as would be the case under the de Bruijn scheme, they can be left

1103: implicit. To understand the pragmatic impact of this observation,

1104: consider again the task of unifying the terms $\lambda\, \ldots

1105: \lambda\, (\# i\app \hat{t}_1\app \ldots\app \hat{t}_m)$ and $\lambda\,

1106: \ldots \lambda\, (\# i\app \hat{s}_1\app \ldots\app \hat{s}_m)$. This

1107: task can be reduced simply to that of unifying the set 

1108: $\{\langle \hat{t}_1, \hat{s}_1 \rangle, \ldots,\langle \hat{t}_m,

1109: \hat{s}_m \rangle \}$,

1110: \ie, the outer abstractions do not need to be appended to

1111: the front of the argument terms. Term simplification thus takes a form

1112: that is closely related to the first-order version: if the heads of

1113: the two rigid terms being considered are identical, the problem simply

1114: becomes one of recursively unifying their arguments. In contrast to

1115: the situation where the outer abstractions need to be replicated and

1116: added in front of the arguments, this transformation is one that can

1117: be easily implemented in a low-level abstract machine.

1118: 

1119: Although the de Bruijn notation obviates $\alpha$-conversion in the

1120: determination of equality, renaming or, more precisely, renumbering is

1121: still necessary in the correct realization of $\beta$-contraction. To

1122: understand what exactly is needed, let us consider the reduction of

1123: the term $\lambdax {x} ((\lambdax {y} \lambdax {z} y \app x)\app

1124: (\lambdax {w} x))$ whose de Bruijn representation, as we have seen, is

1125: $\lambda\, ((\lambda\, \lambda\, \#2\app \# 3) \app (\lambda\, \#

1126: 2))$. This term reduces to $\lambdax {x}\lambdax {z} ((\lambdax {w} x)

1127: \app x)$, a term whose de Bruijn representation is $\lambda\,\lambda\,

1128: ((\lambda\, \#3) \app \#2)$. Comparing the two de Bruijn terms, we

1129: observe the following. First, there may be free variables in the

1130: argument part of a redex and the indices corresponding to

1131: these may have to be renumbered as it is substituted into the body

1132: upon performing a $\beta$-contraction; in the example considered, the

1133: subterm $(\lambda\, \#2)$ is transformed into $(\lambda\, \#3)$ by

1134: this process. Second, $\beta$-contraction

1135: eliminates an abstraction and the indices for variable occurrences

1136: that were free in the body have to be decremented by $1$ to

1137: account for this action; once again, in our example, this is reflected

1138: in the renumbering of the index $3$ in the body of the redex to

1139: $2$. This part of the renumbering work can, however, be realized in

1140: the same structure traversal that carries out the substitution of the

1141: argument into the body of the redex.

1142: 

1143: Renaming is, of course, also necessary in $\beta$-contraction under a

1144: name-based representation. However, in contrast to the situation under

1145: the nameless scheme, renaming now affects only the body of a

1146: redex. Thus, in $\beta$-contracting the term  

1147: $(\lambdax{x} t_1)\app t_2$, it is necessary to consider renaming only

1148: the variables 

1149: explicitly bound within the subterm $t_1$. Even this kind of renaming

1150: can be avoided if it can be determined that the names of these bound

1151: variables do not clash with those of the free variables in

1152: $t_2$. However determining this requires a traversal of the argument

1153: part of the redex to calculate the set of variables that are free in

1154: it. A more efficient approach, used, for instance, in \cite{AP81}, is

1155: to always rename but, in a manner similar to that suggested for the de

1156: Bruijn case, to fold such renamings into the same structure traversal

1157: that realizes the $\beta$-contraction substitution.  

1158: 

1159: From this discussion, it becomes clear that the separating factor

1160: between the name-based and nameless treatments of bound variables from

1161: the perspective of implementing $\beta$-contraction is the effort

1162: expended in renumbering the argument parts of redexes under

1163: the latter regime. We believe this effort to be 

1164: small in practice for two reasons. First, actual renumbering can be

1165: often be finessed.  For example, if there are no externally bound

1166: variables in the argument of the redex or if substitution is

1167: not made into a context embedded under abstractions, then renumbering

1168: is actually vacuous. This, in fact, is often the situation under a

1169: popular style of programming in $\lambda$Prolog

1170: \cite{miller91jlc},

1171: and other features of the lambda term representation that we describe

1172: in this section allow such properties to be recognized and

1173: utilized in reduction.  Second, not all the cases where a nontrivial

1174: renumbering needs to be done constitute an extra cost. In general, when a 

1175: term is substituted in, it is necessary also to examine its

1176: structure and possibly reduce it to an appropriate normal form. The

1177: necessary renumbering can, in this case, be incorporated into the same

1178: walk as the one that carries out this introspection. The main drawback

1179: of this approach is that it leads to a loss of sharing in reduction if

1180: the same term is substituted, and reduced, in more than one place since

1181: the required renumbering may be different in each of these contexts.

1182: However, empirical evidence suggests that the actual loss of such

1183: sharing is negligible \cite{LN02}, indicating thereby that any

1184: renumbering can be profitably folded into a required reduction walk.  

1185: 

1186: In summary, then, the de Bruijn representation of bound variables has

1187: few real drawbacks in realizing $\beta$-contraction and significant

1188: advantages in checking identity modulo $\alpha$-conversion and

1189: implementing higher-order unification. It has been used for this

1190: reason in the {\it Teyjus} implementation and we orient the rest

1191: of our discussion of term representation around it.

1192: 

1193: \subsection{Encoding Substitutions in Terms}\label{ssec:laziness}

1194: The manner in which substitutions are effected over lambda terms is

1195: critical to the efficiency of implementation of the $\beta$-contraction

1196: operation. A potentially desirable feature in the realization of such

1197: substitutions is the ability to perform them in a lazy fashion. For

1198: example, consider the task of determining whether the (de Bruijn)

1199: terms  

1200: $((\lambda\, \lambda\,\lambda\,\#3\app \#2\app s)\app (\lambda\, \#1))$

1201: and $((\lambda\, \lambda\,\lambda\,\#3\app \#1\app t)\app (\lambda\,

1202: \#1))$ can be unified. We assume that $s$ and $t$ denote arbitrary  

1203: terms here.  We can conclude that these two terms cannot be unified by

1204: observing that they reduce respectively to $\lambda\,\lambda\,\#2\app

1205: s'$ and $\lambda\,\lambda\,\#1\app t'$, where $s'$ and $t'$ are

1206: terms that result from $s$ and $t$ by appropriate substitutions. In

1207: making this determination, we do not actually need to calculate the

1208: results of the substitutions over the terms $s$ and $t$. To

1209: achieve this conservation of effort, however, it is necessary 

1210: that we be able to represent $s'$ and $t'$ as  combinations of $s$ and

1211: $t$ with relevant substitutions. Similarly, consider the reduction of   

1212: a term of the form $((\lambda\, ((\lambda\, t_1)\app t_2)) \app t_3)$ to

1213: head normal form. Let $t'_2$ be the term obtained from $t_2$ by

1214: substituting $t_3$ for the first free variable and decrementing 

1215: the indices of all the other free variables by one. Then, producing

1216: the head normal form involves substituting $t'_2$ and $t_3$ for the first

1217: and second free variables in $t_1$ and decrementing the

1218: indices of all other free variables by two. Each of these substitutions 

1219: involves a walk over the {\it same} structure, \ie, the

1220: structure of $t_1$. It would obviously be beneficial if all these

1221: traversals could be combined into one. The ability to do this depends,

1222: once again, on the possibility of temporarily suspending a

1223: substitution generated by a $\beta$-contraction so that it can later

1224: be composed with other substitutions.

1225: 

1226: The delaying of substitutions has, in fact, been used extensively in

1227: the implementation of functional programming languages (\eg, see

1228: \cite{CCM87,FW87,HM76}). In these contexts, the necessary delaying

1229: is realized by the simple device of combining a term with

1230: an environment that represents bindings for free variables that

1231: occur in it. When the de Bruijn representation is used, this simple

1232: device is  

1233: adequate only if the overall term is closed and if subterms

1234: embedded within abstractions need not be explored. These

1235: assumptions are acceptable in the implementation of

1236: functional programming languages but, unfortunately, not

1237: in the context of interest to us: the production of the head normal

1238: forms needed during unification may well require the

1239: $\beta$-contraction of redexes embedded within abstractions as well as the

1240: propagation of substitutions under abstractions. In these cases, a

1241: more complicated 

1242: substitution operation needs to be encoded. Thus, suppose that we need

1243: to $\beta$-contract a term of the form $(\lambda\, t) \app s$ that

1244: appears embedded within some abstractions. Now, $t$ might contain

1245: variables that are bound by outside abstractions. If the result of

1246: $\beta$-contracting this redex is to be encoded by the term $t$ and an

1247: `environment', the environment must record not just the substitution

1248: of $s$ for the first free variable in $t$ but also the decrementing of

1249: the indices corresponding to all the other free variables. Similarly, 

1250: imagine that we wish to propagate an environment 

1251: under the

1252: abstraction in a term of the form $\lambda\, t$. If the result is to

1253: be represented by a term of the form $\lambda\, t'$ where $t'$ is

1254: itself encoded as $t$ and an environment, then this environment must

1255: be obtained from the earlier one by `shifting up' the index for the

1256: variables to be substituted for by one and adding an identity

1257: substitution for the variable with index $1$. Further, the indices of

1258: the free variables in the terms that appear in the environment must

1259: themselves be incremented by $1$.

1260: 

1261: Explicit substitution notations that have been developed in recent

1262: years for the lambda calculus offer a complete treatment of this kind

1263: of encoding of substitutions

1264: \cite{ACCL91,BBLR96,Field90,KR97,NW98tcs}. We outline here a version

1265: of such a notation that we have developed for use specifically in the

1266: implementation of our higher-order language

1267: \cite{Nad99jflp}.\footnote{This notation has also been used in the

1268:   Standard ML of New Jersey compiler \cite{shao98:imp}.} Our

1269: notation builds on the traditional de Bruijn notation by adding a 

1270: new category of terms called a suspension. A suspension represents a

1271: `skeletal' term together with a suspended substitution. Such a term

1272: has the structure $\env{t,ol,nl,e}$, where $t$ is a term, $ol$ and

1273: $nl$ are natural numbers and $e$ is an environment. This suspension

1274: corresponds, intuitively, to a term $t$ 

1275: that used to occur inside $ol$ abstractions but that now appears

1276: within $nl$ of them. In generating the underlying de Bruijn term,

1277: therefore, the bound variables with indices greater than $ol$ have to

1278: have their index values adjusted by the difference between $ol$ and

1279: $nl$. Substitutions for 

1280: the first $ol$ bound variables are, on the other hand, contained in

1281: the environment $e$. 

1282: Conceptually, the elements of such an environment are 

1283: either substitution terms generated by a contraction or are dummy

1284: substitutions corresponding to abstractions that persist in an outer

1285: context. 

1286: However, some renumbering of indices may have to be done at the place

1287: of actual substitution. To encode this renumbering, each element of

1288: the environment is annotated with  the number of remaining

1289: abstractions under which the abstraction relevant to that element

1290: appears. This relative `embedding level' can be used

1291: together with the overall embedding level $nl$ to completely determine

1292: the needed renumbering. 

1293: 

1294: The syntax of lambda terms in the new notation is given formally 

1295: by the category $\langle T \rangle$ defined by the following rules:  

1296: \begin{tabbing}

1297: \qquad\=$\langle ET\rangle$\ \=::=\ \=\kill

1298: \>$\langle ET \rangle$\> ::= \> $\dum \langle N \rangle\ \vert\

1299: (\langle T \rangle, \langle N \rangle)$\\

1300: \>$\langle E \rangle$\> ::= \> ${\it nil}\ \vert\ \langle

1301: ET \rangle :: \langle E \rangle$\\

1302: \>$\langle T\rangle$\>::=\>$\langle C \rangle \ \vert\ \langle

1303: V \rangle \ \vert  \ \#\langle I \rangle\ \vert\ (\langle

1304:  T\rangle\ \langle T\rangle)\ \vert \ (\lambda \langle T\rangle)\

1305:  \vert\ \env{\langle T\rangle,\langle N \rangle, \langle N \rangle,

1306:  \langle E \rangle}$

1307: \end{tabbing}

1308: \noindent In these rules, $\langle C \rangle$ and $\langle V

1309: \rangle$ represent constants and logic variables, $\langle I

1310: \rangle$ is the category of positive numbers 

1311: and $\langle N \rangle$ is the category of natural numbers. Further,

1312: $\langle E \rangle$ and $\langle ET \rangle$ are to be read as the

1313: categories of environments and environment terms, respectively. Terms

1314: of the form $\env{t,i,j,e}$ must satisfy certain wellformedness

1315: constraints that have a natural basis in our informal understanding of 

1316: their content: viewing the environment $e$ as a list, its length must

1317: be equal to $i$, each element of it of the form $\dum(l)$ must be such

1318: that $l < j$ and each element of the form $(t,l)$ must be

1319: such that $l \leq j$. 

1320: 

1321: \begin{figure}

1322: \begin{tabbing}

1323: \qquad\=(r8)\quad\=\qquad\qquad\qquad\=\kill

1324: \>($\beta_s$)\> $(\lambda t_1)\app t_2 \lra \env{ t_1, 1,

1325: 0, (t_2,0) :: {\it nil}}$\\[5pt]

1326: \> ($\beta'_s$)\> $(\lambda

1327: \env{t_1,ol+1,nl+1,\dum{nl}::e})\app t_2 \lra \env{ t_1,ol+1,nl, 

1328: (t_2,nl) :: e }$\\[5pt]

1329: \>(r1)\> $\env{c,ol,nl,e} \lra c$, provided $c$ is a constant.\\[5pt]

1330: \>(r2)\> $\env{x,ol,nl,e} \lra x$, provided $x$ is a logic variable.\\ [5pt]

1331: \> (r3)\>$\env{\#i,ol,nl,e} \lra \#j$, provided $i > ol$ and $j = i - ol + nl$.\\[5pt]

1332: \> (r4)\>$\env{\#i,ol,nl, e} \lra \#j$, provided $i \leq ol$ and $e[i] = \dum(l)$ and $j = nl - l$.\\ [5pt]

1333: \> (r5)\> $\env{\#i,ol,nl,e} \lra \env{t,0,nl - l,{\it nil}}$,\\

1334: \>\> provided $i \leq ol$ and $e[i] = (t,l)$ and $j = nl - l$.\\ [5pt]

1335: \> (r6)\> $\env{t_1\app t_2,ol,nl,e} \lra

1336: \env{t_1,ol,nl,e}\app \env{t_2,ol,nl,e}$.\\[5pt]

1337: \> (r7)\>$\env{\lambda t, ol, nl, e} \lra \lambda \env{t,

1338: ol+1, nl+1, \dum{nl} :: e}$.\\[5pt]

1339: \>(r8)\>$\env{\env{t,ol,nl,e},0,nl',{\it nil}} \lra \env{t,ol,nl+nl',e}$.\\[5pt]

1340: \>(r9)\>$\env{t,0,0,{\it nil}} \lra t$.

1341: \end{tabbing}

1342: \caption{Rule schemata for rewriting terms in the suspension notation}

1343: \label{fig:rewriterules}

1344: \end{figure}

1345: 

1346: In addition to the syntactic expressions, the suspension notation

1347: includes a collection of rewrite rule schemata whose purpose is to

1348: simulate $\beta$-contractions. These schemata are presented in

1349: Figure~\ref{fig:rewriterules}. In these rules we use the notation

1350: $e[i]$ to denote the $i^{th}$ element of the environment. Of the rules

1351: presented, the ones labelled ($\beta_s$) and ($\beta'_s$) generate the

1352: substitutions corresponding to the $\beta$-contraction rule on de

1353: Bruijn terms and the rules (r1)-(r9), referred to as the {\it reading

1354: rules}, serve to actually carry out these substitutions. 

1355: 

1356: The ($\beta'_s$) schema has a special

1357: place in the calculus: it makes possible the

1358: combination of substitutions arising from different

1359: $\beta$-contractions. To understand its use, let us consider the

1360: head normalization of the term $(\lambda\, 

1361: ((\lambda\, t_1)\app t_2)) \app t_3$. As the first step in this

1362: process, we might produce the term  

1363: $\env{(\lambda\, t_1)\app t_2, 1, 0, (t_3,0) :: {\it nil}}$.

1364: The substitution may now be percolated inwards using the reading rules

1365: so as to reveal a $\beta$-redex at the top level. This produces the term

1366: \begin{tabbing}

1367: \qquad\=\kill

1368: \>$(\lambda\, \env{t_1,2,1,\dum(0)::(t_3,0) :: {\it nil}})\app

1369: \env{t_2,1,0,(t_3,0)::{\it nil})}$.

1370: \end{tabbing}

1371: \noindent At this point the $\beta'_s$ rule schema is applicable and

1372: using it 

1373: produces the term 

1374: \begin{tabbing}

1375: \qquad\=\kill

1376: \>$\env{t_1,2,0,(\env{t_2,1,0,(t_3,0)::{\it nil}},0) :: (t_3,0) :: {\it nil}}$. 

1377: \end{tabbing}

1378: \noindent Notice that the substitutions generated by contracting the

1379: two $\beta$-redexes have been combined at this point into one

1380: environment and can be performed in a single walk over the structure

1381: of $t_1$.  

1382: 

1383: In the translation of a suspension, it will eventually be necessary to

1384: substitute the arguments of $\beta$-redexes for bound variable

1385: indices. This operation is carried out in our calculus by instances of

1386: the rule schema (r5). There is, in general, a necessity to renumber

1387: indices in the term being substituted in and this is manifest in the

1388: schema (r5) in the construction of a suitable suspension. The rule

1389: schemata (r8) and (r9) recognize special circumstances relative to such

1390: renumbering. The schema (r9) allows vacuous renumbering

1391: to be eliminated. By so 

1392: doing, this rule facilitates a continued sharing relative to the

1393: substituted term. The schema (r8), on the other hand, permits a

1394: nontrivial renumbering walk to be combined with a walk affecting

1395: substitutions arising out of earlier $\beta$-contractions. Uses of the

1396: schemata (r8) and (r9) can be folded into the application of the

1397: schema (r5) and this is actually done in the {\it Teyjus}

1398: implementation. An interesting aspect of our overall system is that by

1399: utilizing the ($\beta'_s$), (r8) and (r9) schemata within the control

1400: strategy for generating head normal forms that we describe later, it

1401: is possible to eliminate nearly all occurrences of nested

1402: suspensions in practice. This has obvious

1403: consequences with respect to the sharing of substitution walks.  

1404: 

1405: While there is a case in principle for laziness in performing

1406: substitutions, it is still necessary to determine how this plays out

1407: in real applications. In situations where lambda terms are employed in

1408: an essential way in programming, empirical studies indicate that using

1409: the suspension notation and the rules ($\beta'_s$) and (r8)

1410: judiciously can reduce substitution walks to between a third and an

1411: eighth of what is needed when substitutions are performed eagerly

1412: \cite{LN02}. There is a noticeable reduction in computation time as a

1413: result, up to 35\%---measured over all computations, including

1414: backchaining over logic programming clauses---in some important cases.

1415: 

1416: \subsection{A Dependence Annotation on Terms}\label{ssec:dependency}

1417: There is a refinement to the suspension notation that can have

1418: practical benefits. This refinement consists of annotating

1419: terms to determine whether or not they contain variables bound by 

1420: external abstractions. Referring to the two categories of terms as

1421: open and closed with obvious connotations, these annotations can be

1422: determined statically for de Bruijn terms as follows. At the atomic

1423: level, de Bruijn indices are open whereas logic variables

1424: and constants are closed. For complex terms, an application is open 

1425: if either its `function' or `argument' part is open and is closed

1426: otherwise, and an abstraction is open

1427: exactly when there is a bound variable occurrence within its scope

1428: that has a (relative) index greater than $1$. Rewrite rules that

1429: transform terms in the course of computation can be modified in a

1430: straightforward way to maintain and propagate these annotations. For

1431: example, if a $\beta$-redex of the form $(\lambda\, t_1)\app t_2$ is

1432: closed, then the suspension $\env{t_1,1,0,(t_2,0)::{\it nil}}$ that is

1433: generated from it must also be closed. Similarly, given a suspension

1434: of the form $\env{t_1 \app t_2, ol, nl, e}$ that is closed, the two

1435: top-level components of the term $(\env{t_1,ol,nl,e}\app

1436: \env{t_2,ol,nl,e})$ that is obtained from distributing the substitution

1437: over the application must be closed. A complete presentation of these

1438: refined rewrite rules and a characterization of their properties may

1439: be found in \cite{Nad99jflp}. 

1440: 

1441: The cost of maintaining the annotations discussed can be made

1442: small by using suitable low-level devices. In the emulator that is

1443: part of the {\it Teyjus} system, for example, an otherwise unused

1444: low-end bit is employed to indicate the annotation and the

1445: determination and setting of its value is folded into the overall

1446: manipulation of term tags. The advantage of maintaining annotations is

1447: at least twofold. First, the rewriting effort in determining the head

1448: normal form of a given term can be reduced. For example, consider a

1449: term of the form $\env{t,i,j,e}$ where it is known that $t$ is a term

1450: that is not dependent on outside abstractions. Then this term can be

1451: simplified immediately to (a pointer to) $t$. Second, this kind of

1452: simplification can foster a greater sharing of terms and,

1453: consequently, of rewriting steps. Thus, consider, once again, the term

1454: $\env{t,ol,nl,e}$, but this time assuming that $t$ is of the form

1455: $(t_1\app t_2)$ that may possibly be shared with other 

1456: contexts. Attempting to reduce this term to head normal form in a

1457: situation where annotations are not used would result in the

1458: production of the term $(\env{t_1,ol,nl,e}\app \env{t_2,ol,nl,e})$, in 

1459: the process breaking the sharing over $t$. In contrast, with the use

1460: of annotations, the given suspension term will be simplified

1461: immediately to $t$ and the subsequent reduction of $t$ will be shared

1462: with all the other contexts in which it is used. 

1463: 

1464: An obvious question is if the virtues of annotations are

1465: relevant to realistic computations in our higher-order language. We

1466: mention two situations in which these could be of benefit. In the

1467: first instance, observe that the substitutions that are computed by

1468: the higher-order unification process are actually closed in the sense

1469: discussed. Now, if occurrences of the variables being substituted for

1470: appear embedded within $\beta$-redexes, then the propagation of

1471: reduction substitutions over instantiations of these variables can be

1472: calculated trivially by utilizing annotations. As another example

1473: consider a $\beta$-redex of the form $(\lambda\, t_1)\app t_2$ where

1474: $t_2$ is a closed term as would be the case if this term appears 

1475: statically at the top-level. The contraction of this term yields

1476: the suspension $\env{t_1,1,0,(t_2,0)::{\it nil}}$. The percolation of the 

1477: substitution of $t_2$ over the structure of $t_1$ might eventually

1478: lead to the replacement of a bound variable index by $t_2$. With

1479: reference to the rules in Figure~\ref{fig:rewriterules}, this

1480: replacement would produce a term of the form $\env{t_2,0,l,{\it nil}}$, \ie,

1481: a term that corresponds to $t_2$ with a suitable renumbering of

1482: indices corresponding to free variable occurrences. By utilizing the

1483: fact that $t_2$ is known to be closed, the renumbering can be effected

1484: trivially. Furthermore, the bound variable that $t_2$ needs to be

1485: substituted for may occur in more than one place within $t_1$. In this

1486: case the use of the annotation on $t_2$ will also be responsible for

1487: the preservation of a meaningful sharing opportunity. 

1488: 

1489: At an empirical level, we have observed that the use of annotations

1490: yields a substantial speedup relative to an eager approach to

1491: propagating reduction substitutions, the reduction in computation time

1492: being over 70\% in several cases \cite{LN02}. While there is still a

1493: payoff from annotations when laziness in substitution and the

1494: combination of substitution walks as described in

1495: Section~\ref{ssec:laziness} are used, these appear to be of a much

1496: smaller kind. Thus, certain optimizations seem to overlap with others

1497: and a better understanding of these interactions is needed.

1498: 

1499: \subsection{The Implementation of Reduction}\label{ssec:red}

1500: An issue of obvious importance is the order in which various

1501: operations are to be carried out on terms. From the perspective of

1502: unification, the main requirement is that of transforming terms into a

1503: form in which the head is exposed; in particular, the arguments of

1504: terms may be left in the form of suspensions. The idea of head normal

1505: forms has been generalized to the suspension notation and its

1506: relationship to the conventional understanding of this notion has been

1507: explored in \cite{Nad99jflp} as a prelude to its use in

1508: unification. At an implementation level, a strategy that might be used

1509: is one that produces these head normal forms only on demand and that

1510: does this by repeatedly rewriting the leftmost, outermost redex

1511: relative to the rules in Figure~\ref{fig:rewriterules} till such time

1512: that an atomic head is revealed, possibly embedded under some

1513: abstractions.  This strategy is an obvious generalization of the one

1514: used for rewriting $\beta$-redexes towards producing head normal forms

1515: in the usual setting and also has practical advantages: it provides

1516: the basis for delaying substitution walks as discussed in

1517: Section~\ref{ssec:laziness} and the different possibilities for

1518: combining term traversals during substitution and the adjustment of

1519: indices present themselves within it as well-defined choices between

1520: rewrite rules applicable at the same time. We discuss the realization

1521: of this approach within the {\it Teyjus} system further in

1522: Section~\ref{ssec:norm}.

1523: 

1524: Another issue to consider is whether to implement the rewriting of

1525: terms in a destructive or non-destructive manner. To understand 

1526: the tradeoffs involved, let us consider the reduction of the term

1527: $\lambda\, \lambda\, ((\lambda\, t_1)\app t_2)$, in which 

1528: $t_1$ and $t_2$ are arbitrary terms, to head normal form.

1529: Anticipating a discussion of internal representations, we may depict 

1530: terms by graphical structures. Each term in such a representation

1531: translates to a node labelled with its category and containing its

1532: fixed length parts and pointers to relevant subterms and

1533: environments. Assuming such a visualization, the internal structure of

1534: the term of interest may be shown by the graph in the

1535: left half of Figure \ref{fig:internal}. Now, this term has a

1536: redex, given by the subterm $(\lambda\, t_1)\app t_2$, that

1537: has to be $\beta$-contracted in producing a head normal form.  If a

1538: destructive implementation of reduction is used, then this rewriting

1539: step will be effected by replacing the redex in-place by the 

1540: term $\env{t_1,1,0,(t_2, 0)::{\it nil}}$.\footnote{The representation of

1541: different kinds of terms generally require different amounts of space

1542: in an concrete realization. In this case, a destructive change may

1543: be achieved by using a special kind of term that serves as a

1544: `reference' to a value stored elsewhere.}

1545: The consequences of this replacement will be felt immediately in all

1546: places where the redex appears as a subterm. If the

1547: $\beta$-contraction is done non-destructively, on the other hand, the

1548: subterm would be left intact but a new suspension term would be

1549: returned. To obtain the effect of this rewriting step in the overall

1550: context, it would now be necessary to replicate around the suspension

1551: the structure of the term within which the redex is embedded.

1552: Thus, a non-destructive implementation of the

1553: $\beta$-contraction operation would eventually have to produce the

1554: structure shown in the right half of Figure \ref{fig:internal}. 

1555: 

1556: \begin{figure}

1557: \begin{center}

1558: \setlength{\unitlength}{0.00075000in}

1559: %

1560: \begingroup\makeatletter\ifx\SetFigFont\undefined%

1561: \gdef\SetFigFont#1#2#3#4#5{%

1562:   \reset@font\fontsize{#1}{#2pt}%

1563:   \fontfamily{#3}\fontseries{#4}\fontshape{#5}%

1564:   \selectfont}%

1565: \fi\endgroup%

1566: {\renewcommand{\dashlinestretch}{30}

1567: \begin{picture}(6087,4522)(0,-10)

1568: \path(4725,1297)(4725,1597)

1569: \path(5175,1297)(5175,1597)

1570: \path(5925,1597)(5925,1297)

1571: \path(5925,1522)(6075,1597)

1572: \path(5925,1297)(6075,1372)

1573: \path(5925,1372)(6075,1447)

1574: \path(4275,1597)(5625,1597)(5625,1297)

1575: 	(4275,1297)(4275,1597)

1576: \put(4875,1372){\makebox(0,0)[lb]{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}0}}}

1577: \path(5925,1447)(6075,1522)

1578: \path(4500,1447)(4499,1447)(4497,1446)

1579: 	(4493,1444)(4487,1441)(4478,1437)

1580: 	(4467,1431)(4452,1424)(4434,1415)

1581: 	(4412,1405)(4387,1393)(4359,1380)

1582: 	(4327,1365)(4293,1349)(4256,1332)

1583: 	(4216,1313)(4174,1294)(4131,1275)

1584: 	(4085,1254)(4038,1234)(3990,1213)

1585: 	(3941,1192)(3890,1170)(3839,1149)

1586: 	(3786,1128)(3733,1107)(3679,1086)

1587: 	(3623,1066)(3566,1045)(3509,1025)

1588: 	(3449,1005)(3388,985)(3326,966)

1589: 	(3262,947)(3196,928)(3128,910)

1590: 	(3060,893)(2990,876)(2920,861)

1591: 	(2850,847)(2765,832)(2683,819)

1592: 	(2607,809)(2537,801)(2474,794)

1593: 	(2418,789)(2369,785)(2326,783)

1594: 	(2289,781)(2257,780)(2229,780)

1595: 	(2206,780)(2186,781)(2168,782)

1596: 	(2152,783)(2138,784)(2123,787)

1597: 	(2109,789)(2094,792)(2078,795)

1598: 	(2060,799)(2040,804)(2018,809)

1599: 	(1993,815)(1965,823)(1935,832)

1600: 	(1902,842)(1866,854)(1830,868)

1601: 	(1793,884)(1758,902)(1725,922)

1602: 	(1693,947)(1669,974)(1650,1003)

1603: 	(1637,1031)(1630,1060)(1627,1090)

1604: 	(1629,1119)(1634,1148)(1642,1178)

1605: 	(1653,1207)(1667,1236)(1682,1265)

1606: 	(1700,1294)(1718,1323)(1737,1351)

1607: 	(1757,1377)(1776,1403)(1794,1426)

1608: 	(1812,1448)(1827,1467)(1841,1483)

1609: 	(1852,1496)(1861,1506)(1875,1522)

1610: \path(1818.557,1411.936)(1875.000,1522.000)(1773.402,1451.446)

1611: \path(4050,2272)(4050,2271)(4050,2269)

1612: 	(4050,2266)(4050,2261)(4050,2254)

1613: 	(4050,2244)(4050,2231)(4050,2215)

1614: 	(4049,2197)(4048,2175)(4048,2151)

1615: 	(4046,2123)(4045,2093)(4042,2061)

1616: 	(4040,2026)(4036,1989)(4032,1951)

1617: 	(4027,1911)(4022,1869)(4015,1827)

1618: 	(4007,1783)(3998,1739)(3988,1694)

1619: 	(3976,1648)(3963,1601)(3947,1555)

1620: 	(3930,1507)(3911,1459)(3890,1410)

1621: 	(3866,1361)(3840,1311)(3810,1260)

1622: 	(3777,1208)(3741,1155)(3701,1102)

1623: 	(3657,1048)(3609,993)(3556,937)

1624: 	(3500,882)(3439,826)(3375,772)

1625: 	(3314,724)(3251,678)(3187,634)

1626: 	(3124,592)(3062,553)(3002,517)

1627: 	(2945,484)(2889,453)(2837,425)

1628: 	(2788,400)(2741,377)(2698,357)

1629: 	(2658,338)(2620,322)(2585,307)

1630: 	(2552,294)(2521,283)(2492,273)

1631: 	(2464,264)(2438,255)(2412,248)

1632: 	(2387,241)(2362,234)(2338,228)

1633: 	(2313,222)(2287,216)(2260,210)

1634: 	(2232,203)(2202,197)(2170,189)

1635: 	(2136,182)(2099,173)(2060,165)

1636: 	(2017,155)(1971,145)(1922,134)

1637: 	(1870,123)(1814,111)(1754,98)

1638: 	(1692,86)(1626,73)(1558,61)

1639: 	(1488,50)(1417,39)(1346,30)

1640: 	(1275,22)(1187,15)(1103,12)

1641: 	(1024,13)(951,16)(882,22)

1642: 	(819,30)(760,40)(706,53)

1643: 	(656,67)(610,83)(567,100)

1644: 	(528,118)(491,138)(456,158)

1645: 	(424,180)(394,202)(366,224)

1646: 	(340,247)(315,270)(293,293)

1647: 	(271,315)(252,337)(234,357)

1648: 	(219,377)(205,395)(192,411)

1649: 	(182,426)(173,438)(166,448)

1650: 	(160,456)(156,463)(150,472)

1651: \path(241.526,388.795)(150.000,472.000)(191.603,355.513)

1652: \put(900,2572){\makebox(0,0)[lb]{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\it app}}}}

1653: \put(4050,3472){\makebox(0,0)[lb]{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\it lam}}}}

1654: \put(900,3472){\makebox(0,0)[lb]{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\it lam}}}}

1655: \put(4050,4372){\makebox(0,0)[lb]{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\it lam}}}}

1656: \put(900,4372){\makebox(0,0)[lb]{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}{\it lam}}}}

1657: \put(0,1672){\makebox(0,0)[lb]{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}{\it lam}}}}

1658: \path(75,1522)(75,922)

1659: \path(45.000,1042.000)(75.000,922.000)(105.000,1042.000)

1660: \path(5550,1447)(5925,1447)

1661: \path(5805.000,1417.000)(5925.000,1447.000)(5805.000,1477.000)

1662: \path(975,2422)(150,1897)

1663: \path(235.133,1986.735)(150.000,1897.000)(267.346,1936.115)

1664: \path(1125,2422)(1875,1897)

1665: \path(1759.488,1941.239)(1875.000,1897.000)(1793.896,1990.392)

1666: \path(4200,3322)(4200,2797)

1667: \path(4170.000,2917.000)(4200.000,2797.000)(4230.000,2917.000)

1668: \path(1050,3322)(1050,2797)

1669: \path(1020.000,2917.000)(1050.000,2797.000)(1080.000,2917.000)

1670: \path(1050,4222)(1050,3697)

1671: \path(1020.000,3817.000)(1050.000,3697.000)(1080.000,3817.000)

1672: \path(4200,4222)(4200,3697)

1673: \path(4170.000,3817.000)(4200.000,3697.000)(4230.000,3817.000)

1674: \path(4500,2272)(4500,1597)

1675: \path(4470.000,1717.000)(4500.000,1597.000)(4530.000,1717.000)

1676: \put(1875,1672){\makebox(0,0)[lb]{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$t_2$}}}

1677: \put(4050,2572){\makebox(0,0)[lb]{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}{\it susp}}}}

1678: \put(0,622){\makebox(0,0)[lb]{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$t_1$}}}

1679: \put(3900,2272){\makebox(0,0)[lb]{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}(\,\ ,1,0,\,\    )}}}

1680: \end{picture}

1681: }

1682: 

1683: \end{center}

1684: \caption{Non-destructive reduction of lambda terms}

1685: \label{fig:internal}

1686: \end{figure}

1687: 

1688: Based on the above understanding, a destructive implementation

1689: appears to be an obvious choice in a context where 

1690: reduction is deterministic, \ie, where future

1691: events will not require rewriting steps to be undone. The in-place

1692: replacement obviates a copying of the embedding context. Furthermore,

1693: it is only such a replacement that admits of any possibility of

1694: sharing in 

1695: reduction; the effect of replacing $(\lambda\, t_1)\app t_2$ with

1696: $\env{t_1,1,0,(t_2,0)::{\it nil}}$ will be felt in other contexts only if

1697: the term is changed physically at the place where these point to. A

1698: non-destructive implementation actually has an additional cost that is

1699: inhibiting. Consider, for instance, an attempt to head normalize a

1700: term that is already in head normal form but that is not known

1701: statically to be in this form. Since copying of structure is needed in

1702: some cases, a naive implementation might simply replicate the

1703: structure of the term even when its subparts are unchanged. However,

1704: this is undesirable: a mere `look-up' should not cause a new structure

1705: to be created. This kind of a copying can be avoided by putting

1706: explicit checks into the normalization procedure to determine when

1707: copying is necessary.  This incurs a time penalty that does not arise

1708: in a destructive implementation.

1709: 

1710: Our interest is, of course, eventually in a context where backtracking

1711: over reduction computations may be necessary. As a specific example, a

1712: $\beta$-redex may manifest itself in a term as a result of a

1713: substitution for a variable that may have to be repealed at a later

1714: point. In this situation, a destructive implementation has the drawback

1715: that the in-place changes may have to be trailed to facilitate a

1716: subsequent resetting of state. A interesting point to note is that

1717: the form of trailing that is needed here is one that saves old values

1718: of cells and not simply the pointers to affected cells as in

1719: conventional Prolog implementations. The efficiency of such an

1720: implementation can obviously be improved by mechanisms that detect

1721: redundancy in trailing. The simplest method that can be used for this

1722: purpose is one that compares the location in heap of the term being

1723: changed with the most recent heap backtrack point to decide the

1724: necessity for trailing. Controlled forms of eagerness that push

1725: necessary rewriting steps to before the setting up of choice points

1726: are also useful. Another aspect that bears careful investigation is

1727: the possibility of committing to heap a cascade of reduction

1728: steps, such as those corresponding to a $\beta$-contraction and the 

1729: propagation of the substitution it generates, only at the very end,

1730: thereby obviating the retraction of intermediate steps. The present

1731: version of the {\it Teyjus} system employs a graph based, 

1732: destructive implementation of reduction and, as such, provides an

1733: effective vehicle for experimenting with these various

1734: possibilities.\footnote{Such experimentation with reduction

1735:   strategies has actually been carried out since the preparation of

1736:   this paper. Details may be found in \cite{NX03} and \cite{LNX03}.}

1737: 

1738: The implementation of logic programming languages have, in the past,

1739: consider two different methods for the treatment of terms appearing in

1740: program clauses. In the structure sharing approach, these

1741: are represented as a combination of a fixed structure and bindings for

1742: variables \cite{War77}. In the more popular structure copying approach,

1743: entirely new copies of these terms are created through compiled code

1744: in each instance of use \cite{War83}. The destructive

1745: implementation of reduction is compatible only with this structure

1746: copying approach and we therefore assume its use in later

1747: sections. 

1748: 

1749: \subsection{Internal Representation}\label{ssec:intrep}

1750: The final issue that we consider is the low-level representation of

1751: terms that embodies the various mechanisms that we have described.

1752: The most natural such encoding is the one that uses a cell

1753: bearing a tag that indicates the relevant syntactic category for each

1754: term and that is complemented by additional cells containing

1755: information about further components. In the case that the dependency

1756: annotations discussed in Section~\ref{ssec:dependency} are used, it is

1757: best if the information they provide can also be accessed

1758: independently of the term category. In the emulator underlying the {\it

1759: Teyjus} implementation, this purpose is achieved by reserving the

1760: low-end bit of the tag bearing cell for these annotations. 

1761: 

1762: The information that needs to be provided in addition to the term

1763: category depends, of course, on the category of the term. 

1764: If this is a constant or a bound variable, all that is needed is a

1765: pointer to the descriptor for the constant or the index, and this can

1766: be folded into the cell bearing the tag. In the case of a

1767: logic variable that is as yet uninstantiated, the contents of the cell

1768: are unimportant and the instantiation of such a variable is realized by

1769: changing the contents of this cell to correspond to one of the other

1770: term categories. An abstraction cell 

1771: must contain a pointer to the body of the abstraction. 

1772: A suspension term requires the maintenance of its two

1773: indices, a pointer to the skeletal term and a pointer to its

1774: environment. An environment can be represented as a list and,

1775: in this form, admits of considerable sharing. 

1776: 

1777: The representation of the final category of terms, namely,

1778: applications, requires more care. The most natural, and

1779: perhaps the conceptually clearest, approach is to utilize the curried

1780: structure, rendering each application into a pair of pointers to its function

1781: and argument parts. Unfortunately, this kind of rendition incurs a high

1782: cost in the most common form of access to terms. The objective with

1783: terms is typically to get to the heads of their head normal

1784: forms. Further, operations such as term simplification in unification

1785: are best realized if the arguments in a head normal form are available

1786: as a vector. Suppose that we have a term that at compile time has the

1787: structure $\lambda\,\ldots\,\lambda\, (h \app t_1 \ldots t_n)$. If a

1788: curried representation is used for this term, $n$

1789: applications will have to be traversed before the head is

1790: reached and a vector of arguments will also have to be

1791: explicitly constructed in the course of this descent under application

1792: structure.  

1793: 

1794: An alternative encoding of application that is reminiscent of the

1795: treatment of terms in conventional logic programming

1796: implementations is to translate it into a structure containing three

1797: components: a function part, a pointer to a {\it vector} of arguments

1798: and an `arity' that indicates the size of the arguments vector. Such a

1799: representation has especially nice properties when the program at hand

1800: is a first-order one. In this case the top-level structure of every

1801: compound (application) term that is encountered during computation is

1802: already available at compile time. Thus, the head normal forms of

1803: these terms are available without any reduction calculations and

1804: the described representation allows a quick determination of this fact

1805: as well as an immediate access to the functor and arguments

1806: parts. These appear to be important properties since efficiency over

1807: first-order like computations is significant even to a higher-order

1808: logic programming language \cite{MP92}. 

1809: 

1810: Our low-level representation for terms comes close to the 

1811: one generally employed for first-order terms with the described

1812: encoding of applications. However, there are still differences that

1813: should be mentioned. One difference concerns the specific structure

1814: chosen for compound terms. In the first-order case, internal nodes in

1815: the tree representation of terms cannot change. This fact can be

1816: exploited to fold the functor and arguments parts into one vector and,

1817: thereby, to reduce compound terms to a single pointer. A similar

1818: optimization is not possible in the higher-order context. The

1819: contraction of a $\beta$-redex, for instance, transforms an $n$-fold

1820: application into an $(n-1)$-fold one and there must be sufficient

1821: flexibility in the encoding of terms to capture this situation. 

1822: The other difference lies in the registration of destructive

1823: changes for the purposes of backtracking. First-order terms 

1824: evolve during computation only by virtue of bindings for logic

1825: variables. By picking a uniform representation for such variables, 

1826: the state prior to such a change can be recorded simply by retaining a

1827: pointer to the cell for the corresponding variable. This kind of

1828: optimization is not available in the higher-order context when

1829: reduction is implemented destructively and, as we have already noted,

1830: the original value of the modified cell needs also to be remembered in

1831: order to resurrect the previous state.

1832: 

1833: We have up to this point not considered explicitly

1834: the fact that the terms of interest to us have types

1835: associated with them. These types have a twofold role in the language

1836: \cite{NP91}. At one level, they serve to limit the set of acceptable

1837: programs. At another level, they participate in the computational

1838: mechanism of the language; this role is apparent from the manner in

1839: which types determine the imitation and projection substitutions that

1840: are to be generated for a flexible-rigid pair. The first function of

1841: types is relevant to compilation but does not affect the

1842: execution of a program and so does not have a bearing on runtime

1843: representations. As for the second 

1844: purpose, we observe that it is sufficient to maintain types

1845: with only the constants and logic variables appearing in lambda

1846: terms. Maintaining such annotations is also necessary: 

1847: the types of logic variables are needed for both the imitation

1848: and projection substitutions and the types of constants are needed in

1849: determining the imitation substitutions. 

1850: 

1851: The need to maintain types adds a extra component---a pointer to

1852: a type---to the representation of logic variables. The

1853: representation of constants is unchanged since the type information

1854: can be combined with the other data comprising their descriptors. 

1855: While we do not discuss this issue in detail here, in the

1856: presence of polymorphism, types are best represented by pointers to a

1857: type `skeleton' and a type environment \cite{KNW92}. 

1858: The treatment of polymorphism thus adds an extra cell to the

1859: representations of constants and logic variables.

1860: 

1861: \section{Runtime Support for Higher-Order Unification}\label{sec:runtime}

1862: 

1863: We now consider the task of supporting the enhanced notion of

1864: unification present in our language. The

1865: problems that have to be dealt with are threefold. First, it is

1866: necessary to consider the normalization of terms during

1867: execution. Second, states in our abstract interpreter are given also

1868: by disagreement sets and an efficient method for maintaining such sets

1869: explicitly is needed. Finally, higher-order unification has a

1870: branching character, a facet we realize through depth-first search

1871: with backtracking. In implementing this approach, it is necessary to

1872: identify the important components of state that need to be remembered

1873: and also to describe suitable encodings for such information. We

1874: discuss these various issues below and we describe approaches to

1875: accounting for them within an actual implementation.

1876: 

1877: \subsection{Normalization of Terms}\label{ssec:norm}

1878: 

1879: The simplification operation and the postulation of substitutions

1880: within unification depend on terms being presented in (a generalized)

1881: head normal form. Terms can arise during computation that are not in

1882: this form; consider, for instance, the structure of a term after a

1883: substitution dictated by imitation or projection has been made for a

1884: variable of function type that appears in it. Mechanisms for

1885: normalizing terms are therefore needed as also is a protocol for

1886: deploying these at points where head normal forms are desired. 

1887: As discussed in Section~\ref{ssec:red}, a strategy that rewrites the

1888: leftmost, outermost redex at each stage is a natural one to use for

1889: head normalization. The suspension notation allows the substitution

1890: generated by a $\beta$-contraction to be treated as a truly atomic

1891: operation and thereby facilitates an iterative, stack based

1892: realization of this strategy. Such an approach is embedded in the

1893: implementation of normalization within the {\it Teyjus} system. We

1894: sketch this component of the system below as a prelude to

1895: explaining its use in the overall computation scheme. A more detailed

1896: description of the reduction procedure may be found in \cite{Nad98esw}.  

1897: 

1898: The {\it Teyjus} implementation of head normalization actually uses

1899: two stacks called the structures list or {\it SL} stack and the

1900: applications stack, the latter facilitating a destructive 

1901: realization of reduction. Both stacks store references to terms and

1902: can share a common space in an abstract machine, with their tops

1903: growing towards each other. The reduction procedure looks at the term

1904: pointed to by the top of the {\it SL} stack and the value in a global

1905: register {\it NUMARGS} to determine its next step. At the outset, a

1906: reference to the term to be reduced is placed on the top of the {\it

1907: SL} stack and the {\it NUMARGS} register is set to $0$.  The main

1908: actions of the procedure are dependent on the term referenced by the

1909: top of the {\it SL} stack having a non-suspension structure. For this

1910: reason, if this term is a suspension, the first task becomes that of

1911: exposing such a form for it.  This objective is achieved immediately

1912: using one of the reading rules in Figure~\ref{fig:rewriterules} when

1913: the skeleton is itself not a suspension. Otherwise a non-suspension

1914: form must be exposed first for the skeleton and a simple iterative

1915: process that begins by placing a reference to this skeleton on the top

1916: of the {\it SL} stack serves to realize this.  Eventually, when a

1917: non-suspension form is exposed, if the top of the {\it SL} stack is a

1918: reference to an application, this reference is recorded in the

1919: applications stack and is replaced in the {\it SL} stack by a sequence

1920: of references to its ``operand'' and ``operator'' parts, with the {\it

1921: NUMARGS} register being incremented by the number of operands. If the

1922: top of the {\it SL} stack contains a reference to an abstraction, the

1923: action taken depends on the value in the {\it NUMARGS} register. If

1924: this is $0$, the {\it SL} stack reference is replaced by one to the

1925: body of the abstraction. Otherwise, a leftmost, outermost

1926: $\beta$-redex has been found and needs to be contracted. This action

1927: is realized by popping the top two items on the {\it SL} stack, using

1928: them to construct a suitable suspension a reference to which is pushed

1929: onto the {\it SL} stack, destructively updating the application

1930: available from the top of the applications stack and, finally,

1931: decrementing the {\it NUMARGS} register by $1$ to account for the

1932: disappearance of an argument. The final possibility for the top of the

1933: {\it SL} stack is that it is a reference to an atomic term, \ie, one

1934: that is a constant or a bound or free variable. This situation signals

1935: that a head normal form has been found and hence terminates the

1936: overall process. 

1937: 

1938: To understand the integration of the head normalization procedure 

1939: into the larger computational framework, suppose that it is invoked

1940: with a term that can be reduced to the form $\lambdax {x_1}

1941: \ldots \lambdax {x_n} (h \app t_1 \app \ldots \app t_m)$, where $h$ is

1942: a constant or variable. When the procedure is finished, the {\it SL}

1943: stack will contain, in consecutive locations from the top, references

1944: to the de Bruijn representation of $h$ and the 

1945: suspension representations of terms $s_1, \ldots, s_m$ that are

1946: $\beta$-convertible to $t_1, \ldots, t_m$. This kind of access to the

1947: body of the term is particularly convenient for the other operations

1948: required within unification. First of all, the heads of terms and

1949: their status, whether rigid or flexible, is easily

1950: determined. Further, assume that the simplification operation is to be

1951: applied to two terms $t$ and $r$ whose head normal forms have 

1952: identical binders. The head normalization procedure can, in this case,

1953: be invoked to lay out the bodies of these two terms in different

1954: segments of the {\it SL} stack. Then, if the two terms are rigid and have

1955: identical heads, the terms out of which new disagreement pairs have to

1956: be formed appear at the same displacement from different starting

1957: locations, thereby facilitating an iterative structure to further

1958: processing. The availability of the arguments of the head normalized

1959: term in contiguous locations turns out also to be important to the

1960: compilation model that we discuss in Section \ref{sec:abstmachine}.

1961: 

1962: Our description  of the term simplification process above assumes that

1963: the lengths of binders of the two terms to be unified are identical. This

1964: situation may actually not hold automatically  

1965: but, rather, may have to be achieved at the required points in

1966: computation by using the $\eta$-conversion rule. 

1967: A few simple changes to our normalization routine suffices for making

1968: the requisite adjustments. Thus, suppose that we are comparing

1969: two terms that have as head normal forms $\lambdax {x_1} \ldots

1970: \lambdax {x_n} (c\app t_1\app \ldots \app t_l)$ and $\lambdax {x_1}

1971: \ldots \lambdax {x_m} (c'\app s_1\app \ldots \app s_k)$. Our

1972: procedure can easily record the values of $m$ and $n$ when producing

1973: these forms. Now suppose that $n$ is greater than $m$ and that $c'$ is

1974: identical to one of $x_1,\ldots,x_m$. Then the effect of adjusting the

1975: binder length of the second term to $n$ on its head in a suspension

1976: representation of the terms can be captured simply by adding $n-m$ to

1977: the index value corresponding to $c'$. The changes to the first $k$

1978: arguments of this term under such an adjustment are also

1979: straightforward to capture: if $s'_i$ is the term in suspension 

1980: notation corresponding to $s_i$, the desired adjustment is

1981: encapsulated in the term $\env{s'_i,0,j,{\it nil}}$ where $j =

1982: n-k$. Finally, new arguments need to be added to the term, but this is

1983: particularly easy to do on-the-fly, they being just the de Bruijn

1984: indices $\#(n-m), \ldots, \#1$. 

1985: 

1986: The normalization process requires the creation of new structures for

1987: terms at various points in its execution. These terms are best

1988: allocated on the heap in a WAM-like model and this is, in fact, what

1989: is done within the {\it Teyjus} implementation. 

1990: 

1991: \subsection{Explicit Representation of Disagreement Sets}\label{ssec:disset}

1992: 

1993: Disagreement sets arise in principle even in the context of

1994: first-order unification. However, typical implementations of this

1995: operation avoid the explicit treatment of such sets by utilizing a 

1996: recursive, depth-first processing of the subparts of the two terms

1997: that are to be unified. Careful attention to the order in which

1998: subterms are processed is known to make a substantial difference to

1999: the worst case behaviour \cite{MM82}, but the `pathological' cases

2000: seldom seem to arise in practice. Given this, flexibility in choosing

2001: the next pair of (sub)terms is usually sacrificed for a simpler

2002: processing structure.

2003: 

2004: Two properties of first-order unification are actually critical to

2005: adopting the approach that treats disagreement sets implicitly: its

2006: decidability and the existence of most general unifiers. Neither of

2007: these properties carry over to the higher-order context. While it is

2008: still possible to use a recursive process that explores unifiers for

2009: subterms in a depth-first fashion, basing the unification computation

2010: entirely on such an approach appears pragmatically undesirable. In

2011: particular, in a situation where choices have to be made in

2012: substitutions, it appears best to bring all available constraints to

2013: bear on making them. Thus, suppose that it is necessary to

2014: unify two terms of the form $(f \app t_1 \app \ldots \app t_n)$ and

2015: $(f\app s_1 \app \ldots \app s_n)$, where $f$ is a constant (function)

2016: symbol and, for $1 \leq i \leq n$, $t_i$ and $s_i$ are arbitrary

2017: terms. We may well attempt to do this by unifying the pairs $\langle

2018: t_1,s_1\rangle,\ldots,\langle t_n,s_n \rangle$ in sequence. Now, in

2019: the course of unifying the pair $\langle t_1, s_1

2020: \rangle$, it may be necessary to pick one of several substitutions for

2021: a variable $x$. This variable may appear in other pairs of subterms as

2022: well and some of the substitution choices for $x$ may render these

2023: pairs non-unifiable. Using this information, at the very least,

2024: curtails the search. In particular cases, this may even 

2025: make a difference between finding and not finding a unifier: some

2026: choices of substitution for $x$ that are ruled out by their effects on

2027: other pairs may lead to a unending search when the pair $\langle

2028: t_1, s_1 \rangle$ is considered in isolation. 

2029: 

2030: A better approach to finding unifiers for a disagreement set, then,

2031: appears to be the following. At any point in the computation, we

2032: select a pair from the set and proceed to search for a unifier for

2033: only this pair till such time that more than one possibility needs to

2034: be explored. At such a point, we pick a

2035: possible substitution and examine its effect on the rest of the

2036: disagreement set before proceeding further. Implementing this approach

2037: clearly requires an explicit representation and manipulation of

2038: disagreement sets within the unification process. Actually, 

2039: such disagreement sets may even have to be carried {\it across} invocations

2040: to unification: repeated applications of the unification step

2041: described in Section \ref{sec:interp} may reduce a disagreement set to

2042: a form in which, while being nonempty, it contains only

2043: flexible-flexible pairs and, as we have noted already, it is best to

2044: suspend the processing of such a set till further constraints are

2045: imposed on it through backchaining steps. 

2046: 

2047: Given that we need to maintain disagreement sets explicitly, an

2048: important question becomes that of the structure their representation

2049: should take. The following considerations are relevant to this issue:

2050: 

2051: \begin{enumerate}

2052: 

2053: \item These sets evolve incrementally during computation. In

2054: particular, changes result from adding new pairs to an existing set or

2055: by effecting substitutions that modify only some pairs leaving the

2056: others unchanged. Thus, a scheme that allows the representation of a

2057: new disagreement set to reuse that of unchanged portions

2058: of the set from  which it arises might be the preferred one in

2059: practice. 

2060: 

2061: \item For efficiency in backtracking, it should be possible to rapidly 

2062: recreate disagreement sets that were in existence earlier. This

2063: becomes a pertinent issue if the kind of sharing described in (1) is

2064: realized through destructive changes. 

2065: 

2066: \end{enumerate}

2067: 

2068: A representation for disagreement sets that suffices for meeting the

2069: above requirements is one based on doubly linked lists the elements

2070: of which are pairs of pointers to the terms constituting the

2071: pairs in the set. Given that these sets arise in the

2072: course of backchaining or clause invocation and finally disappear in

2073: the event of backtracking, the lists representing them are naturally

2074: allocated in the heap in a WAM-like setting.  The need to examine

2075: disagreement sets during computation requires that the beginning of

2076: the lists representing them be recorded in machine states. A special

2077: register that we refer to as the live list or {\it LL} register and

2078: that contains a reference to the first element in the list at

2079: each execution point can serve this purpose. Now, there are

2080: two ways in which a disagreement set might change during

2081: computation. First, term simplification may require some element of

2082: the set to be removed and new pairs corresponding to subterms that

2083: need to be unified to be added to the set. The removal of a pair is

2084: realized in this setting by changing the `after' and `before' pointers

2085: of the elements on either side of it in the list representation. A

2086: subsequent re-inclusion of the removed pair into the set

2087: can be effected easily if a reference to it is maintained,

2088: something that can be done through a (properly annotated) entry in the 

2089: trail stack. The addition of new pairs is also simple: entries for

2090: these can be created on the heap and added to the beginning of the

2091: live list. The second way in which a disagreement set may change is

2092: through a backtracking operation. To support this action, it is

2093: necessary also to store the contents of the {\it LL} register in

2094: choice points at the time of their creation. The relevant disagreement

2095: set can then be resurrected by utilizing information in the trail

2096: stack to restore deleted pairs and using the old value of the {\it LL}

2097: register to remove the pairs added beyond the point being backtracked

2098: to. 

2099: 

2100: It is in principle possible to perform all the processing within the

2101: term simplification phase of unification using only the heap and the

2102: live list. However, judiciousness should be exercised in utilizing

2103: the heap since space allocated in it is reclaimed only through

2104: backtracking. With this in mind, we  

2105: observe that when a rigid-rigid pair is encountered during term

2106: simplification, the processing can be applied recursively to the

2107: subterms and additions to the heap and the live list need not take

2108: place till a flexible-flexible or a flexible-rigid pair is

2109: encountered. As a specific example consider the following query

2110: involving the {\it mapfun} predicate from Example~\ref{ex:mapfun}: 

2111: \begin{tabbing}

2112: \qquad\=\kill

2113: \>${\it mapfun}\app (a :: b :: {\it nil}) \app G \app (g\app a\app a) ::

2114: (g\app a\app b) :: {\it nil})$

2115: \end{tabbing}

2116: \noindent Using the idea just described, when applying a backchaining

2117: step to this query relative to the second clause for {\it mapfun}, the

2118: addition to the heap of only the pairs in the set

2119: \begin{tabbing}

2120: \qquad\=\kill

2121: \>$\{\langle X, a \rangle, \langle L1, b::{\it nil} \rangle, \langle F, G \rangle,

2122: \langle (F\app X), (g\app a \app a) \rangle, \langle L2, (g\app a \app b)::{\it nil}

2123: \rangle\}$

2124: \end{tabbing}

2125: \noindent need be considered. When one of the terms in a disagreement pair

2126: is known statically, this kind of processing can be realized through

2127: special instructions and a compilation process similar to that used in

2128: the first-order case, and we discuss this matter in greater detail in

2129: the next section. However, the two rigid terms in a pair can sometimes

2130: arise dynamically and term simplification has in this case to be

2131: carried out in `interpretive' mode. In the context of a virtual

2132: machine based implementation, a special pushdown list in combination

2133: with an iterative code fragment can be used to realize this

2134: computation. 

2135: 

2136: There are certain forms of disagreement pairs for which most general

2137: unifiers can be immediately identified. An example of this kind

2138: arises from first-order unification: given a pair of the form 

2139: $\langle X, t \rangle$ where $X$ is a variable of atomic type and $t$

2140: is a term in which $X$ does not appear, all unifiers for the pair must

2141: be instances of the unifier that substitutes $t$ for $X$.

2142: Alternatively, if $X$ does occur in $t$, failure in unification can be

2143: registered immediately. This observation can be generalized to the 

2144: higher-order context. Given a pair of the form $\langle

2145: \lambdax {x_1} \ldots \lambdax {x_n} X, \lambdax {x_1} \ldots \lambdax

2146: {x_n} t \rangle$, where $X$ has an arbitrary type, $X$ can be bound to

2147: $t$ and this pair can be removed from the set provided neither $X$ nor

2148: the variables in $\{x_1,\ldots x_n\}$ appear in $t$; interestingly, the

2149: verification of the proviso is simplified by the use of the de Bruijn

2150: notation. The occurrence of $X$ (or of the other variables) in $t$ on

2151: the other hand does not by itself signal failure in the higher-order

2152: case. However, the `occurs-check' from the first-order case can be

2153: generalized to a `rigid path check' 

2154: that detects the impossibility of unification in some cases and that

2155: simplifies the search for unifiers in other cases by binding $X$ to a

2156: term that represents an initial `section' of $t$ and by adding pairs to

2157: the disagreement set to represent the remaining constraints on

2158: unifiers. Some flexible-flexible pairs, such as $\langle F, G \rangle$

2159: in the example above, can also be solved by this process. Using

2160: observations such as these reduces the need to consider 

2161: the general imitation and projection substitutions and hence also the

2162: attendant bookkeeping steps. In the case of the ${\it mapfun}$ query, the

2163: disagreement set can, in fact, be quickly reduced to $\{\langle (F\app a),

2164: (g\app a\app a) \rangle \}$ by these means. Significantly, first-order

2165: unification can be solved immediately using these observations.

2166: Empirical studies indicate that a large number of 

2167: the unification problems that arise even in the higher-order context

2168: fall into this category \cite{MP92}, suggesting the general importance 

2169: of incorporating these observations into an

2170: implementation.\footnote{The applicability of this first-order like

2171: processing in the higher-order case is dependent on variables being

2172: preserved in an `$\eta$-reduced' form through the compilation

2173: process. The procedure described in \cite{DHKP98} for unification

2174: of what are known as higher-order patterns \cite{miller91jlc}

2175: gives up this property. This is a surprising choice, especially since

2176: it is not dictated by the theory: under it, even the

2177: pair $\langle F, G\rangle$ gets converted into a form that

2178: requires an `inverting' substitution to be computed. The only possible

2179: benefit for this is that variables need never be dynamically

2180: `$\eta$-expanded.' However, this is {\it rarely}, perhaps {\it never},

2181: required in practice. The direct use of explicit 

2182: substitutions also does not seem to have the practical benefits in this

2183: subcase that it has for full higher-order unification \cite{DHK00},

2184: and it possibly has some drawbacks. We are attempting to quantify

2185: these remarks in ongoing research.}

2186: 

2187: The appropriate time to consider such substitutions is during 

2188: the term simplification phase. Doing this and also being

2189: conservative in the additions to the heap now calls for the use of two

2190: pushdown lists. The general scheme works as follows. The

2191: simplification of a disagreement set 

2192: proceeds as before with the use of the first pushdown list, except

2193: that the process may now also involve making bindings to variables.

2194: When the process `bottoms out' with a flexible-flexible or

2195: flexible-rigid pair, this is pushed onto the top of the second

2196: pushdown list instead of the heap. When all the pairs in the

2197: original disagreement set have been simplified, it is checked whether

2198: any bindings were made in the course of simplification. If no bindings

2199: were made, the pairs in the second pushdown list are transferred to

2200: the heap and included in the live list. If, on the other hand, any

2201: bindings were made, the simplification process is repeated with the

2202: disagreement set being given now by the live list and the pairs in the

2203: second pushdown list and the roles of the two pushdown lists

2204: being reversed. 

2205: 

2206: \subsection {Recording Branch Points in Unification}

2207: 

2208: A depth-first approach to exploring alternatives in unification 

2209: requires that information be recorded at branch points that

2210: is sufficient for recreating state and for determining the remaining

2211: possibilities upon backtracking. The state information can actually be

2212: factored into two conceptual kinds: that which pertains to clause

2213: usage in the backchaining model of computation and that which 

2214: relates to the unification problem, such as the disagreement set and

2215: the pair of flexible and rigid terms that are under consideration at a

2216: particular juncture. Now, the approach that we have proposed is one

2217: that solves unification problems to the extent possible before

2218: contemplating further backchaining steps. Under this strategy,  

2219: in situations where genuine higher-order unification is involved, a

2220: sequence of branch points are likely to be generated for which the

2221: state insofar as it pertains to clause usage is identical. Thus, if

2222: this information is represented separately from the rest of the

2223: backtracking data, it becomes possible to share it across more than

2224: one branch point. 

2225: 

2226: In light of the above observations, we propose to record

2227: information relevant to branching in unification in two layers that we 

2228: refer to, respectively, as the shared part and the variable

2229: part. Assuming a WAM style 

2230: compilation model, the most appropriate juncture at which to consider

2231: genuine higher-order unification is right after a compiled form of

2232: term simplification akin 

2233: to first-order unification has been carried out relative to the head

2234: of the clause and before an attempt is made to solve the clause

2235: body. At this stage, if the {\it LL} register indicates a nonempty

2236: disagreement set, the first action would be to create the shared part

2237: of the unification branch point records that stores clause usage

2238: information. More specifically, this part would record at least the

2239: following state data: 

2240: \begin{itemize}

2241: \item The program pointer that determines the instruction to be

2242: executed upon successful completion of this phase of unification.

2243: 

2244: \item A pointer to the most recent environment record.

2245: 

2246: \item The continuation pointer; this is relevant in the case of

2247: clauses with an atomic body for which an environment record does not

2248: exist containing this information. 

2249: 

2250: \item Argument registers that need to be preserved for use in the

2251: first goal in the clause body.

2252: \end{itemize}

2253: Additional information may have to be recorded in this part depending 

2254: on auxiliary language features. For example, in a framework that

2255: permits the use of the {\it cut} control primitive, the contents of

2256: the cut point register that indicates the backtracking point up to

2257: which to eliminate choices needs to be stored as well. Similarly,

2258: it has been found useful to give the programmer dynamic control over

2259: whether projection or imitation substitutions are to be tried first

2260: within higher-order unification. In this situation, the regimen in

2261: effect at this instance should also be stored in the shared part for

2262: later restoration. 

2263: 

2264: Once the shared part has been constructed, a global reference to

2265: it is maintained in a special register that we refer to as the {\it

2266: BRS} register. Computation now 

2267: proceeds to simplifying the disagreement set and, eventually, to

2268: picking a flexible-rigid pair whose imitation and projection

2269: substitutions have to be examined. After such a pair has been determined

2270: and a substitution for it has been selected, information must be left

2271: behind for examining the remaining alternatives in case of 

2272: backtracking. This data is encoded in the variable part of unification

2273: branch point records that comprises the following components:

2274: \begin{itemize}

2275: \item The heads of the flexible and rigid terms together with their

2276: types.

2277: 

2278: \item Information determining what substitutions remain to be tried. A

2279: simple way to encode this is by remembering the number of projection

2280: substitutions already tried; the additional knowledge of whether

2281: imitation or projection substitutions are being tried first completely

2282: determines the alternatives left. 

2283: 

2284: \item The contents of the {\it LL} register that will be used in

2285: consort with the information in the trail stack to restore the

2286: disagreement set on backtracking.\footnote{This component needs also

2287: to be added to the usual {\it choice point record} of the WAM that

2288: stores information for backtracking over clause choices.}

2289: 

2290: \item Pointers to the top of the heap and the trail stack that

2291: determine the status of these data areas. 

2292: 

2293: \item The contents of the {\it BRS} register for restoring clause

2294: context on backtracking.

2295: 

2296: \item A pointer to a record of the preceding branch point in

2297: computation, to be used when all alternatives at this stage have been

2298: exhausted. 

2299: \end{itemize}

2300: Although the heads of the flexible and rigid terms suffice for generating

2301: all the substitutions, certain operations have to be repeated on these

2302: in each case. Thus, the binder of every substitution that is

2303: constructed is identical. Similarly, the vector of arguments of the

2304: general arguments of the substitution terms are identical both within

2305: a single substitution and across the imitation and

2306: projections. Finally, the target 

2307: type of the flexible head is used repeatedly in determining the

2308: appropriateness of each projection substitution. Assuming the

2309: acceptability of trading off space for time, these components may be

2310: computed once when the variable part is set up and references to them

2311: may be saved for later use. This is, in fact, the course adopted within the

2312: {\it Teyjus} implementation.  

2313: 

2314: The successful selection of a substitution within the unification

2315: process is followed by another term simplification phase. If there is

2316: another flexible-rigid pair in the resulting disagreement set, further

2317: substitutions must be posited, leading to the setting up of the

2318: variable part of another unification branch point record. Note that

2319: the shared part of this record, pointed to by the {\it BRS} register,

2320: is the same as that for the previous such record. This process

2321: continues till eventually a failure is encountered or the disagreement

2322: set is reduced to a solved form. In the latter case, computation

2323: continues with an attempt to solve the next (predicate) goal through a

2324: backchaining process.

2325: 

2326: There is, of course, the possibility

2327: of failure along the path currently being explored. In this case 

2328: backtracking must take place to the most recent choice point either in

2329: clause selection or in unification. In order to determine the

2330: appropriate such point, the records corresponding to them are 

2331: chained into one linear sequence based on their age and a pointer to

2332: the most recent one is placed, as in the WAM, in the {\it B} or

2333: backtrack register. Now, certain actions, such as the unwinding of the 

2334: trail stack, the resetting of the disagreement set and recovery of

2335: heap space, are identical regardless of whether computation returns

2336: to trying another clause or another unifier and can be carried out

2337: uniformly with a little coordination in the structures of the records

2338: corresponding to these different kinds of backtrack points. However,

2339: other actions, such as the generation of another substitution or the 

2340: selection of another clause, do need a knowledge of the kind of

2341: choice being reconsidered. One approach to providing this

2342: information would be to mark each backtrack point record in a special

2343: way at the time of its creation. A more elegant solution is

2344: possible in a virtual machine and compilation based framework and is,

2345: in fact, used in {\it Teyjus}. In this system, a special

2346: instruction is included in the instruction set whose purpose is to

2347: utilize the information in the variable part of a unification

2348: branch point record to generate a new substitution, to reset the {\it

2349: BRS} register and the state reflecting clause usage context and to

2350: continue with the unification computation. The right backtracking

2351: action can now be achieved simply by storing a pointer to a program

2352: location containing this instruction in a field of the variable part

2353: of a unification branch point record that is coordinated with the next 

2354: clause field of the usual choice point record of the WAM; a uniform

2355: transfer of control to the stored program point and the execution of

2356: the corresponding instruction then achieves the appropriate

2357: backtracking action.  

2358: 

2359: Branching in computation is obviously costly both in time and in

2360: space and every effort should be expended to exploit deterministic

2361: execution patterns whenever possible. One approach to doing this

2362: within the unification computation is, as we have already mentioned,

2363: to build a treatment of more special cases in which most general

2364: unifiers exist into the term simplification process. Another useful

2365: idea is to employ quick dynamic tests to determine that no further

2366: substitutions exist in certain cases and to discard unification

2367: backtrack points eagerly on this basis. Some heuristics of this kind

2368: are embedded in the {\it Teyjus} system but this is a matter that

2369: deserves further attention.

2370: 

2371: A final point to mention concerns the allocation of space for the

2372: terms generated for projection and imitation substitutions. 

2373: This is best done on the heap since backtracking permits the

2374: space to be reclaimed when the substitution itself becomes redundant. 

2375: 

2376: \section{An Abstract Machine and Compilation Model}\label{sec:abstmachine}

2377: 

2378: The abstract machine for Prolog is designed to support a compiled

2379: treatment of the four main components of the underlying model of

2380: computation: the processing of the structure of complex, usually

2381: conjunctive, goals, the setting up of the arguments of atomic goals,

2382: the sequencing through clause choices for such goals and the

2383: unification of the arguments of these goals with the statically known

2384: arguments of a clause head.  A further aspect that receives special

2385: attention is the detection of determinism. Nondeterminism is costly to

2386: deal with and the need to do so can often be eliminated by utilizing

2387: the structure of the actual arguments of atomic goals to prune choices

2388: early during execution. This observation is exploited in practice by

2389: including a special set of instructions that allow clause choices to

2390: be indexed by the arguments and by building the use of these

2391: instructions  into the compilation process.

2392: 

2393: The basic issues in a first-order context persist also in our

2394: higher-order language. Much of the machinery and even the instruction

2395: set that are embedded in a WAM-like architecture for treating these

2396: aspects can, in fact, be carried over to the implementation task at

2397: hand. However, some new devices are needed, primarily for dealing with

2398: a richer structure for terms and a more complex unification

2399: operation. Moreover, there must be differences in the interpretation

2400: of some instructions. Instructions that examine the structure of terms

2401: must, for instance, have the ability to head normalize these terms if

2402: this is needed during execution. Further, the instructions that

2403: realize unification completely in a first-order setting suffice only

2404: to implement the initial term simplification phase of higher-order

2405: unification. The capability to leave unification problems that cannot

2406: be solved in this manner to a later, interpretive phase should

2407: therefore be built into these instructions. Such a `deferring' action

2408: should, of course, be complemented by an invocation of the remaining 

2409: higher-order unification process at a suitably chosen point.

2410: 

2411: We present, in this section, an extended version of the WAM that

2412: develops on these ideas. We summarize first the modifications to

2413: the machine structure that were implicit in our discussion of

2414: the treatment of higher-order unification. We then describe changes to

2415: the instruction set. The last part of this section illustrates the

2416: compilation model by presenting the code generated for some simple

2417: higher-order programs. A familiarity with the original abstract

2418: machine of Warren, such as might be obtained from \cite{HAK91} or

2419: \cite{War83}, is assumed in this exposition. 

2420: 

2421: 

2422: \subsection{The Structure of the Extended Machine}\label{ssec:wam}

2423: 

2424: Figure~\ref{fig:wamstate} depicts the various data areas and registers

2425: present in the extended abstract machine and provides a snapshot of a

2426: machine state during computation. The code area, the heap, the local

2427: stack and the trail of the WAM persist in this machine. The new data

2428: areas are the {\it SL} stack, the applications stack and the two

2429: pushdown lists. The first two components are utilized by the

2430: head normalization code as described in Section~\ref{sec:runtime}. The

2431: pushdown lists are used in simplifying disagreement sets and help, as

2432: we have seen, in conserving heap space. We observe that only

2433: one of these pushdown lists is really new: one pushdown list is

2434: usually employed by WAM implementations for realizing the part of

2435: first-order unification that must be performed in interpretive

2436: mode.

2437: 

2438: 

2439: \begin{figure}

2440: \begin{center}

2441: \setlength{\unitlength}{0.00083333in}

2442: %

2443: \begingroup\makeatletter\ifx\SetFigFont\undefined%

2444: \gdef\SetFigFont#1#2#3#4#5{%

2445:   \reset@font\fontsize{#1}{#2pt}%

2446:   \fontfamily{#3}\fontseries{#4}\fontshape{#5}%

2447:   \selectfont}%

2448: \fi\endgroup%

2449: {\renewcommand{\dashlinestretch}{30}

2450: \begin{picture}(5877,8787)(0,-10)

2451: \path(12,5862)(1512,5862)

2452: \path(762,5862)(762,5487)

2453: \blacken\path(732.000,5607.000)(762.000,5487.000)(792.000,5607.000)(762.000,5571.000)(732.000,5607.000)

2454: \path(1887,6612)(1512,6612)

2455: \blacken\path(1632.000,6642.000)(1512.000,6612.000)(1632.000,6582.000)(1596.000,6612.000)(1632.000,6642.000)

2456: \path(12,5562)(12,6837)(1512,6837)(1512,5562)

2457: \path(1887,6237)(1512,6237)

2458: \blacken\path(1632.000,6267.000)(1512.000,6237.000)(1632.000,6207.000)(1596.000,6237.000)(1632.000,6267.000)

2459: \path(1887,5862)(1512,5862)

2460: \blacken\path(1632.000,5892.000)(1512.000,5862.000)(1632.000,5832.000)(1596.000,5862.000)(1632.000,5892.000)

2461: \put(2037,6537){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}LL}}}}}

2462: \put(2037,6162){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}HB}}}}}

2463: \put(2037,5787){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}H}}}}}

2464: \put(462,6987){\makebox(0,0)[lb]{\smash{{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Heap}}}}}

2465: \put(162,312){\makebox(0,0)[lb]{\smash{{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Applications}}}}}

2466: \put(162,87){\makebox(0,0)[lb]{\smash{{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Stack}}}}}

2467: \path(12,612)(12,2937)(1512,2937)

2468: 	(1512,612)(12,612)

2469: \path(12,2187)(1512,2187)

2470: \path(12,1212)(1512,1212)

2471: \path(762,2187)(762,1812)

2472: \blacken\path(732.000,1932.000)(762.000,1812.000)(792.000,1932.000)(762.000,1896.000)(732.000,1932.000)

2473: \path(762,1212)(762,1587)

2474: \blacken\path(792.000,1467.000)(762.000,1587.000)(732.000,1467.000)(762.000,1503.000)(792.000,1467.000)

2475: \path(1887,2487)(1512,2487)

2476: \blacken\path(1632.000,2517.000)(1512.000,2487.000)(1632.000,2457.000)(1596.000,2487.000)(1632.000,2517.000)

2477: \path(1887,2187)(1512,2187)

2478: \blacken\path(1632.000,2217.000)(1512.000,2187.000)(1632.000,2157.000)(1596.000,2187.000)(1632.000,2217.000)

2479: \put(2037,2412){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}S}}}}}

2480: \put(2037,2112){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}SL}}}}}

2481: \put(312,3087){\makebox(0,0)[lb]{\smash{{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}SL Stack}}}}}

2482: \path(12,3762)(12,4887)(1512,4887)(1512,3762)

2483: \path(12,4062)(1512,4062)

2484: \path(762,4062)(762,3687)

2485: \blacken\path(732.000,3807.000)(762.000,3687.000)(792.000,3807.000)(762.000,3771.000)(732.000,3807.000)

2486: \path(1887,4062)(1512,4062)

2487: \blacken\path(1632.000,4092.000)(1512.000,4062.000)(1632.000,4032.000)(1596.000,4062.000)(1632.000,4092.000)

2488: \put(2037,3987){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}TR}}}}}

2489: \put(537,5037){\makebox(0,0)[lb]{\smash{{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Trail}}}}}

2490: \path(3012,12)(3012,3237)(4812,3237)(4812,12)

2491: \path(3012,2862)(4812,2862)

2492: \path(3012,2562)(4812,2562)

2493: \path(3012,2187)(4812,2187)

2494: \path(5187,1887)(4812,1887)

2495: \blacken\path(4932.000,1917.000)(4812.000,1887.000)(4932.000,1857.000)(4896.000,1887.000)(4932.000,1917.000)

2496: \path(3012,1887)(4812,1887)

2497: \dashline{60.000}(4812,687)(5112,687)(5112,912)(4812,912)

2498: \blacken\path(4932.000,942.000)(4812.000,912.000)(4932.000,882.000)(4896.000,912.000)(4932.000,942.000)

2499: \dashline{60.000}(4812,987)(5112,987)(5112,1212)(4812,1212)

2500: \blacken\path(4932.000,1242.000)(4812.000,1212.000)(4932.000,1182.000)(4896.000,1212.000)(4932.000,1242.000)

2501: \path(3012,1737)(4812,1737)

2502: \path(3012,1137)(4812,1137)

2503: \path(3012,837)(4812,837)

2504: \path(3012,612)(2487,612)(2487,1662)(3012,1662)

2505: \blacken\path(2892.000,1632.000)(3012.000,1662.000)(2892.000,1692.000)(2928.000,1662.000)(2892.000,1632.000)

2506: \path(3012,912)(2637,912)(2637,1587)(3012,1587)

2507: \blacken\path(2892.000,1557.000)(3012.000,1587.000)(2892.000,1617.000)(2928.000,1587.000)(2892.000,1557.000)

2508: \path(3012,1212)(2787,1212)(2787,1512)(3012,1512)

2509: \blacken\path(2892.000,1482.000)(3012.000,1512.000)(2892.000,1542.000)(2928.000,1512.000)(2892.000,1482.000)

2510: \dashline{60.000}(4812,1287)(5862,1287)(5862,2712)(4812,2712)

2511: \blacken\path(4932.000,2742.000)(4812.000,2712.000)(4932.000,2682.000)(4896.000,2712.000)(4932.000,2742.000)

2512: \path(5187,1587)(4812,1587)

2513: \blacken\path(4932.000,1617.000)(4812.000,1587.000)(4932.000,1557.000)(4896.000,1587.000)(4932.000,1617.000)

2514: \path(3012,537)(4812,537)

2515: \path(2937,1437)(4737,1437)

2516: \path(3837,537)(3837,162)

2517: \blacken\path(3807.000,282.000)(3837.000,162.000)(3867.000,282.000)(3837.000,246.000)(3807.000,282.000)

2518: \put(3387,2637){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}Choice Point}}}}}

2519: \put(3087,1962){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}Environment Record}}}}}

2520: \put(5262,1812){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}E}}}}}

2521: \put(5262,1512){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}BRS}}}}}

2522: \put(5262,537){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}B}}}}}

2523: \put(3087,912){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}Branch Pt. (Variable)}}}}}

2524: \put(3237,3387){\makebox(0,0)[lb]{\smash{{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Local Stack}}}}}

2525: \path(5187,612)(4812,612)

2526: \blacken\path(4932.000,642.000)(4812.000,612.000)(4932.000,582.000)(4896.000,612.000)(4932.000,642.000)

2527: \drawline(3162,1212)(3162,1212)

2528: \put(3087,1212){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}Branch Pt. (Variable)}}}}}

2529: \put(3087,612){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}Branch Pt. (Variable)}}}}}

2530: \put(3012,1512){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}Branch Point (Shared)}}}}}

2531: \path(4737,8337)(4738,8338)(4744,8344)

2532: 	(4756,8355)(4770,8368)(4783,8379)

2533: 	(4794,8388)(4803,8395)(4812,8399)

2534: 	(4819,8403)(4826,8405)(4834,8407)

2535: 	(4841,8408)(4850,8409)(4858,8408)

2536: 	(4865,8407)(4873,8405)(4880,8403)

2537: 	(4887,8399)(4894,8396)(4901,8391)

2538: 	(4908,8385)(4916,8378)(4923,8369)

2539: 	(4930,8360)(4936,8349)(4941,8337)

2540: 	(4946,8325)(4950,8312)(4952,8300)

2541: 	(4954,8287)(4957,8273)(4958,8257)

2542: 	(4960,8241)(4962,8224)(4964,8208)

2543: 	(4966,8192)(4967,8176)(4970,8162)

2544: 	(4972,8149)(4975,8137)(4978,8124)

2545: 	(4983,8111)(4988,8100)(4994,8088)

2546: 	(5000,8078)(5005,8068)(5011,8059)

2547: 	(5016,8051)(5021,8044)(5025,8037)

2548: 	(5028,8030)(5030,8023)(5032,8015)

2549: 	(5033,8008)(5034,7999)(5033,7991)

2550: 	(5032,7984)(5030,7976)(5028,7969)

2551: 	(5025,7962)(5021,7955)(5016,7948)

2552: 	(5011,7940)(5005,7931)(4999,7921)

2553: 	(4994,7911)(4988,7899)(4983,7888)

2554: 	(4978,7875)(4975,7862)(4972,7850)

2555: 	(4970,7837)(4967,7823)(4966,7807)

2556: 	(4964,7791)(4962,7774)(4960,7758)

2557: 	(4958,7742)(4957,7726)(4954,7712)

2558: 	(4952,7699)(4950,7687)(4946,7674)

2559: 	(4941,7662)(4936,7650)(4930,7639)

2560: 	(4923,7630)(4916,7621)(4908,7614)

2561: 	(4901,7608)(4894,7603)(4887,7599)

2562: 	(4880,7596)(4873,7594)(4865,7592)

2563: 	(4858,7591)(4849,7590)(4841,7591)

2564: 	(4834,7592)(4826,7594)(4819,7596)

2565: 	(4812,7599)(4803,7604)(4794,7611)

2566: 	(4783,7620)(4770,7631)(4756,7644)

2567: 	(4744,7655)(4738,7661)(4737,7662)

2568: \put(3087,7737){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}S, HB, A1, ..., An}}}}}

2569: \put(3087,8037){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}P, CP, E, H, B, TR,}}}}}

2570: \put(5262,8112){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}From the }}}}}

2571: \put(5262,7887){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}WAM}}}}}

2572: \path(4737,7362)(4737,7363)(4739,7366)

2573: 	(4743,7373)(4748,7383)(4756,7395)

2574: 	(4764,7407)(4774,7418)(4785,7428)

2575: 	(4797,7434)(4812,7437)(4822,7436)

2576: 	(4832,7433)(4839,7430)(4845,7426)

2577: 	(4850,7423)(4853,7421)(4856,7418)

2578: 	(4858,7415)(4861,7412)(4865,7406)

2579: 	(4870,7399)(4875,7390)(4881,7377)

2580: 	(4887,7362)(4892,7343)(4895,7326)

2581: 	(4895,7312)(4893,7301)(4890,7293)

2582: 	(4887,7287)(4884,7281)(4881,7273)

2583: 	(4879,7262)(4879,7248)(4882,7231)

2584: 	(4887,7212)(4896,7192)(4905,7178)

2585: 	(4914,7171)(4923,7168)(4931,7168)

2586: 	(4939,7168)(4946,7167)(4954,7161)

2587: 	(4959,7151)(4962,7137)(4959,7123)

2588: 	(4954,7113)(4946,7107)(4939,7106)

2589: 	(4931,7106)(4923,7106)(4914,7103)

2590: 	(4905,7096)(4896,7082)(4887,7062)

2591: 	(4882,7043)(4879,7026)(4879,7012)

2592: 	(4881,7001)(4884,6993)(4887,6987)

2593: 	(4890,6981)(4893,6973)(4895,6962)

2594: 	(4895,6948)(4892,6931)(4887,6912)

2595: 	(4881,6897)(4875,6884)(4870,6875)

2596: 	(4865,6868)(4861,6862)(4858,6859)

2597: 	(4856,6856)(4853,6853)(4850,6851)

2598: 	(4845,6848)(4839,6844)(4832,6841)

2599: 	(4822,6838)(4812,6837)(4797,6840)

2600: 	(4785,6846)(4774,6856)(4764,6867)

2601: 	(4756,6879)(4748,6891)(4743,6901)

2602: 	(4739,6908)(4737,6911)(4737,6912)

2603: \put(3087,7212){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}LL, SL, BRS,}}}}}

2604: \put(3087,6912){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}NUMARGS}}}}}

2605: \put(5262,7137){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}New}}}}}

2606: \put(3312,8412){\makebox(0,0)[lb]{\smash{{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Registers}}}}}

2607: \path(12,8487)(1512,8487)(1512,7437)

2608: 	(12,7437)(12,8487)

2609: \path(1887,8187)(1512,8187)

2610: \blacken\path(1632.000,8217.000)(1512.000,8187.000)(1632.000,8157.000)(1596.000,8187.000)(1632.000,8217.000)

2611: \path(1887,7812)(1512,7812)

2612: \blacken\path(1632.000,7842.000)(1512.000,7812.000)(1632.000,7782.000)(1596.000,7812.000)(1632.000,7842.000)

2613: \path(3912,4662)(3912,5037)

2614: \blacken\path(3942.000,4917.000)(3912.000,5037.000)(3882.000,4917.000)(3912.000,4953.000)(3942.000,4917.000)

2615: \path(3912,5787)(3912,5412)

2616: \blacken\path(3882.000,5532.000)(3912.000,5412.000)(3942.000,5532.000)(3912.000,5496.000)(3882.000,5532.000)

2617: \put(237,8637){\makebox(0,0)[lb]{\smash{{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Code Area}}}}}

2618: \put(2037,8112){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}P}}}}}

2619: \put(2037,7737){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}CP}}}}}

2620: \put(3387,3987){\makebox(0,0)[lb]{\smash{{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Second PDL}}}}}

2621: \put(3462,6237){\makebox(0,0)[lb]{\smash{{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}First PDL}}}}}

2622: \path(3387,5037)(3387,4212)(4512,4212)(4512,5037)

2623: \path(3387,4662)(4512,4662)

2624: \path(3387,5337)(3387,6162)(4512,6162)(4512,5337)

2625: \path(3387,5787)(4512,5787)

2626: \end{picture}

2627: }

2628: 

2629: \end{center}

2630: \caption{Abstract Machine Data Areas and Snapshot of State}

2631: \label{fig:wamstate}

2632: \end{figure}

2633: 

2634: While several data areas are carried over from the WAM, their usage in

2635: our machine differs in certain respects. In addition to storing

2636: compound terms that are created in a structure copying implementation,

2637: the heap is used in our context also to store disagreement pairs, the

2638: new terms that are generated during term reduction and the projection

2639: and imitation substitutions generated by higher-order

2640: unification. Similarly, the trail records not only the substitutions

2641: made for variables, but also the destructive changes made to terms

2642: during normalization and pointers to the pairs of terms removed from

2643: disagreement sets in the course of term simplification. Of particular

2644: note in this context are the facts that the trailing of terms requires

2645: also that old values be stored and that different kind of entries

2646: entail different unwinding actions and must be annotated appropriately

2647: for determining this. Finally, in addition to the usual choice point

2648: and environment records, the local stack must also store information

2649: about branch points in unification. These are distinguished by being

2650: labelled as {\it branch points} in Figure~\ref{fig:wamstate} that also

2651: depicts their split representation between a shared and a variable

2652: part. Only the variable parts of these records participate directly in

2653: the chain of backtracking records; the shared parts gain currency by

2654: being used by the variable parts. In the figure, we have used solid

2655: arrows to depict the shared part and the variable part of a branch

2656: point record and dashed arrows to depict the chain of branch points

2657: and choice points that determine backtracking behaviour. 

2658: 

2659: The extended machine also includes a few new registers: the {\it LL}

2660: register indicating the currently active disagreement set, the {\it

2661: SL} register indicating the current top of the {\it SL} stack, the

2662: {\it BRS} register indicating the currently relevant shared part of

2663: branch point records and the {\it NUMARGS} register that holds the

2664: (current) arity of an application encountered during head

2665: normalization.  One slightly intriguing aspect of our depiction 

2666: of the machine state is the fact that the {\it S} register that

2667: indicates the argument vector of a compound term during unification is

2668: shown pointing into the {\it SL} stack rather than the heap. The

2669: reason for this is that the top-level, head normalized structure of a

2670: higher-order term may become apparent only after a reduction process

2671: and, in this case, is available as a vector only in the {\it SL}

2672: stack. In special cases, such as when dealing with first-order terms,

2673: no reduction steps are necessary and our representation of such terms

2674: stores the arguments as a vector. Such situations can be recognized

2675: and, as an optimization, the {\it S} register can be made to point to

2676: the vector that is already available in the heap instead. 

2677: 

2678: 

2679: \subsection{Modifications to the Instruction Set}\label{ssec:instset}

2680: 

2681: A compilation model for our language must account for certain new

2682: aspects in comparison with the one for Prolog. These aspects include a

2683: representation of terms that differs even over the first-order

2684: fragment, the possibility for function variables and abstractions to

2685: appear in terms, the need to realize higher-order unification and the

2686: necessity to treat mixed intensional and extensional uses of predicate

2687: terms. We discuss these aspects in more detail below and we also

2688: indicate changes to the instruction set of the WAM that are geared

2689: towards treating them.

2690: 

2691: 

2692: \medskip

2693: 

2694: \noindent {\bf Creating Typed, Higher-Order Terms.} The usual

2695: compilation model requires that the arguments of atomic goals

2696: appearing in the bodies of clauses be set up in registers prior to the

2697: invocation of code for the relevant procedures. In the case that such

2698: an argument is a compound term, its representation must be created in

2699: the heap with a reference to it being placed in the relevant

2700: register. These effects are actually realized through the {\it put}

2701: and {\it unify} classes of instructions present in the WAM,

2702: the latter being executed in write mode in these particular

2703: situations. 

2704: 

2705: This basic structure carries over well to our higher-order

2706: language and many specific instructions from the WAM can even be

2707: retained for processing first-order like structure. There are,

2708: however, two exceptions. First, in our context, types are retained with

2709: variables and the instructions that create them must, for this reason,

2710: take an extra type argument. In particular, these instructions might

2711: take on the forms

2712: \begin{tabbing}

2713: \qquad\=\kill

2714: \>{\it put\_variable Vi,Aj,type}, and \\

2715: \>{\it unify\_variable Vi,type}

2716: \end{tabbing}

2717: \noindent where {\it Vi} is either a permanent or temporary variable

2718: and {\it type} is a reference to the representation of a

2719: type. The second difference arises from the modified representation of

2720: a structure. We encode this as an application whose argument part is a

2721: pointer to a vector with a size matching the arity of the

2722: application. Moreover, in the general case, the 

2723: `function' part of the application could be different from a

2724: constant. In light of this, the {\it put\_structure} instruction might

2725: be generalized to a {\it put\_app} instruction that fashions an

2726: application on the heap. The abstract machine underlying the {\it

2727: Teyjus} system, in fact, includes two instructions of the form

2728: \begin{tabbing}

2729: \qquad\=\kill

2730: \>{\it put\_capp Ai,Xj,n}, and \\

2731: \>{\it put\_fapp Ai,Xj,n}

2732: \end{tabbing}

2733: \noindent for this purpose. Each of these instructions creates an

2734: application whose function part is obtained from the register {\it

2735: Xj} and leaves a reference to this application in the register {\it

2736: Ai}. Moreover, the application that is created has arity {\it n}, a

2737: fact that is realized by allocating a vector of this size in the heap

2738: for the argument part and by preparing to fill in these arguments by

2739: setting the {\it S} register to the beginning of this vector and

2740: turning the write mode on. The difference between the two instructions

2741: is that the first annotates the application as closed whereas the

2742: second annotates it as (possibly) open. 

2743: 

2744: The higher-order nature of our terms can manifest itself in three

2745: ways in the syntax: the function part may be a variable, abstraction

2746: may be explicitly present and there may be occurrences of abstracted

2747: variables. The instruction for creating applications already accounts

2748: for the special case of a variable `functor.' To support the creation

2749: of abstractions, new instructions may be added to the {\it put} and

2750: {\it unify} classes. The abstract machine for {\it Teyjus}

2751: includes the following instructions for this purpose:

2752: \begin{tabbing}

2753: \qquad\={\it put\_clambda Ai,Xj}\qquad\qquad\=\kill

2754: \>{\it put\_clambda Ai,Xj}\>{\it unify\_clambda Xj}\\

2755: \>{\it put\_flambda Ai,Xj}\>{\it unify\_flambda Xj}

2756: \end{tabbing}

2757: \noindent The {\it put} versions create abstractions whose bodies are

2758: given by the contents of register {\it Xj} on the heap and put

2759: references to these abstractions in the register {\it

2760: Ai}.\footnote{The register {\it Xj} may contain a constant, in which

2761: case the first action of these instructions is to convert {\it Xj}

2762: into a reference to a location on heap containing this constant.} The

2763: difference between the two instructions provided for this purpose is

2764: that one creates closed abstractions and the other open

2765: ones. The {\it unify} versions, that are only ever executed in write

2766: mode,  create similar abstractions but eventually put references to

2767: these in the heap location pointed to by the {\it S} register and also

2768: increment this register at the end. Finally, to support the creation

2769: of bound variables, represented using indices in the de Bruijn scheme,

2770: the following instructions in which {\it n} is a positive number, are

2771: included in our abstract machine: 

2772: \begin{tabbing}

2773: \qquad\={\it put\_index Ai,n}\qquad\qquad\=\kill

2774: \>{\it put\_index Ai,n}\>{\it unify\_index n}

2775: \end{tabbing}

2776: The first instruction writes a bound variable with index {\it n} on

2777: the heap and makes the register {\it Ai} a reference to this

2778: location. The {\it unify\_index} instruction, which, also is only

2779: executed in write mode, stores this bound variable in the location

2780: pointed to by the {\it S} register and then increments this register.

2781: 

2782: In the instructions that create applications and abstractions, the

2783: function part and the abstraction body are both obtained from

2784: registers. However, these components may in particular situations 

2785: correspond to permanent variables. Furthermore, they may actually

2786: dereference to stack cells that must be globalized prior to use. In

2787: light of these possibilities, our abstract machine includes the

2788: instructions {\it globalize Yi,Xj} and {\it globalize Xj}. The first

2789: instruction dereferences the permanent (environment) variable {\it

2790: Yi}. If this turns out to be a reference to the stack, then the value

2791: is copied to the heap and the stack cell and the register {\it Xj} are

2792: both converted into references to the newly created heap

2793: cell. Otherwise the reference that we get to a heap cell is also

2794: stored in the register {\it Xj}. The second instruction simply

2795: dereferences the {\it Xj} register, globalizes this as before if

2796: necessary and leaves a reference to a suitable heap cell in {\it Xj}.

2797: 

2798: \medskip

2799: 

2800: \noindent {\bf Compilation of Higher-Order Unification.} In any given

2801: use of a clause, the terms that appear as arguments of the head of a

2802: clause must be unified with the terms that arrive in the relevant

2803: argument registers. The compilation model for Prolog translates each

2804: of these statically known terms into a sequence of instructions that

2805: either creates a relevant term that the incoming argument is bound to

2806: if this argument is an uninstantiated variable and that carries out an

2807: analysis of the structure of the argument if it is not a

2808: variable. This model requires the same instructions to function in two 

2809: different dynamically determined ways, an ability that is realized

2810: through the use of the read and write modes. 

2811: 

2812: Lifting this treatment of unification to cover the operation in its

2813: entirety in the higher-order situation is difficult. In particular,

2814: statically available structure is not directly usable once a function

2815: variable with arguments is reached in it and is also difficult to

2816: exploit when a flexible, nonvariable part is exposed in the incoming

2817: term relative to which a set of matching substitutions have to be

2818: tried. However, at least the first phase of term simplification can be

2819: compiled and, if augmented with the simple forms of variable bindings

2820: discussed in Section~\ref{ssec:disset}, most of the unification

2821: computation that arises in practice can be treated completely within

2822: this phase. 

2823: 

2824: The {\it get} and {\it unify} class of WAM instructions that treat

2825: head unification can, in fact, be adapted to realize this idea when 

2826: the term to be compiled has a first-order structure at the top level,

2827: \ie, when it is a variable, a constant or an application in which the

2828: head is a constant.\footnote{Since this term will be normalized prior

2829: to compilation, the only remaining possibilities are that it is an

2830: abstraction or an application with a variable at the head.} However, a

2831: few changes in interpretation are necessary for the instructions {\it

2832: get\_structure}, {\it get\_constant} and {\it unify\_constant} that

2833: are used in compiling rigid structure. First, these instructions must

2834: take responsibility for head normalizing the input term at the

2835: outset. In practice, many of these terms have a first-order structure,

2836: a fact that can be recognized through a check of their heads (that

2837: constitutes an overhead only when the terms are {\it not} first-order

2838: ones) built into 

2839: the relevant instructions so that an explicit invocation of

2840: head normalization can be avoided. Notice that the {\it

2841: get\_structure} instruction must set the {\it S} register to point to

2842: the vector of arguments in case the incoming term is itself an

2843: application with the right head and, under the considered

2844: optimization, this would become a pointer either into the {\it SL}

2845: stack or into the heap.  The second change is that when the incoming

2846: term is a variable, the {\it get\_structure} instruction must create

2847: an application of a specified arity on the heap and so should get this

2848: arity as an additional argument. In the {\it Teyjus} abstract machine,

2849: the instruction actually has the format

2850: \begin{tabbing}

2851: \qquad\=\kill

2852: \>{\it get\_structure Ai,f,n}

2853: \end{tabbing}

2854: \noindent where {\it n} is a positive number; when executed in a mode

2855: in which a term has to be created, this instruction pushes an

2856: application with arity {\it n} and function part {\it f} onto the

2857: heap, followed by a vector of size {\it n} constituting the argument

2858: part of this application and sets the {\it S} register to the

2859: beginning of this vector.  The final change arises from the fact that

2860: these instructions must also cater to the possibility that the

2861: incoming term is an application with a flexible head. One possible

2862: strategy in such a case is to add a suitable pair to the existing

2863: disagreement set and to leave its further processing to a later

2864: interpretive treatment of genuine higher-order unification. In the

2865: situation where the instruction is {\it get\_structure}, we note that

2866: the added disagreement pair will actually involve a term that is

2867: created by subsequent actions carried out by this and following

2868: instructions executed in write mode.

2869: 

2870: It is in principle possible to extend the compilation of first-order

2871: like structure to include the case of terms that have abstractions at

2872: their head. However, it is not clear if enough situations where this

2873: is needed will occur in practice so as to make such a treatment

2874: pragmatically useful. We therefore describe a simpler approach that

2875: works uniformly for this case as well as for the last remaining case

2876: which is that of an application whose head is a variable. In essence,

2877: the term in both situations may be translated into a sequence of

2878: instructions that constructs its representation and leaves a reference

2879: to it in a register, followed by an instruction that invokes term

2880: simplification in interpretive mode. We have already discussed

2881: instructions for creating higher-order terms. To realize the last

2882: effect, we may use the {\it get\_value} instruction from the WAM that,

2883: in any case, has to be adapted to deal with higher-order terms. In

2884: particular, in the new form, the instruction invokes an interpretive

2885: phase of term simplification that may make simple bindings for

2886: variables and that may add new flexible-rigid pairs to the existing

2887: disagreement set. A similar kind of generalization

2888: must be made to the {\it unify\_value} instruction. Actually, another

2889: change to these instructions is also necessary. Although usual

2890: implementations of Prolog omit occurs-checks, the place to carry these

2891: out if they are included would be within the process invoked by the

2892: {\it get\_value} and the {\it unify\_value} instructions. The situation

2893: in the higher-order case is similar, except that rigid path checks

2894: would replace occurs checks. These checks turn out to be indispensable

2895: to the envisaged applications of the language whose implementation we

2896: are considering, and so they are included in the `higher-order'

2897: versions of the {\it get\_value} and {\it unify\_value}

2898: instructions.\footnote{These rigid path checks need the complete

2899:   normalization of incoming terms, bringing up an interesting

2900:   question: is there still an advantage to laziness in substitution

2901:   and reduction? This issue is examined in detail in \cite{LNX03}. The 

2902:   conclusion from this study is, briefly, that a demand driven

2903:   approach to reduction that exploits explicit substitutions has

2904:   significant advantages even if the particular style chosen in

2905:   this paper is not uniquely the best.}

2906: Now, as discussed in Section~\ref{ssec:disset}, a rigid path check may

2907: permit only a partial instantiation of a variable, the rest of the

2908: instantiation being subject to the resolution of constraints

2909: represented by new flexible terms and relevant subparts of the

2910: incoming terms. 

2911: When creating these terms, the type of the new (logic) variables at

2912: their heads must be written to the heap. These types can be generated

2913: from a knowledge of the type of the variable whose compilation yields

2914: the {\it unify\_value} instruction and, conversely, the type of this

2915: variable is needed at least in the case when the constraint involves

2916: the entire incoming term. 

2917: In keeping with this observation, the {\it unify\_value} instruction 

2918: acquires a type as an additional argument.

2919: 

2920: After simplification has been carried out relative to all the terms

2921: appearing in the head of a clause, it may be necessary to invoke an

2922: interpretive phase of higher-order unification. Our abstract machine

2923: includes three instructions for this purpose. One of these, the {\it

2924: proceed\_finish\_unify} instruction, is used in place of the {\it

2925: proceed} instruction of the WAM in the situation when the clause body

2926: is empty and when an unresolved higher-order unification problem may

2927: exist. The effect of this instruction is to set the program pointer to

2928: the continuation point, to set up the shared part of a branch point

2929: record and, finally, to invoke code that tries to complete the

2930: unification process. The code that is invoked tries to generate a

2931: matching substitution. If one is found, then this is applied to the

2932: state, the variable part of a branch point record representing the

2933: remaining matching substitutions is created and the simplification

2934: and substitution generation processes are iterated.  A point to note

2935: about the situation in which {\it proceed\_finish\_unify} is used is

2936: that no argument registers need to be stored in the shared part of the

2937: branch point record. The second instruction, {\it

2938: execute\_finish\_unify}, is used when the body of the clause consists

2939: of a single atomic goal. This instruction differs from {\it

2940: proceed\_finish\_unify} in that it must update the program pointer to

2941: the next instruction in sequence and also save the continuation point

2942: and relevant argument registers in the shared part of the branch point

2943: record for use on backtracking. The number of argument registers

2944: that must be remembered becomes a parameter to this instruction. The

2945: final instruction, {\it call\_finish\_unify}, is used when the body of

2946: the clause has multiple goals in it, and therefore requires an

2947: environment record to be created for its invocation. This instruction

2948: behaves differently from {\it execute\_finish\_unify} in only two

2949: respects. First, it does not need to save the continuation point since

2950: this is available from the environment record. Second, before

2951: it allocates space for the shared part of the branch point record, the

2952: instruction must ensure that sufficient space has been left for the

2953: permanent variables in the clause. On account of the latter

2954: requirement, {\it call\_finish\_unify} acquires the count of 

2955: the permanent variables as an argument, in addition to the count of

2956: the register arguments that need to be saved.

2957: 

2958: The interpretive phase of unification is, of course, not always

2959: needed. In particular, it need only be considered if the compiled

2960: form of term simplification leads to additions to the original

2961: disagreement set or to bindings for variables that have the

2962: potential of modifying the status of existing pairs. Compile-time

2963: analysis can sometimes determine this cannot happen and,

2964: consequently, that the new instructions need not be used. Even when the

2965: instructions are included in the compiled code, they can incorporate a

2966: checking of flags set during the compiled term simplification phase to

2967: determine if further processing is necessary. The {\it Teyjus}

2968: implementation utilizes such ideas to avoid unnecessary examination of

2969: disagreement sets and setting up of the shared parts of branch point

2970: records. 

2971: 

2972: \medskip

2973: 

2974: \noindent {\bf Treating Mixed Uses of Predicates.} The crux of this

2975: treatment is the compilation of flexible atomic goals: mixed uses of

2976: predicate terms arises essentially from the fact that flexible goals

2977: may be instantiated by terms with complex logical structure, thereby

2978: reflecting intensional occurrences of quantifiers and connectives into

2979: positions where they function as search directives. 

2980: 

2981: The problem in the treatment of flexible atomic goals is, of course,

2982: that their top-level structure is determined dynamically, and so the

2983: specific action to be performed is not known at compilation time.

2984: Nevertheless, some part of the action can be compiled by using the

2985: knowledge of the possible cases that can arise. In particular,

2986: flexible goals can be compiled into calls to a special procedure named 

2987: {\it solve} to which (the instantiated version of) the goal is

2988: provided as an argument. In the case that (the normalized form of) the

2989: instantiated goal has a complex structure, the behavior of {\it solve}

2990: can be envisaged as if it were based on a compilation of the following

2991: clauses in which we use semicolon to represent disjunction in an

2992: extensional position:

2993: \begin{tabbing}

2994: \qquad\=\kill

2995: \>${\it solve \app (G1 \land G2)}$ {\tt :-} ${\it (solve\app G1),

2996: (solve\app G2)}.$\\ 

2997: \>${\it solve\app (G1 \lor G2)}$ {\tt :-} ${\it (solve\app G1) ; (solve\app G2)}.$\\

2998: \>${\it solve\app (\Sigma \app G)}$ {\tt :-} ${\it solve\app (G\app X)}.$

2999: \end{tabbing}

3000: \noindent To complete the description of {\it solve}, it only remains

3001: to specify its behaviour in the situation when its argument is an atomic

3002: goal. In the case that this goal is a flexible one, {\it solve}

3003: succeeds after instantiating the head of the goal to a term of the

3004: form $\lambda\, \ldots \lambda\, \top$, the binder being chosen based

3005: on type considerations. If this goal is a rigid one, then its

3006: arguments are loaded into appropriate argument registers and the head

3007: is used to determine the code to be invoked next. 

3008: 

3009: In the {\it Teyjus} implementation, the {\it solve} predicate is

3010: treated as a builtin one whose realization is `hard-wired' into 

3011: that of the abstract machine. 

3012: 

3013: \subsection{Examples of Compiled Code}

3014: 

3015: Based on the compilation scheme described in this section, code of the

3016: following form might be generated from the definition of the ${\it

3017: mapfun}$ predicate presented in Section~\ref{sec:hohc}:

3018: \begin{tabbing}

3019: \qquad\={\it mapfun:}\quad\={\it switch\_on\_term L2, L3, L5, fail}\quad\=\kill

3020: \>{\it mapfun:}\>{\it switch\_on\_term L2, L3, L5, fail}\>{\it \%}\\

3021: \>{\it L2:}\>{\it try\_me\_else L4, 3}\>{\it \% mapfun}\\

3022: \>{\it L3:}\>{\it get\_nil A1}\>{\it \% nil}\\

3023: \>\>{\it get\_nil A3}\> {\it \% F nil}\\

3024: \>\>{\it proceed\_finish\_unify}\>{\it \%}\\

3025: \>{\it L4:}\>{\it trust\_me 3}\>{\it \% mapfun}\\

3026: \>{\it L5:}\>{\it get\_list A1}\>{\it \% (::} \\

3027: \>\>{\it unify\_variable A4, ty1}\> {\it \% X}\\

3028: \>\>{\it unify\_variable A1, ty2}\> {\it \%  L1)}\\

3029: \>\>{\it get\_list A3}\>{\it \% F (:: }\\

3030: \>\>{\it unify\_variable A5, ty1}\>{\it \% S1}\\

3031: \>\>{\it unify\_variable A3, ty2}\> {\it \% L2)}\\

3032: \>\>{\it globalize A2}\>{\it \%}\\

3033: \>\>{\it put\_capp A6, A2, 1}\> {\it \% S2 = (F }\\

3034: \>\>{\it unify\_value A4, ty1}\> {\it \% X)}\\

3035: \>\>{\it get\_value A6, A5}\>{\it \% S1 = S2}\\

3036: \>\>{\it execute\_finish\_unify 3}\>{\it \% :-}\\

3037: \>\>{\it execute mapfun}\>{\it \% mapfun L1 F L2}

3038: \end{tabbing}

3039: \noindent This code uses the instructions {\it get\_nil} and {\it

3040: get\_list} that realize, as in the WAM, special cases of the {\it

3041: get\_constant} and {\it get\_structure} instructions. Also used is

3042: the instruction {\it switch\_on\_term} that adapts an indexing

3043: instruction with the same name from the WAM. In our context, this

3044: instruction takes the form 

3045: \begin{tabbing}

3046: \qquad\=\kill

3047: \> {\it switch\_on\_term V,C,L,BV}

3048: \end{tabbing}

3049: \noindent where {\it V}, {\it C}, {\it L} and {\it BV} are

3050: addresses to which control must be transferred in case the

3051: head normalized and dereferenced version of the value stored in

3052: register {\it A1} is, respectively, a flexible term, a rigid term that

3053: has a constant different from {\it ::} as its head, a nonempty list or

3054: a term with a bound variable as its head. In the use that is made of

3055: this instruction above, {\it fail} is assumed to be the location of

3056: code that causes backtracking. The instructions {\it try\_me\_else}

3057: and {\it trust\_me} that are used here function as they do in the WAM

3058: to create, utilize and discard choice points; an extra numeric

3059: argument has been included with each of them that indicates the number

3060: of argument registers that are to be saved or retrieved as

3061: relevant. The {\it unify\_variable} and {\it unify\_value}

3062: instructions that are used take type parameters for reasons that we

3063: have already explained. In this particular instance, {\it ty1} and

3064: {\it ty2} are to be understood as references to the representation of

3065: the types {\it i} and {\it (list i)}, respectively. We note that in

3066: the only place where the {\it unify\_value} instruction appears in

3067: this code, there is no utility for the type argument and, observing that

3068: this instruction will never be executed in read mode, we may replace

3069: it with a special {\it set\_value} instruction as suggested in

3070: \cite{HAK91}.\footnote{This is, in fact, what is done in the abstract

3071: machine and compilation model actually underlying the {\it Teyjus}

3072: implementation.} As a final comment, we observe that both the {\it

3073: proceed\_finish\_unify} and the {\it execute\_finish\_unify}

3074: instructions that appear in this code are essential: depending on the

3075: form of the first and third incoming arguments, execution of the term

3076: simplification code for either clause may lead to bindings that affect

3077: the state of the existing disagreement set.

3078: 

3079: The definition of ${\it mappred}$ presented in Section~\ref{sec:hohc}

3080: illustrates a mixed use of a predicate variable. Compilation of that

3081: definition might produce the following code: 

3082: \begin{tabbing}

3083: \qquad\={\it mappred:}\quad\={\it switch\_on\_term L2, L3, L4, fail}\quad\=\kill

3084: \>{\it mappred:}\>{\it switch\_on\_term L2, L3, L5, fail}\>{\it \%}\\

3085: \>{\it L2:}\>{\it try\_me\_else L4, 3}\>{\it \% mappred}\\

3086: \>{\it L3:}\>{\it get\_nil A1}\>{\it \% nil}\\

3087: \>\>{\it get\_nil A3}\>{\it \% P nil}\\

3088: \>\>{\it proceed\_finish\_unify}\>{\it \%}\\

3089: \>{\it L4:}\>{\it trust\_me 3}\>{\it \% mappred}\\

3090: \>{\it L5:}\>{\it allocate}\>{\it \%}\\                     

3091: \>\>{\it get\_list A1}\>{\% (:: }\\

3092: \>\>{\it unify\_variable A4, ty1}\>{\it \% X}\\

3093: \>\>{\it unify\_variable Y2, ty2}\>{\it \% L1)}\\

3094: \>\>{\it get\_variable Y1, A2}\>{\it \% P}\\

3095: \>\>{\it get\_list A3}\>{\it \% (:: }\\

3096: \>\>{\it unify\_variable A2, ty1}\>{\it \% Y}\\

3097: \>\>{\it unify\_variable Y3, ty2}\>{\it \% L2)}\\

3098: \>\>{\it call\_finish\_unify 3, 3}\>{\it \% :- }\\

3099: \>\>{\it globalize Y1, A3}\>{\it \%}\\

3100: \>\>{\it put\_capp A1, A3, 2}\>{\it \% S1 = (P }\\

3101: \>\>{\it unify\_value A4, ty1}\>{\it \% X}\\

3102: \>\>{\it unify\_value A2, ty1}\>{\it \% Y)}\\

3103: \>\>{\it call solve, 3}\>{\it \% S1, }\\

3104: \>\>{\it put\_value Y2, A1}\>{\it \% (mappred L1}\\

3105: \>\>{\it put\_value Y1, A2}\>{\it \% P}\\

3106: \>\>{\it put\_value Y3, A3}\>{\it \% L2}\\

3107: \>\>{\it deallocate}\>{\it \%}\\

3108: \>\>{\it execute mappred}\>{\it \% )}

3109: \end{tabbing}

3110: \noindent We assume here that {\it ty1} and {\it ty2} are references

3111: to the representation of the types {\it i} and {\it (list i)},

3112: respectively. The flexible goal {\it (P X Y)} is translated in this

3113: code by a call to the predicate {\it solve} as discussed earlier in

3114: this section. Towards understanding the nature of 

3115: this translation, we might consider the execution of the query

3116: \begin{tabbing}

3117: \qquad\=\kill

3118: \> ${\it mappred} \app ({\it bob} :: {\it sue} :: {\it nil}) \app (\lambdax {x} \lambdax {y}

3119: \somex {z} ({\it parent} \app x \app z) \land ({\it parent} \app z \app y))\app L$.

3120: \end{tabbing}

3121: \noindent discussed in Section~\ref{sec:hohc}. Clause indexing will

3122: lead to the selection of the code for the second clause for {\it

3123: mappred} in this case. The term simplification part of this code will

3124: execute successfully, the term $\somex {z} ({\it parent} \app

3125: {\it bob} \app z) \land ({\it parent} \app z \app y))$ will be formed

3126: and stored in register {\it A1} and the code for {\it solve} will be

3127: invoked. Using the definition of {\it solve}, this goal will be

3128: simplified,  leading eventually to the invocation of the atomic goals

3129: {\it (parent bob Z)} and {\it (parent Z Y)}. The recursive call to

3130: {\it mappred} will lead, in a similar fashion, to the invocation of the

3131: atomic goals {\it (parent sue Z')} and {\it (parent Z' Y')}. The query

3132: variable {\it L} will be bound at the end to a list 

3133: containing the values determined for {\it Z} and {\it Z'} by these

3134: goals. Another point to note is that all the unification problems

3135: that arise relative to the query of interest are ones that can be

3136: solved without the invocation of the interpretive, higher-order

3137: phase. 

3138: 

3139: 

3140: \section{Conclusion}\label{sec:conc}

3141: 

3142: We have considered in this paper the implementation of an extension to

3143: logic programming that is based on permitting a quantification over

3144: predicate and function symbols and on using lambda terms as data

3145: structures in place of first-order terms. In addition to a careful

3146: exposition of the issues that need to be dealt with in a low-level

3147: realization of such an extension, our contributions are threefold: we

3148: have discussed representations for lambda terms that facilitate their

3149: intensional treatment, we have presented mechanisms for realizing term

3150: reduction and for supporting higher-order unification within a logic

3151: programming machine model and we have sketched an approach to

3152: compilation. The ideas that we have presented here have been used in

3153: amalgamation with other devices that we have developed for the

3154: treatment of new scoping mechanisms and of polymorphic typing in an

3155: actual implementation of the $\lambda$Prolog language.

3156: 

3157: A question often of interest in the context of language

3158: enrichments is the performance degradation that is to be incurred on

3159: account of them. There are two factors that lead to a different

3160: treatment of first-order programs within our framework from that in

3161: traditional Prolog implementations. First, as discussed in

3162: Section~\ref{ssec:intrep}, a representation must be used for

3163: compound terms that permits changes to be made to internal nodes in

3164: their tree-like structure. Second, the occurs-check that is usually

3165: omitted in logic programming languages is not really a luxury in the

3166: important higher-order applications. A third factor, not discussed

3167: here but that is relevant to the full $\lambda$Prolog language, is a

3168: runtime overhead arising from polymorphic typing. 

3169: The impact of the occurs-check is obviously non-uniform and therefore

3170: impossible to quantify in a general manner. A careful assessment of the

3171: first and third factors requires experiments with controlled auxiliary

3172: implementations, something beyond the scope of this

3173: paper. However, a rough assessment is possible. Lists receive a

3174: specialized treatment in 

3175: the {\it Teyjus} system that comes close to the usual representation

3176: of first-order structures. By contrasting performance under such a

3177: treatment with that when a vanilla functor-based representation is

3178: used, a sense of the additional cost can be obtained.

3179: 

3180: \begin{table}

3181: \caption{Timing Comparisons with Prolog Implementations over Naive Reverse}

3182: \label{fig:nrev}

3183: \begin{minipage}{\textwidth}

3184: \begin{tabular}{lccc}

3185: \hline\hline

3186: {\it System}& {\it Special List} & \multicolumn{2}{c}{\it Functor Based}\\

3187: {\it Employed} & {\it Representation} & \multicolumn{2}{c}{\it

3188: Representation}\\

3189: \hline

3190: {\it Teyjus (v 1.0-b32)} & 11.99 secs & 18.67 secs &  21.18 secs\\

3191: & {\it (Polymorphic)} &{\it\qquad (Monomorphic)} & {\it (Polymorphic)}\qquad\\

3192: \noalign{\vspace {0.5cm}}

3193: {\it SWI-Prolog (v 4.0.0)} & 8.1 secs & \multicolumn{2}{c}{8.8

3194: secs}\\

3195: \noalign{\vspace {0.5cm}}

3196: {\it SICStus (v 3.9.1)} & 0.23 secs & \multicolumn{2}{c}{0.35 secs} \\

3197: \hline\hline

3198: \end{tabular}

3199: \end{minipage}

3200: \end{table}

3201: 

3202: Table~\ref{fig:nrev} presents the results of the kind of experiment

3203: described above, performed with {\it Teyjus} version 1.0-b32 modified

3204: to omit the occurs-check. The numbers in the table represent the time

3205: taken by 10,000 invocations of naive reverse on a 30 element

3206: list. All trials, here and below, were carried out on a 440 MHz

3207: UltraSPARC-IIi processor. A functor-based representation for lists in

3208: {\it Teyjus} can be chosen to be either monomorphic or polymorphic in

3209: nature and execution times are provided for both.  In contrast, the

3210: specialized list representation is available only in polymorphic

3211: form. From the timing measurements for the polymorphic versions, we

3212: conclude that there is about a 75\% overhead to not using the

3213: specialized representation. This is appropriately viewed as an upper

3214: bound on the additional cost for a higher-order representation, at

3215: least some of the improved performance being attributable

3216: to specialized compilation for lists. Polymorphism adds about a 13.5\%

3217: overhead in the functor-based representation and we estimate a similar

3218: cost under the special treatment of lists. For comparison, we also

3219: present performance measurements for two Prolog implementations;

3220: from the perspective of running time, these figures are

3221: best thought of as applying to monomorphic list representations. The

3222: contrast with {\it SICStus} is humbling, indicating the distance to go in

3223: building a well-engineered and highly optimized implementation, even

3224: if revealing little by way of the difference between treatments of

3225: the first-order and the higher-order language.

3226: 

3227: Another important aspect of comparison is that of contrasting our

3228: ideas and system with those of other implementations of

3229: $\lambda$Prolog. There have been four previous implementations of this

3230: language. Three of these are interpreter based, built using

3231: Prolog~\cite{lp2.7}, Lisp~\cite{elliott89elp} and Standard

3232: ML~\cite{EP91,WM97terzo}. None of these systems considered in any

3233: detail the special issues that arise in a low-level treatment of the

3234: higher-order aspects of $\lambda$Prolog and a comparison with them

3235: therefore appears not to be very meaningful.\footnote{The performance

3236: comparisons made in \cite{BR92b} with the Lisp version substantiate

3237: this viewpoint.}  The only remaining realization of $\lambda$Prolog,

3238: called {\it Prolog/Mali} \cite{BR92b}, is one that translates

3239: $\lambda$Prolog programs into C code that can then be compiled. The

3240: translation process utilizes a memory management system called {\it

3241: Mali} that has been developed especially for logic programming

3242: languages: in particular, translation is realized in the form of calls

3243: to functions supported by this system. Using this approach has the

3244: distinct benefit that a memory management scheme is automatically

3245: available but it also forces some awkward choices, such as the full

3246: copying of clause bodies, to be in consonance with the framework

3247: provided by {\it Mali}.

3248: 

3249: Despite the difference in overall structure, there is a scheme to the

3250: treatment of the higher-order aspects in {\it Prolog/Mali} that can be

3251: compared with the ideas we have presented in this paper. At the level of

3252: term representation, there seem to be three differences. First, the de

3253: Bruijn scheme for rendering bound variables is rejected in {\it

3254: Prolog/Mali} on the grounds that ``it forces to renumber the rightmost

3255: term.'' While this observation is correct in principle, it appears not

3256: to be relevant in practice as we have pointed out in

3257: Section~\ref{ssec:debruijn}. To support the comparison of terms in a

3258: situation where a name-based encoding is used for bound variables, an

3259: approach based on using new constants is suggested. Unfortunately, the 

3260: details of this approach are not explained completely making a

3261: satisfactory assessment of it impossible.\footnote{There are also vestiges

3262: of this approach in answer presentations that remain unclear to us

3263: and, quite possibly, to other $\lambda$Prolog users.} A second difference

3264: is that an explicit substitution mechanism is not considered in

3265: {\it Prolog/Mali} and reduction substitutions seem to be effected

3266: eagerly. Finally, first-order terms seem to obtain the usual

3267: Prolog-like treatment in {\it Prolog/Mali}, higher-order facets being

3268: handled via special attributes attached to terms. The treatment of

3269: higher-order 

3270: unification and the integration of reduction into the overall

3271: computational model receives little discussion in \cite{BR92b} and, in

3272: light of this, we believe that a detailed consideration of these

3273: aspects is unique to our work; an interesting exception, however, is

3274: the idea of indexing flexible-flexible pairs by their flexible heads,

3275: to be awakened by bindings for these heads, a possibility whose

3276: integration into our processing model bears investigation. The last

3277: relevant aspect is the compilation of unification. Clearly, the

3278: underlying machine model is explicitly manifest only in our work

3279: although many ideas relating to the compilation of the first phase of

3280: simplification of disagreement sets receive a similar treatment in

3281: both contexts and share also with an early presentation of some of

3282: our ideas \cite{NJ89}. 

3283: 

3284: \begin{table}

3285: \caption{Timing Comparisons between Teyjus and Prolog/Mali}

3286: \label{fig:pmcompare}

3287: \begin{minipage}{\textwidth}

3288: \begin{tabular}{lcc}

3289: \hline\hline

3290: {\it System} & {\it Naive Reverse} & {\it Type Inference}\\

3291: \hline

3292: {\it Teyjus (v 1.0-b32)} & 11.99 secs & 2.95 secs \\

3293: \noalign{\vspace{0.5cm}}

3294: {\it Prolog/Mali } & 12.00 secs & 9.59 secs\\

3295: \hline\hline

3296: \end{tabular}

3297: \end{minipage}

3298: \end{table}

3299: 

3300: 

3301: Table~\ref{fig:pmcompare} complements our qualitative comparisons by

3302: presenting execution times for {\it Prolog/Mali} and {\it Teyjus} on two

3303: different kinds of tasks. The {\it naive reverse} program is the one

3304: used in the earlier tests and, as such, provides a measure of

3305: behaviour over first-order programs. The {\it type inference} program

3306: assigns type schemes to ML-like programs and is a good example for

3307: testing performance over higher-order terms, reduction and (a

3308: specialized form of) higher-order unification.\footnote{This program

3309: also includes dynamically scoped constants and assumptions and

3310: performance differences are therefore not entirely attributable to

3311: the treatment of features discussed in this paper. However, we 

3312: intend the figures that we present to be suggestive rather than

3313: definitive for the reasons we explain.} 

3314: The indications from these tests is that the {\it Teyjus} system

3315: matches performance of {\it Prolog/Mali} over first-order programs and

3316: does significantly better on genuine higher-order ones. A larger set

3317: of tests is needed 

3318: to draw more substantive conclusions. Unfortunately, there are

3319: practical difficulties to providing a suitable collection that

3320: highlights genuine performance differences. {\it Prolog/Mali} omits

3321: the occurs-check that is significant to higher-order applications, 

3322: uses a non-standard syntax for $\lambda$Prolog programs leading to a

3323: substantial overhead in adapting available user programs to run

3324: under it and, finally, appears to yield incorrect results in a few

3325: of the examples we tried.

3326: 

3327: Our focus in this paper has been on describing a broad framework for

3328: the treatment of higher-order features in logic programming. There are

3329: obviously tradeoffs in the actual deployment of these ideas. Although

3330: beyond the scope of the present study, a quantification of these

3331: tradeoffs is important and is, in fact, the object of other work

3332: \cite{LN02,LNX03,NX03}. A particularly exciting  

3333: direction that we are now exploring is that of fine-tuning our

3334: abstract machine and compilation model to the important subclass of

3335: higher-order programs referred to as L$_\lambda$ programs

3336: \cite{miller91jlc}, possibly even with some loss of completeness over

3337: the full collection. In a different vein, many of our

3338: implementation ideas are applicable in related contexts, such as that

3339: of logic programming within a dependently typed lambda calculus

3340: \cite{Pfenning99cade}. The extension of this work in these directions

3341: is also a matter under investigation. 

3342: 

3343: \section*{Acknowledgements}

3344: 

3345: Earlier versions of the ideas in this paper have benefitted from

3346: discussions with Bharat Jayaraman and Debra Wilson. Comments from the

3347: reviewers have helped in an improved presentation. 

3348: 

3349: \begin{thebibliography}{}

3350: 

3351: \bibitem[\protect\citeauthoryear{Abadi, Cardelli, Curien, and L{\'{e}}vy}{Abadi

3352:   et~al\mbox{.}}{1991}]{ACCL91}

3353: {\sc Abadi, M.}, {\sc Cardelli, L.}, {\sc Curien, P.-L.}, {\sc and} {\sc

3354:   L{\'{e}}vy, J.-J.} 1991.

3355: \newblock Explicit substitutions.

3356: \newblock {\em Journal of Functional Programming\/}~{\em 1,\/}~4, 375--416.

3357: 

3358: \bibitem[\protect\citeauthoryear{Aiello and Prini}{Aiello and

3359:   Prini}{1981}]{AP81}

3360: {\sc Aiello, L.} {\sc and} {\sc Prini, G.} 1981.

3361: \newblock An efficient interpreter for the lambda-calculus.

3362: \newblock {\em The Journal of Computer and System Sciences\/}~{\em 23},

3363:   383--425.

3364: 

3365: \bibitem[\protect\citeauthoryear{A{\"{\i}}t-Kaci}{A{\"{\i}}t-Kaci}{1991}]{HAK9%

3366: 1}

3367: {\sc A{\"{\i}}t-Kaci, H.} 1991.

3368: \newblock {\em {W}arren's Abstract Machine: A Tutorial Reconstruction}.

3369: \newblock MIT Press.

3370: 

3371: \bibitem[\protect\citeauthoryear{Andrews}{Andrews}{1971}]{Andrews71}

3372: {\sc Andrews, P.~B.} 1971.

3373: \newblock Resolution in type theory.

3374: \newblock {\em Journal of Symbolic Logic\/}~{\em 36}, 414--432.

3375: 

3376: \bibitem[\protect\citeauthoryear{Appel and Felty}{Appel and

3377:   Felty}{1999}]{AppFel99}

3378: {\sc Appel, A.~W.} {\sc and} {\sc Felty, A.~P.} 1999.

3379: \newblock Lightweight lemmas in $\lambda${P}rolog.

3380: \newblock In {\em International Conference on Logic Programming}. MIT Press,

3381:   411--425.

3382: 

3383: \bibitem[\protect\citeauthoryear{Apt and van Emden}{Apt and van

3384:   Emden}{1982}]{AvE82}

3385: {\sc Apt, K.~R.} {\sc and} {\sc van Emden, M.~H.} 1982.

3386: \newblock Contributions to the theory of logic programming.

3387: \newblock {\em Journal of the ACM\/}~{\em 29,\/}~3, 841--862.

3388: 

3389: \bibitem[\protect\citeauthoryear{Benaissa, Briaud, Lescanne, and

3390:   Rouyer-Degli}{Benaissa et~al\mbox{.}}{1996}]{BBLR96}

3391: {\sc Benaissa, Z.}, {\sc Briaud, D.}, {\sc Lescanne, P.}, {\sc and} {\sc

3392:   Rouyer-Degli, J.} 1996.

3393: \newblock $\lambda\upsilon$, a calculus of explicit substitutions which

3394:   preserves strong normalization.

3395: \newblock {\em Journal of Functional Programming\/}~{\em 6,\/}~5, 699--722.

3396: 

3397: \bibitem[\protect\citeauthoryear{Brisset and Ridoux}{Brisset and

3398:   Ridoux}{1992}]{BR92b}

3399: {\sc Brisset, P.} {\sc and} {\sc Ridoux, O.} 1992.

3400: \newblock The compilation of $\lambda${P}rolog and its execution with {MALI}.

3401: \newblock Publication Interne No 687, IRISA, Rennes, November.

3402: 

3403: \bibitem[\protect\citeauthoryear{Church}{Church}{1940}]{Church40}

3404: {\sc Church, A.} 1940.

3405: \newblock A formulation of the simple theory of types.

3406: \newblock {\em Journal of Symbolic Logic\/}~{\em 5}, 56--68.

3407: 

3408: \bibitem[\protect\citeauthoryear{Cousineau, Curien, and Mauny}{Cousineau

3409:   et~al\mbox{.}}{1987}]{CCM87}

3410: {\sc Cousineau, G.}, {\sc Curien, P.-L.}, {\sc and} {\sc Mauny, M.} 1987.

3411: \newblock The categorical abstract machine.

3412: \newblock {\em The Science of Programming\/}~{\em 8,\/}~2, 173--202.

3413: 

3414: \bibitem[\protect\citeauthoryear{de~Bruijn}{de~Bruijn}{1972}]{debruijn72}

3415: {\sc de~Bruijn, N.} 1972.

3416: \newblock Lambda calculus notation with nameless dummies, a tool for automatic

3417:   formula manipulation, with application to the {Church-Rosser Theorem}.

3418: \newblock {\em Indag. Math.\/}~{\em 34,\/}~5, 381--392.

3419: 

3420: \bibitem[\protect\citeauthoryear{Dowek, Hardin, and Kirchner}{Dowek

3421:   et~al\mbox{.}}{2000}]{DHK00}

3422: {\sc Dowek, G.}, {\sc Hardin, T.}, {\sc and} {\sc Kirchner, C.} 2000.

3423: \newblock Higher-order unification via explicit substitutions.

3424: \newblock {\em Information and Computation\/}~{\em 157}, 183--235.

3425: 

3426: \bibitem[\protect\citeauthoryear{Dowek, Hardin, Kirchner, and Pfenning}{Dowek

3427:   et~al\mbox{.}}{1998}]{DHKP98}

3428: {\sc Dowek, G.}, {\sc Hardin, T.}, {\sc Kirchner, C.}, {\sc and} {\sc Pfenning,

3429:   F.} 1998.

3430: \newblock Unification via explicit substitutions: The case for higher-order

3431:   patterns.

3432: \newblock Tech. Rep. 3591, INRIA. December.

3433: 

3434: \bibitem[\protect\citeauthoryear{Elliott and Pfenning}{Elliott and

3435:   Pfenning}{1989}]{elliott89elp}

3436: {\sc Elliott, C.} {\sc and} {\sc Pfenning, F.} 1989.

3437: \newblock {eLP, a Common Lisp Implementation of $\lambda$Prolog}.

3438: \newblock Implemented as part of the CMU ERGO project.

3439: 

3440: \bibitem[\protect\citeauthoryear{Elliott and Pfenning}{Elliott and

3441:   Pfenning}{1991}]{EP91}

3442: {\sc Elliott, C.} {\sc and} {\sc Pfenning, F.} 1991.

3443: \newblock A semi-functional implementation of a higher-order logic programming

3444:   language.

3445: \newblock In {\em Topics in Advanced Language Implementation}, {P.~Lee}, Ed.

3446:   MIT Press, 289--325.

3447: 

3448: \bibitem[\protect\citeauthoryear{Fairbairn and Wray}{Fairbairn and

3449:   Wray}{1987}]{FW87}

3450: {\sc Fairbairn, J.} {\sc and} {\sc Wray, S.} 1987.

3451: \newblock {TIM}: A simple lazy abstract-machine to execute supercombinators.

3452: \newblock In {\em Functional Programming Languages and Computer Architecture},

3453:   {G.~Kahn}, Ed. Number 274 in Lecture Notes in Computer Science.

3454:   Springer-Verlag, 34--45.

3455: 

3456: \bibitem[\protect\citeauthoryear{Felty}{Felty}{1993}]{Felty93jar}

3457: {\sc Felty, A.} 1993.

3458: \newblock Implementing tactics and tacticals in a higher-order logic

3459:   programming language.

3460: \newblock {\em Journal of Automated Reasoning\/}~{\em 11,\/}~1 (August),

3461:   43--81.

3462: 

3463: \bibitem[\protect\citeauthoryear{Field}{Field}{1990}]{Field90}

3464: {\sc Field, J.} 1990.

3465: \newblock On laziness and optimality in lambda interpreters: Tools for

3466:   specification and analysis.

3467: \newblock In {\em Seventeenth Annual ACM Symposium on Principles of Programming

3468:   Languages}. ACM Press, 1--15.

3469: 

3470: \bibitem[\protect\citeauthoryear{Hannan and Miller}{Hannan and

3471:   Miller}{1992}]{HM92mscs}

3472: {\sc Hannan, J.} {\sc and} {\sc Miller, D.} 1992.

3473: \newblock From operational semantics to abstract machines.

3474: \newblock {\em Mathematical Structures in Computer Science\/}~{\em 2,\/}~4,

3475:   415--459.

3476: 

3477: \bibitem[\protect\citeauthoryear{Hannan and Pfenning}{Hannan and

3478:   Pfenning}{1992}]{hannan92lics}

3479: {\sc Hannan, J.} {\sc and} {\sc Pfenning, F.} 1992.

3480: \newblock Compiler verification in {LF}.

3481: \newblock In {\em Seventh Annual {IEEE} Symposium on Logic in Computer

3482:   Science}. IEEE Computer Society Press, 407--418.

3483: 

3484: \bibitem[\protect\citeauthoryear{Henderson and Morris}{Henderson and

3485:   Morris}{1976}]{HM76}

3486: {\sc Henderson, P.} {\sc and} {\sc Morris, J.~H.} 1976.

3487: \newblock A lazy evaluator.

3488: \newblock In {\em Third Annual ACM Symposium on Principles of Programming

3489:   Languages}. ACM Press, 95--103.

3490: 

3491: \bibitem[\protect\citeauthoryear{Huet}{Huet}{1975}]{Huet75}

3492: {\sc Huet, G.} 1975.

3493: \newblock A unification algorithm for typed $\lambda$-calculus.

3494: \newblock {\em Theoretical Computer Science\/}~{\em 1}, 27--57.

3495: 

3496: \bibitem[\protect\citeauthoryear{Kamareddine and R\'{i}os}{Kamareddine and

3497:   R\'{i}os}{1997}]{KR97}

3498: {\sc Kamareddine, F.} {\sc and} {\sc R\'{i}os, A.} 1997.

3499: \newblock Extending the $\lambda$-calculus with explicit substitution which

3500:   preserves strong normalization into a confluent calculus on open terms.

3501: \newblock {\em Journal of Functional Programming\/}~{\em 7,\/}~4, 395--420.

3502: 

3503: \bibitem[\protect\citeauthoryear{Kwon, Nadathur, and Wilson}{Kwon

3504:   et~al\mbox{.}}{1994}]{KNW92}

3505: {\sc Kwon, K.}, {\sc Nadathur, G.}, {\sc and} {\sc Wilson, D.~S.} 1994.

3506: \newblock Implementing polymorphic typing in a logic programming language.

3507: \newblock {\em Computer Languages\/}~{\em 20,\/}~1, 25--42.

3508: 

3509: \bibitem[\protect\citeauthoryear{Liang and Nadathur}{Liang and

3510:   Nadathur}{2002}]{LN02}

3511: {\sc Liang, C.} {\sc and} {\sc Nadathur, G.} 2002.

3512: \newblock Tradeoffs in the intensional representation of lambda terms.

3513: \newblock In {\em Conference on Rewriting Techniques and Applications},

3514:   {S.~Tison}, Ed. Lecture Notes in Computer Science, vol. 2378.

3515:   Springer-Verlag, 192--206.

3516: 

3517: \bibitem[\protect\citeauthoryear{Liang, Nadathur, and Qi}{Liang

3518:   et~al\mbox{.}}{2003}]{LNX03}

3519: {\sc Liang, C.}, {\sc Nadathur, G.}, {\sc and} {\sc Qi, X.} 2003.

3520: \newblock Choices in representation and reduction strategies for lambda terms

3521:   in intensional contexts.

3522: \newblock Tech. Rep. 2003/2, Digital Technology Center, University of

3523:   Minnesota. October.

3524: 

3525: \bibitem[\protect\citeauthoryear{Martelli and Montanari}{Martelli and

3526:   Montanari}{1982}]{MM82}

3527: {\sc Martelli, A.} {\sc and} {\sc Montanari, U.} 1982.

3528: \newblock An efficient unification algorithm.

3529: \newblock {\em ACM Transactions on Programming Lanuages and Systems\/}~{\em

3530:   4,\/}~2 (April), 258--282.

3531: 

3532: \bibitem[\protect\citeauthoryear{Michaylov and Pfenning}{Michaylov and

3533:   Pfenning}{1992}]{MP92}

3534: {\sc Michaylov, S.} {\sc and} {\sc Pfenning, F.} 1992.

3535: \newblock An empirical study of the runtime behavior of higher-order logic

3536:   programs.

3537: \newblock In {\em Conference Record of the Workshop on the $\lambda$Prolog

3538:   Programming Language}.

3539: \newblock Available as Tech. Rep. MS-CIS-92-86 from Department of Computer and

3540:   Information Sciences, University of Pennsylvania.

3541: 

3542: \bibitem[\protect\citeauthoryear{Miller}{Miller}{1991}]{miller91jlc}

3543: {\sc Miller, D.} 1991.

3544: \newblock A logic programming language with lambda-abstraction, function

3545:   variables, and simple unification.

3546: \newblock {\em Journal of Logic and Computation\/}~{\em 1,\/}~4, 497--536.

3547: 

3548: \bibitem[\protect\citeauthoryear{Miller and Nadathur}{Miller and

3549:   Nadathur}{1987}]{MN87slp}

3550: {\sc Miller, D.} {\sc and} {\sc Nadathur, G.} 1987.

3551: \newblock A logic programming approach to manipulating formulas and programs.

3552: \newblock In {\em IEEE Symposium on Logic Programming}, {S.~Haridi}, Ed. IEEE

3553:   Computer Society Press, 379--388.

3554: 

3555: \bibitem[\protect\citeauthoryear{Miller and Nadathur}{Miller and

3556:   Nadathur}{1988}]{lp2.7}

3557: {\sc Miller, D.} {\sc and} {\sc Nadathur, G.} 1988.

3558: \newblock $\lambda${P}rolog version 2.7.

3559: \newblock Distributed in C-Prolog and Quintus Prolog source code.

3560: 

3561: \bibitem[\protect\citeauthoryear{Miller, Nadathur, Pfenning, and

3562:   Scedrov}{Miller et~al\mbox{.}}{1991}]{MNPS91}

3563: {\sc Miller, D.}, {\sc Nadathur, G.}, {\sc Pfenning, F.}, {\sc and} {\sc

3564:   Scedrov, A.} 1991.

3565: \newblock Uniform proofs as a foundation for logic programming.

3566: \newblock {\em Annals of Pure and Applied Logic\/}~{\em 51}, 125--157.

3567: 

3568: \bibitem[\protect\citeauthoryear{Nadathur}{Nadathur}{1998}]{Nad98esw}

3569: {\sc Nadathur, G.} 1998.

3570: \newblock An explicit substitution notation in a $\lambda${P}rolog

3571:   implementation.

3572: \newblock Tech. Rep. TR-98-01, Department of Computer Science, University of

3573:   Chicago. January.

3574: 

3575: \bibitem[\protect\citeauthoryear{Nadathur}{Nadathur}{1999}]{Nad99jflp}

3576: {\sc Nadathur, G.} 1999.

3577: \newblock A fine-grained notation for lambda terms and its use in intensional

3578:   operations.

3579: \newblock {\em Journal of Functional and Logic Programming\/}~{\em 1999,\/}~2

3580:   (March), 1--62.

3581: 

3582: \bibitem[\protect\citeauthoryear{Nadathur and Jayaraman}{Nadathur and

3583:   Jayaraman}{1989}]{NJ89}

3584: {\sc Nadathur, G.} {\sc and} {\sc Jayaraman, B.} 1989.

3585: \newblock Towards a {WAM} model for {$\lambda$Prolog}.

3586: \newblock In {\em Proceedings of the North American Conference on Logic

3587:   Programming}, {E.~Lusk} {and} {R.~Overbeek}, Eds. MIT Press, 1180--1198.

3588: 

3589: \bibitem[\protect\citeauthoryear{Nadathur, Jayaraman, and Kwon}{Nadathur

3590:   et~al\mbox{.}}{1995}]{NJK94}

3591: {\sc Nadathur, G.}, {\sc Jayaraman, B.}, {\sc and} {\sc Kwon, K.} 1995.

3592: \newblock Scoping constructs in logic programming: Implementation problems and

3593:   their solution.

3594: \newblock {\em Journal of Logic Programming\/}~{\em 25,\/}~2 (November),

3595:   119--161.

3596: 

3597: \bibitem[\protect\citeauthoryear{Nadathur and Miller}{Nadathur and

3598:   Miller}{1988}]{NM88}

3599: {\sc Nadathur, G.} {\sc and} {\sc Miller, D.} 1988.

3600: \newblock An overview of {$\lambda$Prolog}.

3601: \newblock In {\em Fifth International Logic Programming Conference}, {K.~A.

3602:   Bowen} {and} {R.~A. Kowalski}, Eds. MIT Press, 810--827.

3603: 

3604: \bibitem[\protect\citeauthoryear{Nadathur and Miller}{Nadathur and

3605:   Miller}{1990}]{NM90}

3606: {\sc Nadathur, G.} {\sc and} {\sc Miller, D.} 1990.

3607: \newblock Higher-order {Horn} clauses.

3608: \newblock {\em Journal of the ACM\/}~{\em 37,\/}~4 (October), 777--814.

3609: 

3610: \bibitem[\protect\citeauthoryear{Nadathur and Miller}{Nadathur and

3611:   Miller}{1998}]{NM98}

3612: {\sc Nadathur, G.} {\sc and} {\sc Miller, D.} 1998.

3613: \newblock Higher-order logic programming.

3614: \newblock In {\em Handbook of Logic in Artificial Intelligence and Logic

3615:   Programming}, {C.~H. D.~Gabbay} {and} {A.~Robinson}, Eds. Vol.~5. Oxford

3616:   University Press, 499--590.

3617: 

3618: \bibitem[\protect\citeauthoryear{Nadathur and Mitchell}{Nadathur and

3619:   Mitchell}{1999}]{NM99cade}

3620: {\sc Nadathur, G.} {\sc and} {\sc Mitchell, D.~J.} 1999.

3621: \newblock System description: Teyjus---a compiler and abstract machine based

3622:   implementation of $\lambda${P}rolog.

3623: \newblock In {\em Automated Deduction--{CADE}-16}, {H.~Ganzinger}, Ed. Number

3624:   1632 in Lecture Notes in Artificial Intelligence. Springer-Verlag, 287--291.

3625: 

3626: \bibitem[\protect\citeauthoryear{Nadathur and Pfenning}{Nadathur and

3627:   Pfenning}{1992}]{NP91}

3628: {\sc Nadathur, G.} {\sc and} {\sc Pfenning, F.} 1992.

3629: \newblock The type system of a higher-order logic programming language.

3630: \newblock In {\em Types in Logic Programming}, {F.~Pfenning}, Ed. MIT Press,

3631:   245--283.

3632: 

3633: \bibitem[\protect\citeauthoryear{Nadathur and Qi}{Nadathur and Qi}{2003}]{NX03}

3634: {\sc Nadathur, G.} {\sc and} {\sc Qi, X.} 2003.

3635: \newblock Explicit substitutions in the reduction of lambda terms.

3636: \newblock In {\em Proceedings of the 5th ACM SIGPLAN international conference

3637:   on Principles and practice of declaritive programming}. ACM Press, 195--206.

3638: 

3639: \bibitem[\protect\citeauthoryear{Nadathur and Wilson}{Nadathur and

3640:   Wilson}{1998}]{NW98tcs}

3641: {\sc Nadathur, G.} {\sc and} {\sc Wilson, D.~S.} 1998.

3642: \newblock A notation for lambda terms: A generalization of environments.

3643: \newblock {\em Theoretical Computer Science\/}~{\em 198,\/}~1-2, 49--98.

3644: 

3645: \bibitem[\protect\citeauthoryear{Pfenning}{Pfenning}{1988}]{Pfe88}

3646: {\sc Pfenning, F.} 1988.

3647: \newblock Partial polymorphic type inference and higher-order unification.

3648: \newblock In {\em Proceedings of the {ACM} Lisp and Functional Programming

3649:   Conference}. ACM Press, 153--163.

3650: 

3651: \bibitem[\protect\citeauthoryear{Pfenning and Elliott}{Pfenning and

3652:   Elliott}{1988}]{PE88pldi}

3653: {\sc Pfenning, F.} {\sc and} {\sc Elliott, C.} 1988.

3654: \newblock Higher-order abstract syntax.

3655: \newblock In {\em Proceedings of the {ACM}-{SIGPLAN} Conference on Programming

3656:   Language Design and Implementation}. {ACM} Press, 199--208.

3657: 

3658: \bibitem[\protect\citeauthoryear{Pfenning and Sch{\"u}rmann}{Pfenning and

3659:   Sch{\"u}rmann}{1999}]{Pfenning99cade}

3660: {\sc Pfenning, F.} {\sc and} {\sc Sch{\"u}rmann, C.} 1999.

3661: \newblock System description: Twelf --- a meta-logical framework for deductive

3662:   systems.

3663: \newblock In {\em Proceedings of the 16th International Conference on Automated

3664:   Deduction (CADE-16)}, {H.~Ganzinger}, Ed. Springer-Verlag LNAI 1632, Trento,

3665:   Italy, 202--206.

3666: 

3667: \bibitem[\protect\citeauthoryear{Shao, League, and Monnier}{Shao

3668:   et~al\mbox{.}}{1998}]{shao98:imp}

3669: {\sc Shao, Z.}, {\sc League, C.}, {\sc and} {\sc Monnier, S.} 1998.

3670: \newblock Implementing typed intermediate languages.

3671: \newblock In {\em Proc. 1998 {ACM} {SIGPLAN} International Conference on

3672:   Functional Programming ({ICFP}'98)}. ACM Press, 313--323.

3673: 

3674: \bibitem[\protect\citeauthoryear{Warren}{Warren}{1977}]{War77}

3675: {\sc Warren, D. H.~D.} 1977.

3676: \newblock Implementing {P}rolog---compiling predicate logic programs.

3677: \newblock University of Edinburgh, D.A.I Research Reports 39 and 40, May.

3678: 

3679: \bibitem[\protect\citeauthoryear{Warren}{Warren}{1983}]{War83}

3680: {\sc Warren, D. H.~D.} 1983.

3681: \newblock An abstract {P}rolog instruction set.

3682: \newblock Technical Note 309, SRI International, October.

3683: 

3684: \bibitem[\protect\citeauthoryear{Wickline and Miller}{Wickline and

3685:   Miller}{1997}]{WM97terzo}

3686: {\sc Wickline, P.} {\sc and} {\sc Miller, D.} 1997.

3687: \newblock The {T}erzo 1.1b implementation of {$\lambda$Prolog}.

3688: \newblock Distribution in NJ-SML source files. See

3689:   \verb+http://www.cse.psu.edu/~dale/lProlog/+.

3690: 

3691: \end{thebibliography}

3692: 

3693: 

3694: \end{document}

3695: 

3696: