I'm going to try to create function which outgrows Goucher's Xi function. As for now, I have an idea of getting on par with Xi.


I think most of us heard about Brainf*ck. But instead of standard rules, I'm going to use following variant - machine has right-side infinite memory tape with data pointer starting on its left end. If pointer moves out of tape, program halts immediately. Program tape has same shape and has following symbols allowed:

  • (blank) - standard blank character, ignored by program
  • > - move data pointer right
  • < - move data pointer left
  • + - cycle through symbols under data pointer (explained below)
  • [ - jump to after matching ] if data pointer is over blank cell
  • ] - return to matching [ if data pointer is over non-blank cell
  • # - unconditional halt

Although we can allow infinite programs, we will concern only finite ones. If program enters infinite string of blanks, it halts immediately, so it works like standard EOF. Now, memory tape is identified with input. Set of memory tape characters is same as program tape ones. We cycle them in order shown above. I think this isn't hard to see that we can emulate Turing machine with all this stuff (compare with Brainf*ck F by r.e.s.), so it is bounded by \(\omega_1^\text{CK}\)

Output definition

I also wanted to define output value - we don't have output tape, so we will do something else. Halting of a program is called effective if it halts due to hitting # on program tape. If program halts due to EOF, running out of memory tape or hitting non-well formed brackets in ill written program we call this halt ineffective. If program halts effectively it is equal to returning "true" or "yes" in given decision problem.

Forcing ineffective halt


This piece of code anywhere in program will move data pointer out of memory tape no matter of its contents. First loop will clear current cell (it will cycle until cell is blank). Next + will make it non-blank symbol, so we are sure program head enters main loop. Now we repeat following: move data pointer one cell left, clear its content and make cell non-blank. It ensures loop will repeat. And it will do so until it leaves tape, which is immediate, ineffective halt.

Abstract machine interpretation

As you may noticed, memory tape behaves a bit like a left-side ended Turing machine. We can say so about program tape too - program head moves from left end executing commands, until it hits any [. If program is well formed and current memory cell is blank, we move right to corresponding ] and continue after it. Similar with hitting ]. Of course, # is unconditional halt for both heads, like before. This interpretation makes it easy to see how to simulate this by Turing machine.

Oracle Brainf*ck

(I decided to redefine oracle) As you may guessed, this is Brainf*ck with oracle operator. We add 2 new symbols, { and } such that, if program within brackets halts on empty input, we cycle through symbol uner data pointer once and we continue to the right of }. So yeah, oracle! But it doesn't get us out of Church-Turing thesis. Why? Because, while halting problem is undecidable, any single instance of that is. Suppose given program halts. Then following pseudocode solves halting problem for it:

return true;

If program doesn't halt similar code says so. So for any program there is single algorithm deciding its halting problem (but problem of deciding which of these algorithms does so is undecidable). If program halts we can replace {} part with single +. Otherwise, we delete whole subroutine. So Brainf*ck can simulate this form of its own oracle.

If program has nested oracle brackets, we work from the deepest ones. We can make proof that any depth can be resolved by induction on maximal depth of oracles, but I think I can omit that step.

Escaping Church-Turing thesis

Right now we have failed oracle. Why it doesn't work? Because it solves only single instance of halting problem. If we had way to change what's inside of brackets, it'd look a lot better. But we can't alter program tape, so we can't make use of that. So here comes my idea - we have to add special $ symbol. When program head hits that symbol we will make a swap - we replace program head with data pointer and vice versa. If new program doesn't have well formed brackets, we simulate it until we hit bracket without corresponding par. Without oracle operator this system is obviously simulate-able. But what about adding oracle brackets?

Cycling now has form (blank)><+[]#{}$

Solving general halting problem

Given program A as input we want to decide if it halts. We can do it by using {A}. If A halts, {A} behaves like +, otherwise it is skipped. General idea is to have program which converts A to


