Recent searches
Search options
Wait till people find out about computability of functions (Nat -> Nat) -> Nat, they're going to lose their shit
@julesh What do you mean?
@lisyarus Turing completeness is the empirically unique reasonable notion of computability for functions Nat -> Nat, but for (Nat -> Nat) -> Nat (aka type-2 computability) there are multiple reasonable notions of computation that are not equivalent, so there is no such thing as “Turing completeness” there
@julesh Oh wow, thanks!
@lisyarus Specifically, very subtle things happen with the difference between computable functions {computable functions Nat -> Nat} -> Nat and computable functions {all functions Nat -> Nat} -> Nat. If I remember correctly there exist Haskell functions which are total for every Haskell-definable input, but would not terminate if you gave it an oracle for a noncomputable input
@julesh @lisyarus How does this relate to Turing Degrees in computability theory?
Those are really (nat -> nat) -> nat -> nat, and the question is about how changing the power of the first input impacts what the resulting nat -> nat function can compute. It seems related, but I'm not familiar with how.