Re: <http://www.jucs.org/jucs_10_7/total_functional_programming>
In article <7xwsq4l1gf.fsf@[EMAIL PROTECTED]
>,
Paul Rubin <http://phr.cx@[EMAIL
PROTECTED]
> wrote:
> Joachim Durchholz <jo@[EMAIL PROTECTED]
> writes:
> > > I think the idea of codata combined with totality is that a program
> > > operating on codata is guaranteed to work its way through each
element
> > > of even an infinite data stream. I.e. for any N we will eventually
> > > get to the Nth element.
> >
> > Well, sure, but being structural, this covers just all those simple
> > cases that a trivial inference system will cover. Something along the
> > lines of Hindley-Milner, for example, should fully suffice (though one
> > may have to adapt H-M to get the distinction right).
>
> Right, but one of the main points of the paper was that this is really
> enough for almost everything that's actually interesting. In
> particular the language can express any function that's provably total
> in second order arithmetic, which encomp***** just about everything in
> mathematics outside of set theory.
One interesting point which I hadn't come across before is on p 766:
| Theorem: For any language in which all programs terminate, there are
| always-terminating programs which cannot be written in it - among
| these are the interpreter for the language itself.
The proof is simple yet interesting; I'm surprised this didn't come up
in the comp theory cl***** I took.
[added comp.theory, comp.edu]
--
---------------------------
| BBB b \ Barbara at LivingHistory stop co stop uk
| B B aa rrr b |
| BBB a a r bbb | Quidquid latine dictum sit,
| B B a a r b b | altum viditur.
| BBB aa a r bbb |
-----------------------------
|
