Island

Island

Paradigm(s)	Declarative
Designed by	User:Hakerh400
Appeared in	2022
Computational class	Turing complete
Major implementations	Unimplemented
File extension(s)	.txt

Island is a computational model invented by User:Hakerh400 in 2022.

Overview

The author of Island believes that this is the computational model of the future and that in the year of 2100 all programming languages will use this computational model (if the human civilization survives for that long).

In this computational model, we first specify some basic logic (for example higher-order logic) and then we specify axioms (for example Zermelo-Fraenkel set theory), and finally the axiom of global choice.

We write programs by using the global choice to construct objects that satisfy a given specification. The interpreter uses some advanced AI to prove that there exists a model for that specification, so that the specification holds for the constructed objects. The interpreter then performs computation by proving things about the constructed objects.

Examples

Natural numbers

We can construct natural numbers in the following way:

Let $\left(\mathbb {N} ,0,S\right)$ be some ordered 3-tuple, where $\mathbb {N}$ and $0$ are sets and $S$ is a function from sets to sets, such that

• $0\in \mathbb {N}$
• $\forall \left(n\in \mathbb {N} \right),S\left(n\right)\in \mathbb {N}$
• $\forall \left(n\in \mathbb {N} \right),0\neq S\left(n\right)$
• $\forall \left(m,n\in \mathbb {N} \right),S\left(m\right)=S\left(n\right)\to m=n$
• $\forall \left({\text{unary predicate }}P\right),P(0)\to \left(\forall \left(n\in \mathbb {N} \right),P\left(n\right)\to P\left(S\left(n\right)\right)\right)\to \forall \left(n\in \mathbb {N} \right),P\left(n\right)$

The interpreter proves that there exists a model for that specification, creates objects $\mathbb {N}$, $0$ and $S$, and proves that all of the conditions hold for them. Then we can define addition of natural numbers in the following way:

Let $(+)$ be some binary operation on sets such that

• $\forall \left(n\in \mathbb {N} \right),n+0=n$
• $\forall \left(m,n\in \mathbb {N} \right),n+S(m)=S(n+m)$

We define comparison of natural numbers:

Let ($\leq$) be some binary relation on sets such that

• $\forall \left(m,n\in \mathbb {N} \right),m\leq n\iff \exists \left(k\in \mathbb {N} \right),m+k=n$

Real numbers

We can define real numbers like this:

Let $\left(\mathbb {R} ,\leq ,+,\cdot \right)$ be some 4-tuple such that

• $\left(\mathbb {R} ,\leq \right)$ is a totally ordered set
• $\left(\mathbb {R} ,+,\cdot \right)$ is a field
• $\forall \left(x,y,z\in \mathbb {R} \right),x\leq y\to x+z\leq y+z$
• $\forall \left(x,y\in \mathbb {R} \right),0\leq x\to 0\leq y\to 0\leq x\cdot y$
• If $A$ is a non-empty subset of $\mathbb {R}$, and if $A$ has an upper bound (under $\leq$), then $A$ has a least upper bound $u$, such that for every upper bound $v$ of $A$, $u\leq v$
• $\mathbb {N} \subset \mathbb {R}$ (this requires some additional technical conditions)

Of course, we would first need to define what a field and totally ordered set are. This is just to demonstrate the point of how "defining" things would look like.

Calculation

We can, for example, define number $\pi$ as the ratio between the area and the radius of the unit circle (we would need to define $\sigma$-algebra and Lebesgue measure first). We can then define what n-th digit of a real number means and we can "evaluate" number $\pi$ to any number of decimal places, just by letting the interpreter determine each of the digits of interest by proving/disproving that the digit is equal to some value. We do not need to bother about optimizations or advanced and complex algorithms. We simply specify what we need and the interpreter figures out everything for us.

The interpreter is able to prove any provable statement (provable within the system of axioms we specified).

Conclusion

There are some languages such as Coq or Lean that have the concept of "computation", but they are very limited in that regard. First, not all functions in them are computable. Second, their computation has only one "path" that can be followed.

The computation in Island is much more powerful. All functions are potentially computable and the interpreter can do whatever it wants to "compute" the result by proving/disproving statements about the result, eventually reducing the result to a single concrete value.

For example, we can create a 3D rendering engine that has infinite precision. We define the world, objects, light, reflections, mirrors, shadows, and so on. Then we let the interpreter render each frame by "computing" the RGB value of each pixel, by proving/disproving for each pixel that the specific color value of that pixel is less than or greater than some constant, eventually bisecting the value to an 8-bit integer and displaying it on the screen.