Skip to main content Accessibility help

We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.

Close cookie message
×
  1. Home
  2. Browse subjects
  3. Computer Science
  4. Programming Languages and Applied Logic
  5. Content listing

Refine search

Refine search

Access:
Content type:
Publication date:
Apply   From and To filters
Subject: Show more
Journals Show more
Publishers: Show more
Societies Show more
Series: Show more
Collections: Show more

Actions for selected content:

Select all | Deselect all
  • View selected items
  • Export citations
  • Download PDF (zip)
  • Save to Kindle
  • Save to Dropbox
  • Save to Google Drive

Save Search

You can save your searches here and later view and run them again in "My saved searches".

Please provide a title, maximum of 40 characters.
Cancel
×

5646 results in Programming Languages and Applied Logic

Page 159 of 283

  • Appendix A3 - Strong normalization proofs

  • J. Roger Hindley, University of Wales, Swansea, Jonathan P. Seldin, University of Lethbridge, Alberta
  • Book:
    Lambda-Calculus and Combinators
    Published online:
    05 June 2012
    Print publication:
    24 July 2008, pp 293-304

  • Summary

    As we have seen in Chapter 10, the main property of typed systems not possessed by untyped systems is that all reductions are finite, and hence every typed term has a normal form. In this appendix we shall prove this theorem for the simply typed systems in Chapter 10, and for an extended system from which the consistency of first-order arithmetic can be deduced.

    The proofs will be variations on a method due to W. Tait, [Tai67]. (See also [TS00, Sections 6.8, 6.12.2] or [SU06, Sections 5.3.2–5.3.6].) Simpler methods are known for pure λ and CL, but Tait's is the easiest to extend to more complex type-systems.

    We begin with two definitions which have meaning for any reduction concept defined by sequences of replacements. The first is a repetition of Definition 10.14. The second is the key to Tait's method.

    Definition A3.1 (Normalizable terms) A typed or untyped CL-or λ-term X is called normalizable or weakly normalizable or WN with respect to a given reduction concept, iff it reduces to a normal form. It is called strongly normalizable (SN) iff all reductions starting at X are finite.

    As noted in Chapter 10, SN implies WN. Also the concept of SN involves the distinction between finite and infinite reductions, whereas WN does not, so SN is a fundamentally more complex concept than WN.

  • 4 - Representing the computable functions

  • J. Roger Hindley, University of Wales, Swansea, Jonathan P. Seldin, University of Lethbridge, Alberta
  • Book:
    Lambda-Calculus and Combinators
    Published online:
    05 June 2012
    Print publication:
    24 July 2008, pp 47-62

  • Summary

    Introduction

    In this chapter, a sequence of pure terms will be chosen to represent the natural numbers. It is then reasonable to expect that some of the other terms will represent functions of natural numbers, in some sense. This sense will be defined precisely below. The functions so representable will turn out to be exactly those computable by Turing machines.

    In the 1930s, three concepts of computability arose independently: ‘Turing-computable function’, ‘recursive function’ and ‘λ-definable function’. The inventors of these three concepts soon discovered that all three gave the same set of functions. Most logicians took this as strong evidence that the informal notion of ‘computable function’ had been captured exactly by these three formally-defined concepts.

    Here we shall look at the recursive functions, and prove that all these functions can be represented in λ and CL. (We shall not work with the Turing-computable functions because their representability-proof is longer.)

    An outline definition of the recursive functions will be given here; more details and background can be found in many textbooks on computability or textbooks on logic which include computability, for example [Coh87], [Men97] or the old but thorough [Kle52].

    Notation 4.1 This chapter is written in the same neutral notation as the last one, and its results will hold for both λ and CL unless explicitly stated otherwise.

Page 159 of 283