Technical Reports for 1994
Duke University
Department of Computer Science
Durham, North Carolina

CS-1994-01 - A Notation for Lambda Terms II: Refinements and Applications, Gopalan Nadathur, Debra Sue Wilson.

Issues that are relevant to the representation of lambda terms in contexts where their intensions have to be manipulated are examined. The basis for such a representation is provided by the suspension notation for lambda terms that is described in a companion paper. This notation obviates -conversion in the comparison of terms by using the `nameless' scheme of de Bruijn and also permits a delaying of substitutions by including a class of terms that encode other terms together with substitutions to be performed on them. The suspension notation contains a mechanism for `merging' substitutions so that they can be effected in a common structure traversal. The mechanism is cumbersome to implement in its full generality and a simplification to it is considered. In particular, the old merging operations are eliminated in favor of new ones that capture some of their functionality and that permit a simplified syntax for terms. The resulting notation is refined by the addition of annotations to terms that serve to indicate whether or not they can be affected by substitutions generated by external -contractions. These annotations permit substitutions to be performed trivially in certain situations, and can consequently lead to a conservation of space and time in a graph-based implementation of reduction. The use of the refined notation in the comparison of terms is then examined. The notion of head normal forms is generalized to its context and shown to be useful in checking terms for equality and a graph-based procedure for finding head normal forms is presented. This procedure is accompanied by a complete proof of its correctness and the tools of analysis afforded by our notation are used in this process. The relevance of the considerations here to an ongoing implementation of the language >=Prolog is discussed.

CS-1994-02 - Selection in Monotone Matrices and Computing kth Nearest Neighbors, Pankaj K. Agarwal, Sandeep Sen.

An m? n matrix A = (aij), 1 <= i <= m and 1 <= j <= n, is called a totally monotone matrix if for all i1; i2; j1; j2, satisfying 1 <= i1 < i2 <= m; 1 <= j1 < j2 <= n,

ai1j1 < ai1j2 =) ai2j1 < ai2j2 :

We present an O((m + n)pn log n) time algorithm to select the kth smallest item from an m ? n totally monotone matrix for any k <= mn. This is the first subquadratic algorithm for selecting an item from a totally monotone matrix. Our method also yields an algorithm for generalised row selection in monotone matrices of the same time complexity. Given a set S = fp1; : : : ; png of n points in convex position and a vector k = fk1; : : : ; kng, we also present an O(n4=3 logc n) algorithm to compute the kthi nearest neighbor of pi for every i <= n; c is an appropriate constant. This algorithm is considerably faster than the one based on a row-selection algorithm for monotone matrices. If the points of S are arbitrary, then the kthi nearest neighbor of pi, for all i <= n, can be computed in time O(n7=5 logc n), which also improves upon the previously best-known result.

CS-1994-03 - (Revision of CS-1993-22) A Notation for Lambda Terms I: A Generalization of Environments, Gopalan Nadathur, Debra S. Wilson.

A notation for lambda terms is described that is useful in contexts where the intensions of these terms need to be manipulated. This notation uses the scheme of de Bruijn for eliminating variable names, thus obviating -conversion in comparing terms. This notation also provides for a class of terms that can encode other terms together with substitutions to be performed on them. The notion of an environment is used to realize this `delaying' of substitutions. The precise mechanism employed