[TYPES] Implementing induction principles

[Andreas Abel]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Dear Patricia,

concerning 3., you might be interested in Scott and Okada's paper

  A Note on Rewriting Theory for the Uniqueness of Iteration

They prove that uniqueness of primitive recursion destroys decidability.

Cheers,
Andreas

Patricia Johann wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 
> Dear Types,
> 
> I'm trying to implement the induction principle for the natural numbers.
> 
> Briefly, given P: Nat -> * and
> 
> u: P(0)
> v: forall n:Nat. Pn -> P(n+1)
> 
> I can bundle these together to form a 1+_-algebra on the type Sigma n:Nat. 
> P n, i.e., a function
> 
> my_algebra  : (1 + Sigma n:Nat. P n) -> Sigma n:Nat. P n
> my_algebra = [ (0,u), \(n,p) -> (n+1, v n p)]
> 
> Then I can write
> 
> ind P :: forall n:Nat. P n
> ind P n = p where (m,p) = iterate my_algebra n
> 
> To show that this is correct, I need to show that n=m. This is easily done 
> using the uniqueness of the iteration operator.
> 
> Here are my questions:
> 
> 1. Can I implement ind in a programming language, theorem prover or 
> intensional type theory where the uniqueness of the iteration operator is 
> not available? Maybe this can be done because I only need to know that 
> projection after a specific iterator is the identity. Or maybe there is a 
> different approach to implementing ind?
> 
> 2. Is there a programming language or theorem prover where the uniqueness 
> of the iteration operator can be used?
> 
> 3. Or are there theoretical reasons (perhaps due to undecidability of type 
> checking) why this is not possible?
> 
> Thanks very much in advance,
> -patty
> 


- --
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFKP5RtPMHaDxpUpLMRAiRyAJ9Qzvphdo/IFUJwZRPpZSBsLohCsQCePdP2
g2ECXW9blh0gocV8NOhwEQ4=
=P8so
-----END PGP SIGNATURE-----