Viewing profile — cofunctor

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 …

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…

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 alg…

This ought to work with any lazy language (or lazy data structure), which is one of the huge benefits of laziness for FP.

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 understandin…