Re:Curry–Howard correspondence
by gciruelos on Monday August 13, 2018 @11:39PM
(#17755435)
Yes, in general it is obviously undecidable.
I should have been clearer, but I'm mostly interested in structure (traversal) algorithms, most of which could be coded in a language with bounded loops.
An easier question is the one of determining the complexity of an algorithm. I think there's a ton of work in this area, for example in techniques that use typing systems (types may for example specify how many times a parameter is used, thus allowing the program to infer the complexity).
(easier because the equivalence relation of "implementing the same algorithm" is strictly finer than "having the same complexity")
I should have been clearer, but I'm mostly interested in structure (traversal) algorithms, most of which could be coded in a language with bounded loops.
An easier question is the one of determining the complexity of an algorithm. I think there's a ton of work in this area, for example in techniques that use typing systems (types may for example specify how many times a parameter is used, thus allowing the program to infer the complexity).
(easier because the equivalence relation of "implementing the same algorithm" is strictly finer than "having the same complexity")