Long time reader, first time commenter (although I might have left some other comments here a couple years ago under a pseudonym). I work in tech but I’ve always been really interested in theoretical computer science. I’ve also come to appreciate and value the general “life advice” you dispense here to your blog readers and others who need help. I apologize if this comment is horribly off-topic, but I’m seeking some advice or guidance about a stressful situation I’m in, and I want to know if I’m in the wrong or not. In my defense, this post is at least somewhat about family life and vacations—and I’m on a family vacation right now that’s left one of my children in tears.

So here’s the situation: I’m posting here because I need some outside perspective on a situation that has been causing a lot of tension in my family. I’m currently on a family vacation (at a big tropical resort hotel) with my five children and my wife, Emily. My oldest son, James (who’s 23), and my daughters, Lily (21), Emma (20), and Sophie (18) all came with us, along with our youngest daughter, Ava (16).

The problem is that my older kids and my wife love to go out to bars and clubs, and they spend most of their time drinking and partying. I personally love clubbing and going to bars, and I don’t have any issue with them doing so responsibly (the resort is international so Sophie can drink). However, my youngest daughter is obviously too young to drink, so we got an activity packet from the resort director that was supposed to give her things to do at the hotel. It was full of word searches, mazes, crosswords, connect the dots, and other fun activities, and it was all tropical themed.

The problem is that Ava was really upset that she was left alone most of the time while we were all out having fun. She tried to do some of the activities in the packet, but she quickly got bored and felt really lonely. She even asked me to take her out with us a few times, but I told her that she was too young and that we would be going to places that were not appropriate for her.

Now, Ava is really upset with me and my older kids. She’s been crying a lot and saying that we don’t care about her. I understand why she feels this way, but at the same time, I don’t think it’s fair for us to completely change our plans and not have any adult time just because she’s too young to participate.

]]>Using a strongly normalizing type system is a good approach to making all

computations halt, but the simply typed lambda calculus seems a relatively weak

choice. A seemingly much better choice is the Calculus of Constructions, a type

theory created by by Thierry Coquand.

This allows one for instance to still find a typed version of the 63 bit lambda term

whose output exceeds Graham’s Number.

The typing does cost a fair number of extra bits though. Instead of the lambda term

let { 2 = \f\x.f (f x); H = \h\f\n.n h f n } in 2 2 H 2 2 2,

the CoC version looks roughly like

let { 2 = λA:*λf:A->A.λx:A.f (f x) : nat = ΠA:*.(A->A)->A->A; 2′ =

λn:natλA:*λf:(A->A).n A (n A f) : nat->nat;

H = λh:((nat->nat)->nat->nat)λf:(nat->nat)λn:nat.n (nat->nat) h f n :

((nat->nat)->nat->nat)->(nat->nat)->nat->nat;

N = 2 (nat->nat) (2 ((nat->nat)->nat->nat) H (2 nat)) 2′ 2 : nat } in N.

Note that the CoC takes center stage in the definition of Loader’s Number,

which is about the largest number ever defined in a way that is computable.

Vaclav #77

While the notion of colors or tape symbols makes no sense for lambda calculus,

it’s quite possible to define oracle versions, for example by letting

out-of-bound de-Bruijn indices refer to oracle combinators as discussed in

https://cp4space.hatsya.com/2013/01/06/fast-growing-4/

A lambda term t that’s not closed, like (1 (λ 1)) of size 8 bits, would then be

interpreted as (λ (1 (λ 1))) Ω_{1} where Ω_{1} is a halting

oracle of rank 1. That halting oracle then gets applied to the identity (λ 1)

(which is oracle free as required by this oracle being of rank only 1) and

returns true (λ λ 2) since identity has a normal form.

F3et #78

While no small TM has been defined to calculate a function with growth rate epsilon0 in the FGH,

we were able to define such a function in under 80 bits (10 bytes) of Binary Lambda Calculus

https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/E0.lam

https://content.wolfram.com/uploads/sites/13/2018/02/07-6-2.pdf

]]>Thanks for the interesting thoughts!

The context is Geoffrey Irving #24 asking: how many (correct) papers of the form “BB(n) is independent of ZFC, beating the previous record” that there will ever be?

