11:25 pm, 12 Nov 03

### all i have to talk about is schoolwork these days

Man, this is ugly. Multiplication is implemented recursively as repeated addition, then exponentiation on top of that as repeated multiplication. But it works! And type-checks! Give it two integers and it gives you n^m.

Sadly, recursive functions mean that it's no longer guaranteed to terminate.

(fn n:int. (rec pwr:int->int m. (if m > 0 then (rec mul:int->int y. (if y > 0 then n+(mul (y + (-1))) else 0) ) (pwr (m + (-1))) else 1 ) ) )I was about to rewrite in in Python just for fun, but then I realized you can't (?) make recursive functions with Python lambdas.

billemonWhat's scary is that by messing with recursion you can have addition, multiplication, exponentiation and then carry on .. is there even a name for what happens after exponentiation?

conjectureevanA simple infinite loop using the above syntax is

(rec f:int->int. f x) 1(That is, define f(x) to be running f(x), and then call it with some integer.)

My exponentiation function probably terminates, though... maybe some creative overflowing of integers could work around that? (To be clear: the termination proof, from before recursion, showed that no matter what the functions did, they had to terminate. So I suppose tricks like overflow are a valid way of trying to break that-- they still would terminate.)

(I'm not completely solid on this stuff yet so I apologize if I get any of it wrong.)

conjectureconjectureHere's what the pwr function boils down to, right?

pwr n m = mul (n) (pwr (n) (m - 1))

And here's the muliplication function:

mul n m = n + mul (n) (m - 1)

To prove pwr terminates, you should also prove mul terminates.

here's your base cases:

For m = 0:

mult n 0 = 0

pwr n 0 = 1

Which trivially terminate. As long as m converges to 0, then the functions should terminate, no?

Strong induction sez: If we assume these two functions terminate for all 0 <= m <= k, then if we prove they terminate for m = k + 1, we know it terminates for all m.

Let's prove mul terminates first with m = k+1:

mul n (k + 1) = n + mul (n) (k + 1 - 1)

-> reduces to mul n (k + 1) = n + mul (n) (k)

But, we know "mul (n) (k)" terminates (by our assumption), and n + (value) terminates, therefore "mul n (k + 1)" terminates! excellent.

So, substitute (k + 1) for m in the pwr function:

pwr n (k + 1) = mul (n) (pwr (n)(k + 1 - 1))

-> mul (n) (pwr (n)(k))

|__________|--> this terminates by our assumption.

and "mul (n) (value)" terminates for all values >= 0 because we just proved it. So "pwr (n) (k + 1)" terminates. Therefore, pwr (n, m) terminates for all m.