[Agda] termination

[Jesper Louis Andersen]

On Thu, Mar 3, 2011 at 15:18, James McKinna <james.mckinna at cs.ru.nl> wrote:
> Dear All,
>
> I join this thread rather late in the day, so let me back up to Conor's
> suggestion to use add-with-carry.

Let me put forth a completely different but likewise observation where
added information in the output yields easier "proofs" because the
extra information carried is crucial.

Take yer standard Fibonacci function, fib(n). Now suppose we want to
run it in *reverse* that is run it from the output to the input. This
is in general impossible, because if fib(n) = 1, we don't know which
of the numbers in the sequence

0,1,1,2,3,5,8,13,... we came from, in particular if n is 1 or 2
(counting from 0). If we on the other hand alter its output, so it
outputs the pair (fib(n), fib(n+1)) then it is obviously possible to
reverse the function: The added information is enough to provide the
bijection.

A contrived example perhaps, but nevertheless, it provides another
nail for the coffin to imprison the vampire.


-- 
J.