Conversation

Notices

1. Embed this notice
   julesh (julesh@mathstodon.xyz)'s status on Wednesday, 06-Nov-2024 18:50:59 JST julesh

   Wait till people find out about computability of functions (Nat -> Nat) -> Nat, they're going to lose their shit

   • Embed this notice
     julesh (julesh@mathstodon.xyz)'s status on Wednesday, 06-Nov-2024 19:04:04 JST julesh

     in reply to

     • Nikita Lisitsa

     @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

   • Embed this notice
     Nikita Lisitsa (lisyarus@mastodon.gamedev.place)'s status on Wednesday, 06-Nov-2024 19:04:06 JST Nikita Lisitsa

     in reply to

     @julesh What do you mean?

     julesh repeated this.
   • Embed this notice
     julesh (julesh@mathstodon.xyz)'s status on Wednesday, 06-Nov-2024 19:12:31 JST julesh

     in reply to

     • Nikita Lisitsa

     @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

   • Embed this notice
     Nikita Lisitsa (lisyarus@mastodon.gamedev.place)'s status on Wednesday, 06-Nov-2024 19:12:33 JST Nikita Lisitsa

     in reply to

     @julesh Oh wow, thanks!