12 ms·

The whole point of Ethereum is turing completeness. Ethereum without Turing completeness already exists and its called Bitcoin. While this implementation of Th

The whole point of Ethereum is turing completeness. Ethereum without Turing completeness already exists and its called Bitcoin. While this implementation of The Dao has failed, Ethereum is the only blockchain where implementing The Dao is possible.

TylerE 10y ago
There is a huge canyon between "you can use this small set of ops" and "turing complete".
- jacques_chester 10y ago
  Not really. Any language that has sequential instructions, branching and loops is Turing complete, per the Structured Programming Theorem. Given how hard it is to avoid accidentally introducing these three "simple" elements, Turing completeness often turns up without being planned for.
drdeca 10y ago
There is a thing that advertises itself as being like Ethereum but without the Turing completeness. It is meant to be able to do more computation based stuff than Bitcoin, but without being Turing complete. However, they seem to have confused the halting problem not being computable with Godel's second incompleteness theorem? (They might have corrected this since I saw when they published something with this.)
- wtallis 10y ago
  >However, they seem to have confused the halting problem not being computable with Godel's second incompleteness theorem? (They might have corrected this since I saw when they published something with this.) They seem to be related concepts. See http://www.scottaaronson.com/blog/?p=2725 http://www.scottaaronson.com/blog/?p=2725 for discussion of some interesting examples: > [...] has explicitly constructed a one-tape, two-symbol Turing machine with 7,918 states, whose behavior (when run on a blank tape) can never be proven from the usual axioms of set theory, under reasonable consistency hypotheses. Adam has also constructed a 4,888-state Turing machine that halts iff there’s a counterexample to Goldbach’s Conjecture, and a 5,372-state machine that halts iff there’s a counterexample to the Riemann Hypothesis.
  - drdeca 10y ago
    I didn't mean that the two aren't related, just that they aren't as strongly related as the group seemed to be implying. They were saying that Ethereum being turing complete made it inconsistent in some way. But yes, the two definitely are connected. For example: A program which could solve the halting problem would be able to determine whether a given system is consistent. So, as a result, if a system could prove that a program solved the halting problem, and it could simulate programs running, then it could simulate the program that solves the halting problem being applied to a program that searches for inconsistencies in the system. This would allow it to prove whether it is itself consistent. Therefore, by Godel's second incompleteness theorem, a system which can simulate programs for any number of steps, and which is consistent, and which can do arithmetic and such, cannot prove that any particular program solves the halting problem. Admittedly, this is a lot weaker than "no program solves the halting problem", but I think it is a fairly clear connection. So, yes, I agree that they are related. But Ethereum's Turing completeness (or, Turing completeness except being limited by gas costs), does not mean that Ethereum is "inconsistent", because that is, uh, pretty much a nonsense claim. And that is the claim that I think the other group was making (Though they may have stopped making it since.) Also, btw, wrt that blogpost, they got the number of states for a machine which ZFC cannot prove does not halt, but which does not halt, down to, iirc, like 2030 ? But you probably knew that already because it is the next blogpost on there. But yeah that is a cool result!
dkarapetyan 10y ago
This doesn't sound right to me. Contract law should not require turing completeness. First order logic should be more than sufficient. How does having a loop in contract law make any sense?
- conception 10y ago
  Would regular payments based on criteria be an example? A paycheck basically.
  - naasking 10y ago
    This argues for a temporal logic, not for recursion. Something like: http://szabo.best.vwh.net/contractlanguage.html http://szabo.best.vwh.net/contractlanguage.html
- wyager 10y ago
  There are also a class of total languages (Coq, Agda, Idris) that are guaranteed to terminate but admit (polymorphic) recursion. This is stronger than FOL but weaker than turing-completeness, and certainly sufficient to implement any feasible contract.
  - dkarapetyan 10y ago
    I agree. I said first-order logic because I think it is more accessible. Coq, Agda, Idris, etc. employ I think some pretty sophisticated type theory and that would all have to be packaged up in a way that is accessible to an average programmer.
    - wyager 10y ago
      > in a way that is accessible to an average programmer. The average programmer should not be writing multi-million-dollar contracts.
      - dkarapetyan 10y ago
intrasight 10y ago
I also don't see the relevance of it being TC. I've heard regex is TC. Wouldn't want to write a contract in regex.
- wyager 10y ago
  > I've heard regex is TC. You heard wrong. Regex is specifically not turing complete. It corresponds to the class of machines called DFAs. Above regexes are CFGs, which correspond to pushdown automata. Above CFGs are CSGs, which correspond to linear bounded automata. Above CSGs are unrestricted grammars, which correspond to turing machines. You may be thinking of PCREs, which aren't actually regular expressions, but are sometimes erroneously referred to as such. I don't know if those are turing complete or not.
- SolarNet 10y ago
  By definition regular expressions are not Turing complete... There is an ordering relationship between turing machines and regular expressions which explicitly states regular expressions are strictly a subset of turning machines. This is automata theory 101. Ask for a refund from your school. Jesus what has this field come to.