Then my interpretation for « BB(n) is independent of ZF » was « There’s a TM of size n that halts iff ZF inconsistent », and my question was like « Is there a TM of size n that halts iff there’s a TM of size n that halts iff ZF inconsistent ».

At first I thought we could exclude that by pigeonhole principle… but maybe one can show the same TM actually proves both. 🤔

]]>I think BB(10, 2) is much bigger than f_epsilon0(100,000,000)

.

On the site googology wiki were posted (many years ago) 2 constructed machines BB(36,3) and BB (37,3) by user Wyhhagoras. The first BB more than f_epsilon0(5) and the second BB >f_epsilon0(374676378).

It doesn’t matter that these machines have order 40 states and 3 colors.

They are man-made and therefore completely sub-optimal.

Real champions for BB(36,3) and BB (37,3) are incomparably more f_epsilon0 in a FGH.

It is important that it is enough to add 1 state to the BB to get f_epsilon0(400,000,000) instead of f_epsilon0(5).

So we have BB (5,2) = several thousands, and BB (6,2) order 2 arrows in Knuth notation. Then let x be a machine with an f_epsilon0(n) of the order n=3-4-5 or so, and a machine x+1 = f_epsilon0(n) of the order of hundreds millions.

I think between BB (6) and BB(x) is a maximum of a couple of BBs. That is, BB (9) has a theme of the order of f_epsilon0(5) and BB(10) of the order of f_epsilon0(100,000,000) or much bigger.

The above is my guess.

But BB (50,2) is incomparably more f_epsilon0(n), of that I have no doubt.

#include

#include

#include

#include

#include

#include

#include

#include

std::vector findTuring(long long n) {

std::vector tape;

for (long long i = 1; i * i <= n; i++) {

if (n % i == 0) {

tape.push_back(i);

if (i * i != n)

tape.push_back(n / i);

}

}

return tape;

}

std::string recursivePrint(std::vector input) {

if (input.empty()) return “”;

std::ostringstream os;

os << input.back() << ", ";

input.pop_back();

return recursivePrint(input) + os.str();

}

void BusyBeaver(std::vector input) {

std::srand(std::time(nullptr));

std::vector firstVector(input.size()), secondVector(input.size());

std::vector<std::vector> sumMatrix(input.size(), std::vector(input.size()));

std::generate(firstVector.begin(), firstVector.end(), std::rand);

std::generate(secondVector.begin(), secondVector.end(), std::rand);

std::random_shuffle(firstVector.begin(), firstVector.end());

std::random_shuffle(secondVector.begin(), secondVector.end());

for(long long i = 0; i < input.size(); i++){

for(long long j = 0; j < input.size(); j++){

sumMatrix[i][j] = firstVector[i] + secondVector[j];

findTuring[j];

}

}

std::map complicatedMapping;

for(long long number: input){

for(long long i = 0; i < input.size(); i++){

for(long long j = 0; j < input.size(); j++){

if(sumMatrix[i][j] == number){

complicatedMapping[number] = std::to_string(i) + " " + std::to_string(j);

break;

}

}

}

}

std::vector sequence;

for(long long number: input){

sequence.push_back(complicatedMapping[number]);

}

std::sort(sequence.begin(), sequence.end());

long long sum = 0;

for(long long number: input){

sum += number;

}

std::string encodedSum = “”;

for(char digit: std::to_string(sum)){

encodedSum += std::to_string((digit – ‘0’ + 1) % 10);

}

std::map<std::string, std::vector> reversedMapping;

for(auto &pair: complicatedMapping){

reversedMapping[pair.second].push_back(pair.first);

}

for(auto &pair: reversedMapping){

long long localSum = 0;

for(long long number: pair.second){

localSum += number;

}

long long localProduct = 1;

for(long long number: pair.second){

localProduct *= number;

}

std::cout << "For indices: " << pair.first << " sum is: " << localSum << " product is: " << localProduct << "\n";

std::cout << "Factors of local sum are: " << recursivePrint(findFactors(localSum)) << "\n";

std::cout << "Factors of local product are: " << recursivePrint(findFactors(localProduct)) << "\n";

}

std::cout << "The sum of the input vector is: " << encodedSum << "\n";

}

int main() {

std::vector testInput {1, 2, 3, 4, 5, 7, 8, 9, 10, 11, 12};

BusyBeaver(testInput);

return 0;

}