(0)

From Esolang
Jump to: navigation, search

(0) is a family of programming languages by David Madore defined in the 2017-08 blog entry Un peu de programmation transfinie.

Just like with the language Amycus was supposed to be, the goal of these languages is theoretical and educational. The languages are easy to describe and have just enough features to make writing programs in them easy, as long as you don't care about runtime performance at all.

Description of (0)

(0) has only one basic data type, ordinal numbers.

The language has user-defined named functions. Functions take any number of parameters, each an ordinal, the number of parameters for each function is fixed in the code. Functions return a single ordinal as the return value. Functions can also have additional mutable local variables whose value is also always an ordinal.

Built-in operations include loading or storing variables local to the function, calling named functions, natural number literals, ordinal addition, ordinal multiplication, all six ordered comparisons, and creating and decomposing ordered pairs. Pairs of ordinals are represented as ordinals too.

Recursive function calls are not permitted, functions can only call functions defined earlier in the source code. Control sequences include if-else conditionals, bounded size counting loops, and breaks and returns for jumping out of any number of nested loops or one function early. The counting loops count a loop variable on successive ordinals less than a bound given before you start of the loop, in increasing order. A copy of the loop variable is available during the loop, but assigning to the variable representing that doesn't modify how the loop executes. The loop variable is also available after the loop, keeping either the value when you broke out the loop, or the value of the loop bound if the loop run to completion. On loop iterations where the loop variable is a limit ordinal (an ordinal that isn't zero or a successor), local variables of the function take the value of the limsup of the values of the same variable at the end of all previous iterations of that instance of the same loop. Similarly, when a loop runs to completion and its bound is a limit ordinal, the value of the local variables is the limsup of their values at the end of each loop iteration.

There is no IO, when running a program you're just assumed to run a top-level function with parameters and examine the return value.

Properties of (0)

(0) is a total language, that is, programs always have a well-defined return value for any argument, they never get into undefined states or loops that never end.

If you restrict the inputs (arguments to the top level function) to natural numbers, than (0) can compute exactly the primitive recursive functions. In this case, the value of all expressions, local variables, and return values will always be a natural number during the execution of the program, and you don't need to use the limsup rule. The execution trace of the program will be finite in this case.

If you don't use such a restriction on the starting arguments, then (0) is uncomputable, and can in fact simulate any Turing machine, solve the halting problem for ordinary Turing machines, and do computations even more powerful than that.

Extensions

The article also defines a family of other languages that are extensions of (0).

(1)

(1) is like (0) but recursive function calls are allowed. This language is not total, because a function may never return if it gets into an infinite recursion.

If you use the restriction that the inputs are natural numbers, then (1) is Turing complete and no more powerful than that. In this case too, the language can't compute values other than natural numbers.

(2)

For certain ordinals λ that are called admissible ordinals, we define the language (2)λ as similar to (0) except that “unbounded loops” are allowed. An unbounded loop is similar to a bounded loop whose loop bound is λ, except that if the loop runs to completion, then the program is defined to never end (gives a bottom value). An ordinal λ is called admissible if and only if the language defined this way couldn't compute ordinals greater than or equal to λ.

(2)λ is not total.

It is interesting to examine (2)λ only when the inputs are restricted to less than λ. If you allow larger inputs, then (2)λ is as powerful as (0) with the same inputs, because it can compute a value greater than λ and simulate unbounded loops using that.

The simplest case is (2)ω. With inputs restricted to natural numbers, that language is Turing complete. It can only compute natural numbers, and unbounded loops work the same as while loops in ordinary programming languages.

For larger admissible λ, the (2)λ language is uncomputable.

(3)

(3)λ is similar to (2)λ, but allows recursive function calls.

The admissible ordinals turn out to be the same for (2) and (3), but this is hard to prove. (2)λ and (3)λ are equally powerful for any admissible λ, but this is also hard to prove.

with arrays

There's another version of each of the languages defined above that have arrays. Functions can declare array typed local variables. Array local variables are indexed by ordinals, and initially all array elements are zero. Expressions can load or store an element of an array variable with any expression as the index. Arrays have no size limit, they are extended to as far as the program accesses them. You cannot assign entire arrays, nor can you have arrays as arguments or return values. In limit ordinal steps of loops, each element of an array local variable gets its value by the same limsup rule as scalar variables.

When inputs are restricted to natural numbers only, (0) with arrays, (1) with arrays, (2)ω with arrays and (3)ω with arrays have exactly the same power as the same language without arrays. In this case, all values computed are natural numbers, and so all array indexes are too.

When inputs and λ are not restricted to natural numbers, then (0) with arrays, (1) with arrays, (2)λ with arrays and (3)λwith arrays still have exactly the same power as the same language without arrays, but this is hard to prove

History

Just like with the Amycus was supposed to be, David didn't bother to name the programming languages. Maybe he thought he couldn't top the name “Юᓂ곧⎔”. The (0) is just a name distinguishing the language from its extended versions. But that name seemed sufficiently esoteric and seems to be yet unused, so I just didn't bother to invent a proper name.