7 ms·

Regarding 2 I think you're missing my point. Firstly, the first "property of interest" was rendered incorrectly (and also stated incorrectly). It was supposed

by tome 7y ago

Regarding 2 I think you're missing my point. Firstly, the first "property of interest" was rendered incorrectly (and also stated incorrectly). It was supposed to be > How about `bar (factorial (10^10^10^10 + 1))`? Is that `True`? Can we easily prove or disprove that property of interest? Secondly, I know the second result is true. I'm asking how you would easily prove it. How do you easily show that "forall m. bar m == True" is equivalent to Euclid's theorem?

pron 7y ago
> Can we easily prove or disprove that property of interest? Maybe we could answer that affordably, albeit with some probability, using fast probabilistic primality tests (I don't know how high they can practically go). But can we easily prove what the result of sorting a particular list with a 10^10^10 elements is? Maybe not, but I don't think it's as much a property of interest as "does this program ever crash." In other words, for every algorithm with some non-trivial complexity, the question of what the result would be for some very large input is hard to answer, but I don't think that is a common property of interest. But if I get your meaning, you are correct that sometimes, if our focus is on an algorithm rather than on a working system, we forget that all systems can, at best, be shown correct only with some probability (because the hardware only does what it's told with probability), and at some point, there are algorithmic bugs that can occur in practice with a probability that's lower than that of a hardware glitch. > How do you easily show that "forall m. bar m == True" is equivalent to Euclid's theorem? By proving that bar is, indeed, a primality test, which is not hard. I.e. you prove that bar n = TRUE iff ∀ m ∈ ℕ . 1 < m < n ⇒ n % m ≠ 0. This is usually proven by induction.

7 ms·

Regarding 2 I think you're missing my point. Firstly, the first "property of interest" was rendered incorrectly (and also stated incorrectly). It was supposed

by tome 7y ago

pron 7y ago
> Can we easily prove or disprove that property of interest? Maybe we could answer that affordably, albeit with some probability, using fast probabilistic primality tests (I don't know how high they can practically go). But can we easily prove what the result of sorting a particular list with a 10^10^10 elements is? Maybe not, but I don't think it's as much a property of interest as "does this program ever crash." In other words, for every algorithm with some non-trivial complexity, the question of what the result would be for some very large input is hard to answer, but I don't think that is a common property of interest. But if I get your meaning, you are correct that sometimes, if our focus is on an algorithm rather than on a working system, we forget that all systems can, at best, be shown correct only with some probability (because the hardware only does what it's told with probability), and at some point, there are algorithmic bugs that can occur in practice with a probability that's lower than that of a hardware glitch. > How do you easily show that "forall m. bar m == True" is equivalent to Euclid's theorem? By proving that bar is, indeed, a primality test, which is not hard. I.e. you prove that bar n = TRUE iff ∀ m ∈ ℕ . 1 < m < n ⇒ n % m ≠ 0. This is usually proven by induction.