Author: ZmnSCPxj 2021-07-07 04:26:31
Published on: 2021-07-07T04:26:31+00:00
In a discussion about banning Turing completeness in Bitcoin, ZmnSCPxj suggests that unbounded recursive covenants should be allowed while partial Turing-completeness should be banned. He argues that such covenants are total Turing-complete and not partial Turing-complete. In a total programming language, there is a distinction between data and codata. Data is defined according to its constructors, whereas codata is defined according to its destructors. In a total function programming language, recursion is restricted by substructural recursion that ensures that every self-call should pass in a substructure of an argument as that argument, which provably terminates. Unbounded computations like infinite sequences of Fibonacci numbers are prevented in this way. Copattern matching makes corecursion termination as trivial as substructural recursion on the destructors, and copatterns are an important advance in total programming languages. Arbitrary-bound recursion can be implemented in a total language using the RecResult and Rec types, where the step function is a substructural recursion. The infinite loop is passed to a driving function written in C, which continuously calls step on the Haskell-level main program until it results in Complete () and exits. Similarly, recursive covenants in Bitcoin work equivalently to the codata types in total functional languages. As long as Bitcoin SCRIPT itself is provably terminating, unbounded processing can be achieved by using covenants outside the SCRIPT that have to be operated separately by a separate program, without objections.
Updated on: 2023-06-15T00:02:56.187561+00:00