University of Tasmania
whole_WrightDavidAmson1993_thesis.pdf (9.29 MB)

Reduction types and intensionality in the lambda-calculus

Download (9.29 MB)
posted on 2023-05-27, 14:52 authored by Wright, David Amson
In this thesis I introduce a new approach to the automated analysis of the reduction behaviour of A-calculus terms. This new approach improves on earlier analysers in several ways, not least in its treatment of higher-order terms and polymorphism, two notably troublesome issues. In addition, this thesis introduces a stronger notion of reduction behaviour than strictness. This concept, called strong head neededness, forms the basis for a new notation for describing the reduction behaviour of terms. This notation is a kind of type, elements of which are built using a Boolean algebra of function type constructors. Thus the form of the methodology proposed is that of a type system. Consideration is given to a variety of type assignment systems for the new type system. This supports the hypothesis that the approach proposed is suitable as a framework for building a range of analyses. Having established this framework it is then a matter of engineering to determine the appropriate trade off between information derived and performance achieved. An investigation is conducted into the formal semantics of all the constructs introduced. In particular, the investigation proves a range of soundness and completeness results. Also examined is the semantics of the new notion of type and the development of a model for reduction types. The model is of interest in its own right, as it gives further insight into the reduction behaviour of A-terms. The thesis includes detailed implementations of all the type assignment systems and ascertains the correctness of these implementations.


Publication status

  • Unpublished

Rights statement

Copyright 1992 the Author - The University is continuing to endeavour to trace the copyright owner(s) and in the meantime this item has been reproduced here in good faith. We would be pleased to hear from the copyright owner(s). Thesis (Ph.D.)--University of Tasmania, 1993. Includes bibliographical references (p. [202]-207)

Repository Status

  • Restricted

Usage metrics

    Thesis collection


    No categories selected


    Ref. manager