What is the mathematical significance of "all (==1) [1,1..]" not terminating?
<p>Intuitively, I would expect the "mathematical" answer to <code>all (==1) [1,1..]</code> to be <code>True</code> because all of the elements in a list that only contains 1s are equal to 1. However I understand that "computationally", the process of evaluating the infinite list in order to check that each element does in fact equal 1 will never terminate, therefore the expression instead "evaluates" to bottom or <code>⊥</code>. </p>

<p>I find this result counter-intuitive and a little unnerving. I think the fact that the list is an infinite one confuses the issue both mathematically and computationally, and I would love to hear from anyone who has some insight and experience in this area</p>

<p>My question is, which is the most mathematically correct answer? <code>⊥</code> or <code>True</code>?
Some elaboration as to why one answer is more correct than the other would also be much appreciated. </p>

<p>edit: This might indirectly have something to do with the <a href="https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence">Curry-Howard isomorphism</a> (Programs are proofs and types are theorems) and <a href="https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems">Gödel's incompleteness theorems</a>. If I remember correctly, one of the incompleteness theorems can be <em>(incredibly roughly)</em> summarised as saying that "sufficiently powerful formal systems (like mathematics or a programming language) cannot prove all true statements that can be expressed in the system"</p>