Codificación de Gödel
La 40ª Conferencia General de la UNESCO ha proclamado el de enero el Día mundial de la Lógica. La fecha del 14 de enero se ha eligido para rendir homenaje a dos grandes lógicos del siglo XX: Kurt Gödel (que falleció el 14 de enero de 1978) y Alfred Tarski (que nació el 14 de enero de 1901).
Gödel demostró en 1931 los teoremas de incompletitud y para su demostración introdujo la actualmente conocida como codificación de Gödel que asigna a cada fórmula de un lenguaje formal un número único.
En este ejercicio aplicaremos la codificación de Gödel a las listas de números enteros.
Dada una lista de números naturales xs, la codificación de Gödel de xs se obtiene multiplicando las potencias de los primos sucesivos, siendo los exponentes los sucesores de los elementos de xs. Por ejemplo, si xs es [6,0,4], la codificación de xs es
2^(6+1) * 3^(0+1) * 5^(4+1) = 1200000
Definir las funciones
codificaG :: [Integer] -> Integer decodificaG :: Integer -> [Integer]
tales que
- (codificaG xs) es la codificación de Gödel de xs. Por ejemplo,
codificaG [6,0,4] == 1200000 codificaG [3,1,1] == 3600 codificaG [3,1,0,0,0,0,0,1] == 4423058640 codificaG [1..6] == 126111168580452537982500
- (decodificaG n) es la lista xs cuya codificación es n. Por ejemplo,
decodificaG 1200000 == [6,0,4] decodificaG 3600 == [3,1,1] decodificaG 4423058640 == [3,1,0,0,0,0,0,1] decodificaG 126111168580452537982500 == [1,2,3,4,5,6]
Comprobar con QuickCheck que decodificaG es la inversa por la izquierda de codificaG; es decir, para toda lista xs de números enteros, se verifica que
decodificaG (codificaG ys) == ys
donde ys es la lista de los valores absolutos de los elementos de xs.
Soluciones
import Data.List (genericLength, group) import Data.Numbers.Primes (primes, primeFactors) import Test.QuickCheck codificaG :: [Integer] -> Integer codificaG xs = product [p^(x+1) | (p,x) <- zip primes xs] decodificaG :: Integer -> [Integer] decodificaG n = aux primes (group (primeFactors n)) where aux _ [] = [] aux (x:xs) (ys:yss) | x == head ys = genericLength ys - 1 : aux xs yss | otherwise = 0 : aux xs (ys:yss) -- La propiedad es propCodifica1 :: [Integer] -> Bool propCodifica1 xs = decodificaG (codificaG ys) == ys where ys = map abs xs -- La comprobación es -- λ> quickCheck propCodifica1 -- +++ OK, passed 100 tests.