En las clases de ayer y hoy Informática de 1º del Grado en Matemáticas hemos comentado las soluciones de la relación 31 en la que se plantean ejercicios de demostración por inducción de propiedades de programas. En concreto,

• la suma de los n primeros impares es n^2,
• 1 + 2^0 + 2^1 + 2^2 + … + 2^n = 2^(n+1),
• todos los elementos de (copia n x) son iguales a x,
• la equivalencia de las definiciones de factorial con y sin
• acumulador,
• amplia xs y = xs ++ [y].
• numeroDeListasConSuma n = 2^(n-1),
• fibItAux n (fib k) (fib (k+1)) = fib (k+n),
• potencia x n == x^n,
• reverse (xs ++ ys) == reverse ys ++ reverse xs,
• reverse (reverse xs) = xs,

y por inducción sobre árboles binarios

• espejo (espejo x) = x,
• postorden (espejo x) = reverse (preorden x),
• reverse (preorden (espejo x)) = postorden x,
• nNodos (espejo x) == nNodos x,
• length (preorden x) == nNodos x,
• nNodos x <= 2^(profundidad x) - 1,
• nHojas x = nNodos x + 1,
• preordenItAux x ys = preorden x ++ ys

Estos ejercicios corresponden al tema 8 del curso.

Los ejercicios de la relación, junto con sus soluciones, se muestran a continuación
Read More “I1M2012: Ejercicios de razonamiento sobre programas”

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado cómo demostrar propiedades de funciones definidas en Haskell. Los esquemas de demostración estudiados son:

• por simplificación,
• por casos,
• por inducción sobre los números naturales,
• por inducción sobre listas,
• por inducción anidada y
• por generalización e inducción.

Las transparencias usadas en la clase son las del tema 8:
Read More “I1M2012: Razonamiento sobre programas Haskell”