Dimostrazione di indecidibilità

[Deckard]

Gli esercizi di informatica in questa sezione non vanno tanto di moda, però la soluzione di questo mi sembrava carina, se qualcuno vuole cimentarsi:
Dimostrare che il seguente linguaggio è indecidibile:
$ L={(:M:) : M \text{ è una mdT che lavora in tempo } 100n^2 + 200} $

Con $(:M:)$ si intende la rappresentazione in binario della mdT $M$. Il tempo di calcolo scelto, $100n^2 + 200$, è ovviamente arbitrario.
Questo esercizio è stato preso dall'Arora-Barack, es. 3.1.
Per chi vuole un suggerimento:

Testo nascosto, fai click qui per vederlo

per dimostrarlo si può usare una riduzione dall'halting problem. Probabilmente è possibile dimostrarlo anche per diagonalizzazione, però per ora non ci sono riuscito

La dimostrazione è interessante perchè mette in luce un fatto non scontato:

Testo nascosto, fai click qui per vederlo

esiste una macchina di Turing $(:M:)$ che si sa per certo lavorare in tempo polinomiale, ma il cui tempo di calcolo rimane comunque indecidibile

[Lord K]

Io non vedo molto bene le formule che hai inserito...

[Deckard]

Io non vedo molto bene le formule che hai inserito...

Io le vedo normalmente, provo a riscriverle comunque come testo semplice:
Il linguaggio da dimostrare indecidibile è L = {<M>: M è una mdT che lavora in tempo 100n^2 + 200}
dove con <M> s'intende la rappresentazione in binario della mdT M. La funzione 100n^2 + 200 è arbitraria, non c'è niente di particolare in essa.