Subject: lillibridge, strong termination, exceptions
From: Johan Ovlinger (firstname.lastname@example.org)
Date: Mon Feb 04 2002 - 23:49:48 EST
It's all Matthias's fault (betcha never heard that before)!
Anyway, He mentioned Mark Lillibridge, whose Thesis I read many moons
ago (and was very jealous). So on a lark I checked out his homepage at
dig^h^h^h compaq SRC (birthplace of Modula-3, coincidentally (?)).
The following abstract (from his pubs) is pertinent to our discussion
about strong normalisation this afternoon:
More precisely, we prove that a natural extension of the
simply-typed lambda calculus with unchecked exceptions is strictly
more powerful than all known sound extensions of Girard's F-omega (a
superset of the simply-typed lambda calculus) with call/cc.
This result is established by showing that the first language is
Turing complete while the later languages permit only a subset of
the recursive functions to be written.
This suprised me. Adding exceptions to the STLC makes it turing
complete! If only I didn't have a thesis proposal to write...
This archive was generated by hypermail 2b28 : Mon Feb 04 2002 - 23:49:50 EST