naasking 10y ago
> Ethereum without Turing completeness already exists and its called Bitcoin. There are an infinite number of non-Turing complete languages. Not-Turing complete != Bitcoin.

TylerE 10y ago

There is a huge canyon between "you can use this small set of ops" and "turing complete".

jacques_chester 10y ago
Not really. Any language that has sequential instructions, branching and loops is Turing complete, per the Structured Programming Theorem. Given how hard it is to avoid accidentally introducing these three "simple" elements, Turing completeness often turns up without being planned for.

drdeca 10y ago

There is a thing that advertises itself as being like Ethereum but without the Turing completeness. It is meant to be able to do more computation based stuff than Bitcoin, but without being Turing complete. However, they seem to have confused the halting problem not being computable with Godel's second incompleteness theorem? (They might have corrected this since I saw when they published something with this.)

wtallis 10y ago
>However, they seem to have confused the halting problem not being computable with Godel's second incompleteness theorem? (They might have corrected this since I saw when they published something with this.) They seem to be related concepts. See http://www.scottaaronson.com/blog/?p=2725 http://www.scottaaronson.com/blog/?p=2725 for discussion of some interesting examples: > [...] has explicitly constructed a one-tape, two-symbol Turing machine with 7,918 states, whose behavior (when run on a blank tape) can never be proven from the usual axioms of set theory, under reasonable consistency hypotheses. Adam has also constructed a 4,888-state Turing machine that halts iff there’s a counterexample to Goldbach’s Conjecture, and a 5,372-state machine that halts iff there’s a counterexample to the Riemann Hypothesis.
- drdeca 10y ago
  I didn't mean that the two aren't related, just that they aren't as strongly related as the group seemed to be implying. They were saying that Ethereum being turing complete made it inconsistent in some way. But yes, the two definitely are connected. For example: A program which could solve the halting problem would be able to determine whether a given system is consistent. So, as a result, if a system could prove that a program solved the halting problem, and it could simulate programs running, then it could simulate the program that solves the halting problem being applied to a program that searches for inconsistencies in the system. This would allow it to prove whether it is itself consistent. Therefore, by Godel's second incompleteness theorem, a system which can simulate programs for any number of steps, and which is consistent, and which can do arithmetic and such, cannot prove that any particular program solves the halting problem. Admittedly, this is a lot weaker than "no program solves the halting problem", but I think it is a fairly clear connection. So, yes, I agree that they are related. But Ethereum's Turing completeness (or, Turing completeness except being limited by gas costs), does not mean that Ethereum is "inconsistent", because that is, uh, pretty much a nonsense claim. And that is the claim that I think the other group was making (Though they may have stopped making it since.) Also, btw, wrt that blogpost, they got the number of states for a machine which ZFC cannot prove does not halt, but which does not halt, down to, iirc, like 2030 ? But you probably knew that already because it is the next blogpost on there. But yeah that is a cool result!

dkarapetyan 10y ago

This doesn't sound right to me. Contract law should not require turing completeness. First order logic should be more than sufficient. How does having a loop in contract law make any sense?

conception 10y ago
Would regular payments based on criteria be an example? A paycheck basically.
- naasking 10y ago
  This argues for a temporal logic, not for recursion. Something like: http://szabo.best.vwh.net/contractlanguage.html http://szabo.best.vwh.net/contractlanguage.html
wyager 10y ago
There are also a class of total languages (Coq, Agda, Idris) that are guaranteed to terminate but admit (polymorphic) recursion. This is stronger than FOL but weaker than turing-completeness, and certainly sufficient to implement any feasible contract.
- dkarapetyan 10y ago
  I agree. I said first-order logic because I think it is more accessible. Coq, Agda, Idris, etc. employ I think some pretty sophisticated type theory and that would all have to be packaged up in a way that is accessible to an average programmer.
  - wyager 10y ago
    > in a way that is accessible to an average programmer. The average programmer should not be writing multi-million-dollar contracts.
    - dkarapetyan 10y ago

intrasight 10y ago

I also don't see the relevance of it being TC. I've heard regex is TC. Wouldn't want to write a contract in regex.

wyager 10y ago
> I've heard regex is TC. You heard wrong. Regex is specifically not turing complete. It corresponds to the class of machines called DFAs. Above regexes are CFGs, which correspond to pushdown automata. Above CFGs are CSGs, which correspond to linear bounded automata. Above CSGs are unrestricted grammars, which correspond to turing machines. You may be thinking of PCREs, which aren't actually regular expressions, but are sometimes erroneously referred to as such. I don't know if those are turing complete or not.
SolarNet 10y ago
By definition regular expressions are not Turing complete... There is an ordering relationship between turing machines and regular expressions which explicitly states regular expressions are strictly a subset of turning machines. This is automata theory 101. Ask for a refund from your school. Jesus what has this field come to.

naasking 10y ago

> Ethereum without Turing completeness already exists and its called Bitcoin. There are an infinite number of non-Turing complete languages. Not-Turing complete != Bitcoin.