Skip to main content
2 of 3
added 4 characters in body
John Tromp
  • 1.7k
  • 9
  • 15

May I suggest the use of Binary Lambda Calculus [1] for writing programs and measuring their size in bits?

There are many BLC programs of only a few dozen bits, comparable in complexity to 5 state TMs that need nearly 50 bits to describe, whose halting behavior is unknown.

Beyond that, there are programs like this 215 bit one for computing Laver tables [2], whose halting behavior is related to existence of large cardinals. A counterexample to Goldbach's conjecture can be found with a 267 bit program.

[1] https://tromp.github.io/cl/Binary_lambda_calculus.html

[2] https://codegolf.stackexchange.com/questions/79620/laver-table-computations-and-an-algorithm-that-is-not-known-to-terminate-in-zfc

John Tromp
  • 1.7k
  • 9
  • 15