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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \left(\mathbb N,0,S\right)}
be some ordered 3-tuple, where Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \mathbb N}
and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle 0}
are sets and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle S}
is a function from sets to sets, such that
- Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle 0\in\mathbb N}
- Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \forall\left(n\in\mathbb N\right),S\left(n\right)\in\mathbb N}
- Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \forall\left(n\in\mathbb N\right),0\ne S\left(n\right)}
- Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \forall\left(m,n\in\mathbb N\right),S\left(m\right)=S\left(n\right)\to m=n}
- Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \mathbb N} , Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle 0} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle S} , and proves that all of the conditions hold for them. Then we can define addition of natural numbers in the following way:
- Let Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle (+)}
be some binary operation on sets such that
- Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \forall\left(n\in\mathbb N\right),n+0=n}
- Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \forall\left(m,n\in\mathbb N\right),n+S(m)=S(n+m)}
We define comparison of natural numbers:
- Let (Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \le}
) be some binary relation on sets such that
- Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \forall\left(m,n\in\mathbb N\right),m\le n\iff\exists\left(k\in\mathbb N\right),m+k=n}
Real numbers
We can define real numbers like this:
- Let Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \left(\mathbb R,\le,+,\cdot\right)}
be some 4-tuple such that
- Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \left(\mathbb R,\le\right)} is a totally ordered set
- Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \left(\mathbb R,+,\cdot\right)} is a field
- Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \forall\left(x,y,z\in\mathbb R\right),x\le y\to x+z\le y+z}
- Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \forall\left(x,y\in\mathbb R\right),0\le x\to 0\le y\to 0\le x\cdot y}
- If Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle A} is a non-empty subset of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \mathbb R} , and if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle A} has an upper bound (under Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \le} ), then Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle A} has a least upper bound Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle u} , such that for every upper bound Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle v} of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle A} , Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle u\le v}
- Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \pi} as the ratio between the area and the radius of the unit circle (we would need to define Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \sigma} -algebra and Lebesgue measure first). We can then define what n-th digit of a real number means and we can "evaluate" number Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://en.wikipedia.org/api/rest_v1/":): {\displaystyle \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.