3 ms·
Give me an example of how this is done or can be done.
by gems 14y ago
Give 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.