Theses & Reports

---

Instructions for submitting a technical report or thesis.

You can find technical reports published prior to 1990 archived here.

• Ph.D. Thesis 1983 A Practical Method for Lr and Ll Syntactic Error Diagnosis and Recovery Burke, Michael George Abstract | PDF

  Title: A Practical Method for Lr and Ll Syntactic Error Diagnosis and Recovery

  Candidate: Burke, Michael George

  Abstract:

  A powerful, practical, and language-independent method for diagnosing and recovering from syntactic errors within the LR and LL parsing frameworks is described. The method proceeds in three phases. The simple recovery phase attempts a single token modification of the source text, scope recovery attempts a multiple token insertion to close one or more open scopes, and secondary recovery involves a multiple deletion of tokens surrounding the error point. When the token at which the error is detected is not the token that is in error, points on the parse stack must be considered if the error is to be corrected. Condensation that has occurred on the parse stack, however, is sometimes harmful in this context. Also, in some of the parsing frameworks under consideration, unwanted condensation may occur even if the error is detected at the point at which it occurs. This problem motivates the existence of four versions of the method involving tradeoffs between the quality of error recovery and efficiency with respect to space and time. Techniques are described that make the method efficient in practice. Other implementation issues, such as language specific tuning and the issuing of diagnostic messages, are discussed. Empirical results are presented that demonstrate that the versions of the method offer choices ranging from very high quality recovery with reasonable efficiency to high quality recovery with excellent efficiency.

• Ph.D. Thesis 1983 Resolution by Unification and Equality Digricoli, Vincent Joseph Abstract | PDF

  Title: Resolution by Unification and Equality

  Candidate: Digricoli, Vincent Joseph

  Abstract:

  In resolution by unification and equality, we recast the theory of binary resolution on the basis of the properties of the equality relationship as stated by the equality axioms. In standard binary resolution as introduced by J. A. Robinson in 1965, complete and strict unification is the sole basis for resolving complementary literals leading to exceptionally long proofs for even simple theorems involving equality. In RUE resolution implicit use of the equality axioms is made through their incorporation into two rules of inference which are sound and complete to prove E-unsatisfiability. Proofs by RUE resolution are significantly shorter and more transparent than standard refutations with the equality axioms. These qualities permit more effective application of heuristics to guide the search for refutations. We here present the complete theory of RUE resolution, with proofs of lemmas and theorems in support of the theory. We define RUE hyperresolution as a restriction strategy and develop a heuristic theory to order the search for refutations. We have implemented an RUE theorem prover and performed experiments in the fields of Boolean algebra, Ring theory and Group theory. We present a careful comparison with the work of McCharen, Overbeek and Wos, whose theorem prover using unification resolution with the equality axioms and paramodulation represents one of the most successful uses of unification resolution. The comparison of results presents major evidence that RUE resolution is a significant advance over unification resolution.

• Ph.D. Thesis 1983 Measuring Setl Performance Shields, Lynwood David Abstract | PDF

  Title: Measuring Setl Performance

  Candidate: Shields, Lynwood David

  Advisor(s): Schwartz, Jacob T.

  Abstract:

  Current computer technology is being driven by the hardware advances that have provided a constant and dramatic decrease in the cost of elementary hardware operations. This has made more feasible the use of high-level languages that permit program development without the constant attention to detail needed to achieve efficient execution that characterizes low-level languages; indeed, such languages can be realized by a combination of microcode and special-purpose VLSI chips. However, effective use of this technology requires an understanding of the underlying performance issues. We have analyzed the problem of measuring performance of high-level languages by studying in detail one such language, SETL, and have developed a set of measurement tools addressed both to the user and the implementor. Our thesis is that such measurement efforts must aim to provide measurement tools that can be integrated into the system, but only after their efficacy has been demonstrated by their use on real programs. This work has resulted in prototype versions of four program profilers, each providing a specific view of SETL performance; we discuss their use in analyzing, and then improving, the performance of actual SETL programs. We also discuss the implementation of the hard code system that provides an essential starting point for evaluating the effectiveness of the representation sublanguage provided by SETL. Finally, we indicate some ways in which SETL performance can be improved.

• Ph.D. Thesis 1983 Undecidable Complexity Statements in a Hierarchy of Extensions of Primitive Recursive Arithmetic Sigal, Ron Mark Abstract | PDF

  Title: Undecidable Complexity Statements in a Hierarchy of Extensions of Primitive Recursive Arithmetic

  Candidate: Sigal, Ron Mark

  Advisor(s): Weyuker, Elaine; Davis, Martin D.

  Abstract:

  For each transfinite ordinal (alpha) (LESSTHEQ) (epsilon)(,0), we fix a unique well-ordering of the natural numbers which we call its canonical well-ordering. Let S((alpha)) be Primitive Recursive Arithmetic plus function definition by transfinite recursion on the canonical well-ordering of order type (alpha). For a hierarchy of theories S((alpha)), where (omega)('(omega)('(omega))) (LESSTHEQ) (alpha) < (epsilon)(,0), we define functions (phi)(,(alpha)) such that statements asserting extremely loose upper bounds on the computational complexity of (phi)(,(alpha)) are independent of S((alpha)). We quantify the gap between actual and provable complexity bounds in terms of the Lob-Wainer hierarchy of rapidly growing functions. A statement asserting a primitive recursive upper bound for the complexity of (phi)(,(alpha)) can be proven in a theory slightly higher in the hierarchy than S((alpha)).

• Ph.D. Thesis 1983 Formal Languages with Oracles Weixelbaum, Elia S. Abstract | PDF

  Title: Formal Languages with Oracles

  Candidate: Weixelbaum, Elia S.

  Abstract:

  A relativization of formal language theory is studied in this dissertation. Specifically, we examine possible relativizations of the four language classes of the Chomsky hierarchy. Definitions are given for oracle finite automata, oracle pushdown automata, oracle linear bounded automata, and oracle Turing machines. The relativized regular languages are characterized via results derived from AFL (abstract families of languages) theory. We then use this characterization to help us derive a relativization of the Chomsky-Schutzenberger theorem for relativized context free languages. We examine relativized recursively enumerable (r.e.) languages by studying oracle Turing machines and also by suggesting a definition for an oracle phrase structure grammar. We demonstrate two different types of equivalences between these two models. The context sensitive languages are relativized in the same manner as are the r.e. languages, although there are difficulties in proving the respective results for the context sensitive case. Several unresolved questions remain in this case.