Re: [Qi] Fwd: book deal goes through with printer

["Kyle R. Burton" <kyle.burton@gmail.com>]

> Lately I've been reading a bunch of papers about languages that go in
> the other direction, and which aren't subject to the halting problem
> at all.

Come on, do you have links or at least pointers to more information?

> This turns out to be unexpectedly useful.

I'll bet!

> Such languages can't express every possible algorithm, but it's not
> that important, because in typical programming contexts we only write
> functions that are guaranteed to halt anyway; this is the usual
> definition of "algorithm".

Right, in most cases it's fine.  I find myself creating DSLs for users
that can't express every possible algorithm - but it makes for more
guarantees about the system, which better serves the users.

> One example is the paper "Total Functional Programming", by D. A. Turner.
> http://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf

> Turner's initial point is that the presence of _|_ values in languages
> like Haskell spoils one's ability to reason from the program
> specification.  His basic example is simple:
>
>        loop :: Integer -> Integer
>        loop x = 1 + loop x
>
> Taking the function definition as an equation, we subtract (loop x)
> from both sides and get
>
>        0 = 1
>
> which is wrong.  The problem is that while subtracting (loop x) from
> both sides is valid reasoning over the integers, it's not valid over
> the Haskell Integer type, because Integer contains a _|_ value for
> which that law doesn't hold: 1 /= 0, but 1 + _|_ == 0 + _|_.
>
> Before you can use reasoning as simple and as familiar as subtracting
> an expression from both sides, you first have to prove that the value
> of the expression you're subtracting is not _|_.
>
> By banishing nonterminating functions, one also banishes _|_ values,
> and familiar mathematical reasoning is rescued.

I think I kinda get this...

> Also:
>
>        http://en.wikipedia.org/wiki/Total_functional_programming

"For example, any algorithm which has had an asymptotic upper bound
calculated for it can be trivially transformed into a
provably-terminating function by using the upper bound as an extra
argument which is decremented upon each iteration or recursion"

is an interesting insight.

> Sorry, that turned out to be a much longer digression than I expected.
> I did not mean to distract attention from Qi.

This is exactly the kind of discussion I have been looking for from
Philly Lambda.

> I wish Professor tarver had not written his web pages in white text on
> a black background.

Yes :)


Thanks for the discussion.

Kyle