On Thu, 2009-02-19 at 05:53 -0800, Kim-Ee Yeoh wrote: > There's a lot to chew on (thank you!), but I'll just take something > I can handle for now. > > > Dan Doel wrote: > > > > An existential: > > > > exists a:T. P(a) > > > > is a pair of some a with type T and a proof that a satisfies P (which has > > type > > P(a)). In Haskell, T is some kind, and P(a) is some type making use of a. > > That > > doesn't mean that there is only one a:T for which P is satisfied. But it > > *does* mean that for any particular proof of exists a:T. P(a), only one > > a:T is > > involved. So if you can open that proof, then you know that that is the > > particular a you're dealing with, which leads to the problems in the > > grandparent. > > > > re: Constructivity and the opening of a proof > > A form of the theorem that the primes are infinite goes > "Given a finite set of primes, there's a prime bigger than any of them." > > The usual proof is constructive since factorization is algorithmic, > but I don't see why a priori, applications of this theorem on a given input > should always yield the same prime when more than one factor exists.
They don't. Any particular constructive proof will yield a particular new bigger prime, but they don't have to yield the same one. Let's choose a simpler example: There exists an Integer. Any (constructive) proof of that proposition is just an Integer and thus certainly a particular Integer. However, there is nothing special about any particular Integer. > Is non-deterministic choice forbidden in constructive math? A cursory > google seems to suggest that if not, it's at least a bĂȘte noire to some. Not particularly, but if you ultimately want an executable algorithm, you are sooner or later going to have to spell out how such a non-deterministic choice is made. -Proof-search-, though, is usually quite non-deterministic. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe