4 ms·

A problem I've thought about lately has been making a programming language that optimizes for being expressive up to, but not including, being Turing complete (

A problem I've thought about lately has been making a programming language that optimizes for being expressive up to, but not including, being Turing complete (specifically, making non-terminating programs unexpressible).

Kranar 4y ago
Yeah you can definitely make a language that is not Turing complete but your goal of "up-to" is not possible. For any complexity class C that is not Turing complete, there is a complexity class C' that is a strict super-set of C and is also not Turing complete.
- convolvatron 4y ago
  sorry, really genuinely interested in the structure here, reference?
  - Kranar 4y ago
    Sure, the insight/intuition comes from diagonalization, or perhaps more directly from Cantor's theorem. For any complexity class O(F(N)), there must exist a complexity class O(2^F(N)) that is strictly a superset of O(F(N)). If F(N) is decidable then so too is 2^F(N). https://en.wikipedia.org/wiki/Cantor%27s_theorem https://en.wikipedia.org/wiki/Cantor%27s_theorem
- deleted 4y ago
  [deleted]
chaosite 4y ago
The go-to example for something like that is Datalog.
lapinot 4y ago
Basically you disallow general recursion (while loops, etc) and just allow structural/well-founded/inductive recursion (for loops, finite structure walking, etc). https://en.wikipedia.org/wiki/Total_functional_programming https://en.wikipedia.org/wiki/Total_functional_programming Type-theory based proof assistants (coq, agda, lean, idris, ..) are like this.
- nyrikki 4y ago
  The problem being that if you can reduce a problem to being well ordered on the naturals it is already in the computable set. Note how the limits on recursion as given by the original paper apply to the fibonacci sequence, but restricted to the Natural numbers to avoid the -2 -1 1 0 1,1 2 portion that would break total ordering. Any problem that you can map to von Neumann ordinals will be computable. Same thing with the Cantor diagonalization example below. Basically if you can reduce your problem to a monoid, you can typically compute it easily. But as a group has to be a magma with inverse, the recursive example provided couldn't be used in a case that function needed to be applied to algebras, rings, fields etc.... Note that as Cantor diagonalization was used as a counterexample to Laplacian causal determinism, showing that no two computational device can completely predict each other when defined by external behavior, there are further constraints. For me, an easier lens to see if there is a P solution to a typically NP problem is looking at Schaefer's dichotomy theorem. Total Functional Programing is exactly equivalent to #3, 1) all relations which are not constantly false are true when all its arguments are true; 2) all relations which are not constantly false are true when all its arguments are false; 3) all relations are equivalent to a conjunction of binary clauses; 4) all relations are equivalent to a conjunction of Horn clauses; 5) all relations are equivalent to a conjunction of dual-Horn clauses; 6) all relations are equivalent to a conjunction of affine formulae. The mapping to the Natural numbers is a leaky abstraction, as the Natural numbers are a non-empty totally ordered set with no upper bound. Any function that takes finitely many natural numbers as arguments and produce a value which is a single natural number are by definition computable. That restricted problem will always be computable no matter if the more generalized problem is in NP or not. https://ncatlab.org/ufias2012/files/turner.pdf https://ncatlab.org/ufias2012/files/turner.pdf
Animats 4y ago
Decision tables [1] have that property. They have a finite number of states and you can test all of them. If "smart contracts" in crypto land were written as decision tables, it might have helped a bit. [1] https://en.wikipedia.org/wiki/Decision_table https://en.wikipedia.org/wiki/Decision_table
deterministic 4y ago
This already exists: Coq, Idris, Agda, LEAN etc.

Kranar 4y ago

Yeah you can definitely make a language that is not Turing complete but your goal of "up-to" is not possible. For any complexity class C that is not Turing complete, there is a complexity class C' that is a strict super-set of C and is also not Turing complete.

convolvatron 4y ago
sorry, really genuinely interested in the structure here, reference?
- Kranar 4y ago
  Sure, the insight/intuition comes from diagonalization, or perhaps more directly from Cantor's theorem. For any complexity class O(F(N)), there must exist a complexity class O(2^F(N)) that is strictly a superset of O(F(N)). If F(N) is decidable then so too is 2^F(N). https://en.wikipedia.org/wiki/Cantor%27s_theorem https://en.wikipedia.org/wiki/Cantor%27s_theorem
deleted 4y ago
[deleted]

chaosite 4y ago

The go-to example for something like that is Datalog.

lapinot 4y ago

Basically you disallow general recursion (while loops, etc) and just allow structural/well-founded/inductive recursion (for loops, finite structure walking, etc). https://en.wikipedia.org/wiki/Total_functional_programming https://en.wikipedia.org/wiki/Total_functional_programming Type-theory based proof assistants (coq, agda, lean, idris, ..) are like this.

nyrikki 4y ago
The problem being that if you can reduce a problem to being well ordered on the naturals it is already in the computable set. Note how the limits on recursion as given by the original paper apply to the fibonacci sequence, but restricted to the Natural numbers to avoid the -2 -1 1 0 1,1 2 portion that would break total ordering. Any problem that you can map to von Neumann ordinals will be computable. Same thing with the Cantor diagonalization example below. Basically if you can reduce your problem to a monoid, you can typically compute it easily. But as a group has to be a magma with inverse, the recursive example provided couldn't be used in a case that function needed to be applied to algebras, rings, fields etc.... Note that as Cantor diagonalization was used as a counterexample to Laplacian causal determinism, showing that no two computational device can completely predict each other when defined by external behavior, there are further constraints. For me, an easier lens to see if there is a P solution to a typically NP problem is looking at Schaefer's dichotomy theorem. Total Functional Programing is exactly equivalent to #3, 1) all relations which are not constantly false are true when all its arguments are true; 2) all relations which are not constantly false are true when all its arguments are false; 3) all relations are equivalent to a conjunction of binary clauses; 4) all relations are equivalent to a conjunction of Horn clauses; 5) all relations are equivalent to a conjunction of dual-Horn clauses; 6) all relations are equivalent to a conjunction of affine formulae. The mapping to the Natural numbers is a leaky abstraction, as the Natural numbers are a non-empty totally ordered set with no upper bound. Any function that takes finitely many natural numbers as arguments and produce a value which is a single natural number are by definition computable. That restricted problem will always be computable no matter if the more generalized problem is in NP or not. https://ncatlab.org/ufias2012/files/turner.pdf https://ncatlab.org/ufias2012/files/turner.pdf

Animats 4y ago

Decision tables [1] have that property. They have a finite number of states and you can test all of them. If "smart contracts" in crypto land were written as decision tables, it might have helped a bit. [1] https://en.wikipedia.org/wiki/Decision_table https://en.wikipedia.org/wiki/Decision_table

deterministic 4y ago

This already exists: Coq, Idris, Agda, LEAN etc.