Exceptions Are Strictly More Powerful Than Call/CC.

Abstract

We demonstrate that in the context of statically typed pure functional lambda calculi, exceptions are strictly more powerful than call/cc. More precisely, we prove that the simply typed lambda calculus extended with exceptions is strictly more powerful than Girard's F(w), (a superset of the simply typed lambda calculus) extended with call/cc and abort. This result is established by showing that the first language is Turing equivalent while the second language permits only a subset of the recursive functions to be written. We show that the simply typed lambda calculus extended with exceptions is Turing equivalent by reducing the untyped lambda calculus to it by means of a novel method for simulating recursive types using exception-returning functions. The result concerning F(w) extended with call/cc is from a previous paper of the author and Robert Harper's.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jul 01, 1995
Accession Number
ADA307740

Entities

People

  • Mark Lillibridge

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Calculus
  • Coding
  • Computations
  • Computer Programming
  • Computer Science
  • Computers
  • Language
  • Programming Languages
  • Recursive Functions
  • Semantics
  • Simulations
  • Test And Evaluation

Readers

  • Computational Linguistics