No, non è, in quanto se il compilatore potrebbe fare questa determinazione, che sarebbe equivalente a risolvere il Fermare il problema. In generale, il fatto che due funzioni si chiamino a vicenda in un pattern di "loop" non è sufficiente per concludere che effettivamente chiamare una delle funzioni risulterà in un loop.
Per usare un esempio (forzato),
collatzOdd :: Int -> Int
collatzOdd 1 = 1
collatzOdd n = let n' = 3*n+1 in if n' `mod` 2 == 0 then collatzEven n'
else collatzOdd n'
collatzEven :: Int -> Int
collatzEven n = let n' = n `div` 2 in if n' `mod` 2 == 0 then collatzEven n'
else collatzOdd n'
collatz :: Int -> Int
collatz n = if n `mod` 2 == 0 then collatzEven n else collatzOdd n
(Questo è, naturalmente, non è il modo più naturale per l'attuazione del Collatz conjecture, ma illustra le funzioni mutuamente ricorsive.)
Ora collatzEven
e collatzOdd
dipendono l'uno dall'altro, ma la congettura di Collatz afferma che la chiamata collatz
termina per tutti i positivi n
. Se GHC potesse determinare se una classe che aveva collatzOdd
e collatzEven
come definizioni predefinite avesse o meno una definizione completa, allora GHC sarebbe in grado di risolvere la congettura di Collatz! (Questo non è ovviamente una prova della non decifrabilità del problema di stallo, ma dovrebbe illustrare perché determinare se un insieme di funzioni reciprocamente ricorsive sia ben definito non è affatto banale come potrebbe sembrare.)
In in generale, poiché GHC non può determinarlo automaticamente, la documentazione per le classi Haskell fornirà la "definizione completa minima" necessaria per creare un'istanza di una classe.
fonte
2012-09-04 19:59:14
Sì! Nel caso del problema dell'arresto, le lingue globali come Agda dimostrano che i problemi irrisolvibili in generale possono avere sottoinsiemi solvibili grandi e interessanti. –
"" Semplicemente indecidibile "non è un criterio sufficiente per liquidare in modo inavvertito una tecnica di compilazione: la maggior parte dei problemi indecidibili che sono indecidibili nel caso generale sono abbastanza decidibili in casi specifici." http://c2.com/cgi/wiki?SufficientlySmartCompiler –
Il ticket trac è stato chiuso per un motivo priva di senso: qualcuno potrebbe definire un'istanza 'Num' senza' -' o 'negate' ma dove' + 'non valuta il suo secondo argomento, quindi la sua definizione apparentemente circolare finirà bene. Questo secondo argomento, sempre scartato, è l'unico modo per uscire dalla non-terminazione senza definire '-' o' negate'. Penso che questi siano casi d'uso bizzarri, ed è bene dover specificare '-noarnundefinedcyclicmethods 'se si vuole sfuggire alle definizioni circolari usando' _'. Non ho idea di come aumentare quello su Trac. – AndrewC