<< Dependent type theories that are total and have a computable normalization procedure are Turing-incomplete. This is a theorem, not an opinion. Now, what the implications are for practical usability of dependent type theories that are total, that is an entirely different matter. >> [1] (slightly adapted: see the entire discussion for background)
Conversely, I would argue that Turing Machines are not an adequate model of computation: there just is no such thing as a machine that does not halt or crash or get switched off, eventually. And, eventually rather goes with interactively.
In fact, more generally, the name of that "misunderstanding" is yet again the problem of infinity in standard mathematics and mathematical logic.
[1] SE, Proof Assistants, "Possible root cause(s) of the misunderstanding that
DTT implies not Turing complete?"
https://proofassistants.stackexchange.com/q/4002/3006#comment7782_4002
No comments :
Post a Comment