[Prev][Next][Index][Thread]
The relationship between exceptions and call/cc
The following Tech Report is now available by anonymous ftp:
"Exceptions are Strictly More Powerful Than Call/CC"
by: Mark Lillibridge, Carnegie Mellon University
URL: ftp://reports.adm.cs.cmu.edu/usr/anon/1995/CMU-CS-95-178.ps
ftp-server: reports.adm.cs.cmu.edu
directory: /usr/anon/1995
file: CMU-CS-95-178.ps
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-omega
(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-omega extended with call/cc is from a previous paper of the
author and Robert Harper's.