Author: Billy Tetrud 2021-07-07 06:12:24
Published on: 2021-07-07T06:12:24+00:00
The bitcoin-dev mailing list is having a discussion about Turing-completeness and the use of recursive covenants. ZmnSCPxj argues that unlimited recursive covenants are total Turing-complete, but not partial Turing-complete, and should be allowed. He explains the concept of substructural recursion rules, which ensure that every self-call should pass in a substructure of an argument as that argument, leading to provable termination. ZmnSCPxj also introduces copattern matching, which allows for corecursion termination as trivial as substructural recursion on the destructors. He defines the RecResult and Rec types, which are sufficient to define an infinite loop in a total programming language. He notes that everything terminates within the total language and any infinite recursion would have to resolve to some IO type which explicitly allows for infinite recursion. He believes that recursive covenants work equivalently to the codata types in total functional languages. As long as Bitcoin SCRIPT itself is provably terminating, he has no objections to the fact that we get arbitrary-bound processing by use of covenants.Another topic of discussion is the need to operate ants separately by a separate program as they are "outside" the script. The writer suggests that state can be encoded in other parts of the transaction, making it possible to write something more substantive than `while (true) { /* do nothing */ }`. As a result, the suggestion is made to add `OP_TWEAK` and possibly convenience opcodes for building Taproot Merkle trees to make things easier.
Updated on: 2023-06-15T00:03:52.394825+00:00