3 ms·
> How does a computer help when you have conjectures involving infinite mathematical structures or extremely large numbers? Basically, you hop up a level (go m
by xyzzy123 14y ago
> How does a computer help when you have conjectures involving infinite mathematical structures or extremely large numbers?
Basically, you hop up a level (go meta). Instead of working with the extremely large numbers or sets, you symbolically manipulate statements about them.
- gems 14y agoGive me an example of how this is done or can be done.
- sharkbot 14y agoCheck out Adam Chlipala's Coq tutorial, specifically the section on infinite proofs: http://adam.chlipala.net/cpdt/html/Coinductive.html http://adam.chlipala.net/cpdt/html/Coinductive.html I'll repeat what szany and xyzzy123 mentioned: you work at a level of abstraction where infinite data structures are represented symbolically with enough definitional scaffolding to allow proofs to go through. In a sense, a properly typed program provides a proof of some theorem over infinite data structures. For instance, an instance of a tree (in generic Java) is usually a finite data structure, but the set of all trees representable in Java is infinite. (Handwaving begins) The types prove that certain operations can't happen, like a tree of Strings changing to a tree of Arrays by a node search algorithm, which is a proof about an infinite set.