cofunctor

6 ms·

1. 1.▲
   by cofunctor 7mo ago

   Such an algorithm would be computing the (uncomputable) function BB : Nat -> Nat, and not the computability of a given BB(n) . Every fixed natural number is computable: just print out the number. This is a subtlety of doing computabilit
2. 2.▲
   by cofunctor 7mo ago

   Here’s a nice concrete construction. To start, fix some enumeration ϕ of Turing machines. Let’s define a sequence of rational numbers x_k as $\sum_{i=0}^k 2^{-(i+1)} * halts(ϕ(i),k)$, where $halts(M,k)$ returns 1 if the machine M halts befo
3. 3.▲
   by cofunctor 7mo ago

   One nice way of seeing the inevitability of the complex numbers is to view them as a metric completion of an algebraic closure rather than a closure of a completion. Taking the algebraic closure of Q gives us algebraic numbers, which are a
4. 4.▲
   by cofunctor 7y ago

   This ought to work with any lazy language (or lazy data structure), which is one of the huge benefits of laziness for FP.
5. 5.▲
   by cofunctor 7y ago

   In some sense it does though. Type Theories (and their associated pure FP languages) often have the exact same algebraic structure as different classes of logic. To my understanding, JML uses Hoare Logic, which is a great tool for proving c