simbolos - Pruebas funcionales(Haskell)

instalar haskell en ubuntu

Question

Fallé en la lectura de RWH; y no renuncié, ordené a Haskell: el oficio de la programación funcional . Ahora tengo curiosidad acerca de estas pruebas funcionales en la página 146. Específicamente estoy tratando de probar la sum (reverse xs) = sum xs 8.5.1 sum (reverse xs) = sum xs . Puedo hacer algunas de las pruebas de inducción pero luego me quedo atascado ..

HYP:

sum ( reverse xs ) = sum xs

BASE:

sum ( reverse [] ) = sum []

Left  = sum ( [] ) (reverse.1)
      = 0          (sum.1)

Right = 0          (sum.1)

INDUCCIÓN:

sum ( reverse (x:xs) ) = sum (x:xs) 

Left = sum ( reverse xs ++ [x] )    (reverse.2)

Right = sum (x:xs)   
      = x + sum xs                  (sum.2)

Así que ahora solo estoy tratando de probar que la sum ( reverse xs ++ [x] ) Left sum ( reverse xs ++ [x] ) es igual a la x + sum xs Right , pero eso no está muy lejos de donde empecé la sum ( reverse (x:xs) ) = sum (x:xs) .

No estoy muy seguro de por qué esto debe probarse, parece totalmente razonable usar la prueba simbólica de reverse x:y:z = z:y:x (por definición), y porque + es conmutativo (arth) y luego reverse 1+2+3 = 3+2+1 ,

Answer 1

Aquí es donde creo que estás atrapado. Necesitas probar un lema que diga

sum (xs ++ ys) == sum xs + sum ys

Para probar esta ley, tendrá que asumir que la suma es asociativa, lo cual es cierto solo para enteros y racionales.

Luego, también deberá asumir que la suma es conmutativa, lo que es cierto para enteros y racionales, pero también para flotadores.

Digresión: El estilo de tus pruebas me parece muy extraño. Creo que le será más fácil escribir este tipo de pruebas si usa el estilo en el libro de Graham Hutton .

Answer 2

Básicamente necesitas demostrar que

sum (reverse xs ++ [x]) = sum (reverse xs) + sum [x]

que luego conduce fácilmente a

                        = x + sum (reverse xs)
                        = x + sum xs  -- by inductive hyp.

El problema es mostrar que la sum distribuye sobre la concatenación de listas.

Answer 3

Usa la definición de una suma para dividir (suma inversa xs ++ [x]) en x + suma (inversa (xs)), y usando tu hipótesis inductiva, sabes suma (inversa (xs)) = suma (xs). Pero estoy de acuerdo, la inducción es una exageración para un problema como este.

Answer 4

sum (reverse [])     = sum []                     -- def reverse
sum (reverse (x:xs)) = sum (reverse xs ++ [x])    -- def reverse
                     = sum (reverse xs) + sum [x] -- sum lemma below
                     = sum (reverse xs) + x       -- def sum
                     = x + sum (reverse xs)       -- commutativity assumption!
                     = x + sum xs                 -- inductive hypothesis
                     = sum (x:xs)                 -- definition of sum

Sin embargo, hay suposiciones subyacentes de asociatividad y conmutatividad que no están estrictamente garantizadas y esto no funcionará correctamente para una serie de tipos numéricos como Float y Double donde se violan esas suposiciones.

Lema: sum (xs ++ ys) == sum xs + sum ys dada la asociatividad de (+)

Prueba:

sum ([] ++ ys)     = sum ys           -- def (++)
                   = 0 + sum ys       -- identity of addition
                   = sum [] ++ sum ys -- def sum

sum ((x:xs) ++ ys) = sum (x : (xs ++ ys))  -- def (++)
                   = x + sum (xs ++ ys)    -- def sum 
                   = x + (sum xs + sum ys) -- inductive hypothesis
                   = (x + sum xs) + sum ys -- associativity assumption!
                   = sum (x:xs) + sum ys   -- def sum