Next wednesday as part of World Logic Day, Swansea CS will have an event with three talks:
"Provably Total NP Search Problems of Bounded Arithmetic and beyond" by Arnold Beckmann
"Non-strictly Positive Induction for Extracting Breadth-first Search" by Ulrich Berger and
"The History of Computability Theory and its Impact" by John Tucker.

You can attend via zoom by registering at https://sites.google.com/view/swanseaworldlogicday2026/home

#logic #computability

Some AI Systems May Be Impossible to Compute

https://spectrum.ieee.org/deep-neural-network

The limits of our current approach to AI. The halting problem in the context of neural networks.

#AI #computability

I've been thinking about something that's related to Tarski's undefinability theorem (and might possibly be a corollary if viewed from the right angle), but relates to computability rather than truth. It seems to have implications for systems like Agda and Rocq, which I don't have much experience with, but which I think will (at least with certain settings) only let you define computable things. I'd love to know if this is well-known already.

Suppose you have a system, S, that lets you encode (as natural numbers) definitions of computable functions from Nat to Bool. Not every natural number has to represent such a function, but given any natural number, n, you have to be able to tell whether n is the encoding of such a function, and if it is, you have to be able to evaluate it for any natural number you want.

Now we can define a function f that takes a natural number n as input, and returns a boolean value which is True if and only if n is the encoding (in S) of a computable function g from Nat to Bool, and g(n) = False.

By the constraints I described for S, this must be a computable function. So can it be encoded in S?

No! If it could be encoded as a natural number k, then f(k) would be True if and only if f(k) = False.

So Agda, for example, with settings that allow only definitions of computable things, can't allow definitions of all computable functions. In particular, it seems it can't implement a complete simulation of Agda with the same settings.

This is almost the opposite of the problem with the halting problem. A universal Turing machine can simulate a universal Turing machine, but it can't always tell if it will halt if given certain input. Agda can guarantee that any algorithm you write in it will halt, but, if my reasoning above is correct, it can't simulate itself.

So what other computable functions might not be definable in Agda? What obstacles would you find, for example, if you tried to simulate Agda in Agda?

#Agda #Rocq #computability #logic

Shakespeare: What's in a name?
Computable analysts: Exactly one real number

#computability #complexity

🧵 Alan Turing showed that not everything logically definable is also computable.

Using a diagonalization method like Cantor’s, we can build a set D:
the set of Turing machine codes that don’t belong to their own halting set.

🔁 Here’s the twist:
No Turing machine can generate D without causing a contradiction.

#Turing #computability

1/🧵

Thanks to the work of @mspstrath all the TYPES 2025 talks are available (including mine)
Update: as fred points out the playlist was not supposed to be public yet, so, er watch this space

https://www.youtube.com/watch?v=W-lYwG3E_x4&

Like comment and subscribe, ring the bell, all that stuff

#categorytheory #computability

As promised. Here is the sequel to my Weihrauch reductions are Containers post, this time relating strong reductions to dependent adaptors. Enjoy!

https://www.countingishard.org/blog/strong-reducibility-as-an-adaptor

#categorytheory #computability

I've written up a draft post about strong weihrauch reducibility from the containers POV written. Will have the full version up in a couple of days once I've let it breathe.

#categorytheory #computability