And then swaps with data pointer on far left. Then produced code is executed as input. First it clears current cell. If A halts, then current cell is made non-empty and executes [#] part. It hits #, which means effective halt. Otherwise program skips that part and reaches my ineffective halt subroutine. So program always halts, and it halts effectively iff A halts.

Deciding decider

Problem of deciding if given program halts on every finite input (program is so called decider) is known to be strictly harder than halting problem (as it requires infinite number of halting instances to be checked). But it is no problem for above machine! Say we have some ordering on finite strings (say, lexicographical order). For nth string we need program An, which writes input and runs A on it without swap. This can be done recursively. We have to make program which will do following code:


Where after swapping we replace An with A(n+1) and will repeat. If for any string m Am won't halt, we'll reach [#] which will halt program. So program halts iff A isn't decider. By applying halting problem solver with effective/ineffective halt commands swapped, we just solved decider...ness problem!

Paradoxal statement

If there is Beauty, there must be the Beast. It is possible to create program P which, on empty tape, will write following minimalistic statement on tape:


And then will swap and execute it. Because of $'s place in cycle, after cycling it becomes blank. Does P halt? If it does, tape character will become non-blank, program head will enter brackets and will bounce between them indefinitely (If you're against empty brackets, put >< in them). So P won't halt, contradiction. Then, P doesn't halt, leaves mentioned character empty, skips brackets and hits EOF. Immediate halt. Contradiction. Paradox. \(\displaystyle\lim_{x \to 0} sin({1 \over x})\).

Strength of this system

If we can write programs of given strength \(\omega^\text{CK}_\alpha\), we can apply oracle operator to it, producing \(\omega^\text{CK}_{\alpha+1}\). Now goes hard part - if we can reach \(\alpha\) we can reach \(\omega^\text{CK}_\alpha\). This is highly non-trivilal, once I tried to write proof of that fact for Goucher's SKIΩ calculus. Same'd apply here, but formal proof must be pain in eye.

Using abstract machine interpretation one move is defined as any change of position of program head (i.e. executing command or skipping brackets).Define \(\Lambda(n)\) as largest number of steps achieved by n-character, halting program in Brainf*ck variant described above. Also, define \(\lambda(n)\) as corresponding function for effectively halting programs. Above analysis shows that: \(\Lambda(n)\approx \lambda(n) \approx f_\alpha(n)\), where \(\alpha\) is smallest fixed point of following map: \(\alpha \to \omega^\text{CK}_\alpha\).

Oracle tape (failed extension)

I had an idea of extending this system by adding rewritable oracle-like tape. It is infinite tape with own oracle head which always starts empty (all blank) and each cell holds either 1 or blank. This tape can be considered output even for nonhalting machines with following constrain - after infinite time given cell holds blank iff it becomes 1 only for finite number of steps. Now, main idea was to have additional command which replaces content of oracle tape to the right of oracle head with output of specified program (by adding another type of brackets or whatever).

With this new command we could make infinitely running program which checks all programs and writes 1 on oracle tape iff program halts. This'd allow to diagonalize through all \(\lambda\)-programs. Let's name all programs in newest system H-programs. Wait a minute - we diagonalized through \(\lambda\)-programs without any restriction which would disallow to generalize. So we can use same idea to diagonalize through H-programs! But here comes a problem - unrestricted diagonalization would lead us all the way to \(\omega_1\). So there must be a problem somewhere.

Problem is on very beginning. Program diagonalizing through \(\lambda\)-programs would certainly meet a problem of paradoxal programs. It can be proven that every program avoiding paradoxes must have strength weaker than \(\lambda\)-programs in general. Deciding paradoxes was already considered by Goucher, so I want to go some other way.

Paradox detection - big leap

First I want to define n-paradoxal program - program which, for all m<n, leads to paradox of form "program is m-paradoxal iff it isn't m-paradoxal", with 0-paradoxal programs being nonhalting programs. By adding subscript-indexed paradox checkers we can create by induction n+1-paradoxal program Pn+1 given n-paradoxal one Pn:


Yes, this is same thing Goucher defined, but I have hopes to define it transfinitely. I already now how to define such system in finite number of symbols. Now I'm trying to construct \(\omega\)-paradoxal statement using only finite paradox checkers. Any help appreciated!

Due to lack of any ideas I decided to reveal my secret plans anyway.

Transfinitely paradoxal programs

First I'll define \(\omega\)-paradoxal program - program which, for all finite n, is n-paradoxal. Let \(P_\omega\) be any such program (if it exists!). To check if program is \(\omega\)-paradoxal we introduce another paradox checker - | |ω+1. Now we can construct \(\omega+1\)-paradoxal program, checker for such programs, \(\omega+2\)-paradoxal program, etc. unboundedly. But that'd require infinitely many symbols... So, what now?

Ranking programs

For every well formed program I'm going to specify rank, just like Goucher did. Non-oracle programs have rank 0. Program applying oracle operator to programs with rank less than \(\alpha\) has rank \(\alpha\). For finite n we can have trivial n-ranked programs, like >{>{>{+}>}>}>. For transfinite ranks this requires diagonalization, for example, program which sequentially checks arbitrary programs with finite ranks. non-well formed programs have no rank.

Combining these ideas

Now we add single symbol - |. For programs P and Q, where Q has rank \(\alpha\), define {P|Q} as + iff P is \(\alpha\)-paradoxal and ignore it otherwise. So we now have paradox deciders for all ordinals as long as there is program with such rank. I think without use of | we can make programs with any rank as long as they are less than \(\Lambda\) function's limit. I will quickly recall Extended Veblen hierarchy \(\Phi(\alpha,\beta)\). It works like original Veblen hierarchy, expect \(\Phi(0,\alpha)=\omega^\text{CK}_\alpha\). So without | we can reach \(\Phi(1,0)\). Once I conjectured n-th order paradox decider has strength \(\Phi(n,0)\) and that this also follows transfinitely. So, with use of programs without | we can have paradox deciders up to \(\Phi(1,0)\), so adding these to the right of | leads us all the way up to \(\Phi(\Phi(1,0),0)\). My another conjecture is that this number is also bound on ranks of programs like these. If that's true, programs with |'s nested once have rank limit \(\Phi(\Phi(1,0),0)\). By nesting |'s and adding lots of conjectures we can have ranks, and function strengths, of form \(\Phi(\Phi(\Phi(\Phi((\Phi(\Phi(1,0),0),0),0),0),0)\) and further. So limit of that system reaches FB100Z's dream - \(\Gamma^\text{CK}_0\) function!

I want to recall that I have nothing of form of proof for any of these conjectures. Another thing is that I still don't know if there exists \(\omega\)-paradoxal program, although I strongly believe in it. If there is, we can extend that construction for all limit ordinals we need. If there is no such program, we are stuck at \(\Phi(\omega,0)\).

Further extension?

Right now, all programs of form {P|Q|R} are not well written, so maybe there is possibility to use that? And what about using {P|Q} with not-well-formed Q? Is it possible to define any structure on these programs? How about giving rank \(\Omega_1\) to 1-paradoxal programs? Does it make any sense? I don't know, but maybe I'll figure it out.

(Fun note: I l and | look a bit similar. "I'll" looks like three lines)