4 ms·

How does the famous largest number contest winner loader.c fit into this? Its search for well typed programs has to be halting...

• thaliaarchi 4y ago
  I was not familiar with loader.c, so I did some digging[0]. It implements the Calculus of Constructions, which Coq is based upon, and generates all programs encoded lower than some value. The search is halting, though very long. From the analysis[1] in the contest: > {loader.c}, diagonalizes over the Huet-Coquand `calculus of constructions'. This is a highly polymorphic lambda calculus such that every well-formed term in the calculus is strongly normalizing; or, to put it another way, a relatively powerful programming language which has the property that every well-formed program in the language terminates. The program's main function is called D. … D works approximately as follows: given an argument x, it iterates over all bit strings with binary value less than or equal to x, and, if such a bit string codes for a well-formed program (`term' in lambda-calculus language), it runs the program (`strongly normalizes the term' in lambda-calculus language.) The return value of D is then obtained by packaging together the return values of all these programs. The program's return value is D@@5(99). [0]: https://googology.fandom.com/wiki/Loader%27s_number https://googology.fandom.com/wiki/Loader%27s_number [1]: http://djm.cc/bignum-results.txt http://djm.cc/bignum-results.txt