- TR-83-01 Formalizing Non-Monotonic Reasoning Systems, January 1983 David W. Etherington
In recent years, there has been considerable interest in non-monotonic reasoning systems. Unfortunately, formal rigor has not always kept pace with the enthusiastic propagation of new systems. Formalizing such systems may yield dividends in terms of both clarity and correctness. We show that Default Logic is a useful tool for the specification and description of non-monotonic systems, and present new results which enhance this usefulness.

- TR-83-02 Data Types as Term Algebras, March 1983 K, Akira a and Karl Abrahamson
Data types in programming have been mathematically studied from two different viewpoints, namely data types as (initial) algebras and data types as complete partial orders. In this paper, we explore a possibility of finitaristic approach. For finitarists, the only sets accepted are ``recursively defined'' sets. We observe that recursive definition not only defines a set of terms but also basic operations over them, thus it induces an algebra of terms. We compare this approach to the existing two approaches. Using our approach we present finer classification of data types.

- TR-83-03 Numeration Models of $\lambda$-Calculus, April 1983 K and Akira a
Models of $\lambda$-calculus have been studied by Church [2] and Scott [7]. In these studies, finding solutions to the isomorphic equations \(S \approx [S \rightarrow S] \) where \( [S \rightarrow S] \) is a certain set of functions from $S$ to $S$ is the main issue. In this paper, we present an example of such solutions which fails to be a model of $\lambda$-calculus. This example indicates the necessity of careful consideration of the syntax of $\lambda$-calculus, especially for the study of constructive models of $\lambda$-calculus. Taking this into account, we axiomatically show when a numeration of Er\u{s}ov [3] forms a model of $\lambda$-calculus. This serves as a general framework for countable models of $\lambda$-calculus. Various examples of such numerations are studied. An algebraic characterization of this class of numerations is also given.

- TR-83-04 On the Complexity of Achieving K-Consistency, January 1983 Raimund Seidel
A number of combinatorial search problems can be formulated as constraint satisfaction problems. Typically backtrack search is used to solve these problems. To counteract the frequent thrashing behaviour of backtrack search, methods have been proposed to precondition constraint satisfaction problems. These methods remove inconsistencies involving only a small number of variables from the problem. In this note we analyze the time complexity of the most general of these methods, Freuder's $k$-consistency algorithm. We show that it takes worst case time $O(n^{k})$, where $n$ is the number of variables in the problem.

- TR-83-05 A Linear Algorithm for Determining the Separation of Convex Polyhedra, January 1983 David P. Dobkin and David G. Kirkpatrick
The separation of two convex polyhedra is defined to be the minimum distance from a point (not necessarily an extreme point) of one to a point of the other. We present a linear algorithm for constructing a pair of points that realize the separation of two convex polyhedra in three dimensions. Our algorithm is based on a simple hierarchical description of polyhedra that is of interest in its own right. .br Our result provides a linear algorithm for detecting the intersection of convex polyhedra. Separation and intersection detection algorithms have applications in clustering, the intersection of half-spaces, linear programming, and robotics.

- TR-83-06 (g,f) - Factors \& Packings, When g
(Abstract not available on-line)

- TR-83-07 Marriage Before Conquest: A Variation on the Divide \& Conquer Paradigm, October 1983 David G. Kirkpatrick and Raimund Seidel
We present a new planar convex hull algorithm with worst case time complexity $O(n \log H)$ where $n$ is the size of the input set and $H$ is the size of the output set, i.e. the number ot vertices found to be on the hull. We also show that this algorithm is asymptotically worst case optimal on a rather realisic model of computation even if the complexity of the problem is measured in terms of input as well as output size. The algorithm relies on a variation of the divide-and-conquer paradigm which we call the ``marriage-before-conquest'' principle and which appears to be interesting in its own right.

- TR-83-08 A Prological Definition of HASL, a Purely Functional Language with Unification Based Expressions, January 1983 Harvey Abramson
We present a definition in Prolog of a new purely functional (applicative) language HASL ({\em HA}rvey's {\em S}tatic {\em L}anguage). HASL is a descendant of Turner's SASL and differs from the latter in several significant points: it includes Abramson's unification based conditional binding constructs; it restricts each clause in a definition of a HASL function to have the same arity, thereby complicating somewhat the compilation of clauses to combinators, but simplifying considerably the HASL reduction machine; and it includes the single element domain \{fail\} as a component of the domain of HASL data structures. It is intended to use HASL to express the functional dependencies in a translator writing system based on denotational semantics, and to study the feasibility of using HASL as a functional sublanguage of Prolog or some other logic programming language. Regarding this latter application we suggest that since a reduction mechanism exists for HASL, it may be easier to combine it with a logic programming language than it was for Robinson and Siebert to combine LISP and LOGIC into LOGLISP: in that case a fairly complex mechanism had to be invented to reduce uninterpreted LOGIC terms to LISP values. .br The defnition is divided into four parts. The first part defines the lexical structure of the language by means of a simple Definite Clause Grammar which relates character strings to ``token'' strings. The second part defines the syntactic structure of the language by means of a more complex Definite Clause Grammar and relates token strings to a parse tree. The third part is semantic in nature and translates the parse tree definitions and expressions to a variable-tree string of combinators and global names The fourth part of the definition consists of a set of Prolog predicates which specifies how strings of combinators and global names are reduced to ``values'', ie., integers, truth values, characters, lists, functions fail, and has an operational flavour: one can think of this fourth part as the definition of a normal order reduction machine.

- TR-83-09 R-Maple: A Concurrent Programming Language Based on Predicate Logic, Part I: Syntax \& Computation, January 1983 Paul J. Voda
(Abstract not available on-line)

- TR-83-10 A Fast Data Compression Method, August 1983 Samuel T. Chanson and Jee Fung Pang
This paper presents a new data compression scheme. The scheme uses both fixed and variable length codes and gives a compression ratio of about one-third for English text and program source files (without leading and trailing blank suppression). This is very respectable compared to existing schemes. The compression ratio for numbers ranges from 52\% for numbers in scientific notation to 65\% for integers. The major advantage of the scheme is its simplicity. The scheme is at least six times faster than Huffman's code and takes about half the main memory space to execute.

- TR-83-11 A Sound and Sometimes Complete Query Evaluation Algorithm for Relational Databases with Null Values, June 1983 Raymond Reiter
This paper presents a sound and, in certain cases, complete method for evaluating queries in relational databases with null values where these nulls represent existing but unknown individuals. The soundness and completeness results are proved relative to a formalization of such databases as suitable theories of first order logic.

- TR-83-12 Acceptable Numerations of Function Spaces, October 1983 K and Akira a
We study when a numeration of the set of morphisms from a numeration to the other is well-behaved. We call well-behaved numerations ``acceptable numerations''. We characterize acceptable numerations by two axioms and show that acceptable numerations are recursively isomorphic to each other. We also show that for each acceptable numeration a fixed point theorem holds. Relation between Cartesian closedness and S-m-n property is discussed in terms of acceptable numerations. As an example of acceptable numerations, we study directed indexings of effective domains.

If you have any questions or comments regarding this page please send mail to help@cs.ubc.ca.