PDF de programación - Tema 8: Razonamiento sobre programas - Informática (2015–16)

Tema 8: Razonamiento sobre programas

Informática (2015–16)

José A. Alonso Jiménez

Grupo de Lógica Computacional

Departamento de Ciencias de la Computación e I.A.

Universidad de Sevilla

IM Tema 8: Razonamiento sobre programas

Tema 8: Razonamiento sobre programas
1. Razonamiento ecuacional
Cálculo con longitud
Propiedad de intercambia
Inversa de listas unitarias
Razonamiento ecuacional con análisis de casos

2. Razonamiento por inducción sobre los naturales

Esquema de inducción sobre los naturales
Ejemplo de inducción sobre los naturales

3. Razonamiento por inducción sobre listas

Esquema de inducción sobre listas
Asociatividad de ++
[] es la identidad para ++ por la derecha
Relación entre length y ++
Relación entre take y drop
La concatenación de listas vacías es vacía

4. Equivalencia de funciones

2 / 49

IM Tema 8: Razonamiento sobre programas

Razonamiento ecuacional
Cálculo con longitud

Tema 8: Razonamiento sobre programas

1. Razonamiento ecuacional
Cálculo con longitud
Propiedad de intercambia
Inversa de listas unitarias
Razonamiento ecuacional con análisis de casos

2. Razonamiento por inducción sobre los naturales

3. Razonamiento por inducción sobre listas

4. Equivalencia de funciones

5. Propiedades de funciones de orden superior

3 / 49

IM Tema 8: Razonamiento sobre programas

Razonamiento ecuacional
Cálculo con longitud

Cálculo con longitud

Programa:

longitud []
longitud (_:xs) = 1 + longitud xs

= 0

-- longitud.1
-- longitud.2

Propiedad: longitud [2,3,1] = 3
Demostración:

longitud [2,3,1]
= 1 + longitud [2,3]
= 1 + (1 + longitud [3])
= 1 + (1 + (1 + longitud []))
= 1 + (1 + (1 + 0)
= 3

[por longitud.2]
[por longitud.2]
[por longitud.2]
[por longitud.1]

4 / 49

IM Tema 8: Razonamiento sobre programas

Razonamiento ecuacional

Propiedad de intercambia

Tema 8: Razonamiento sobre programas

1. Razonamiento ecuacional
Cálculo con longitud
Propiedad de intercambia
Inversa de listas unitarias
Razonamiento ecuacional con análisis de casos

2. Razonamiento por inducción sobre los naturales

3. Razonamiento por inducción sobre listas

4. Equivalencia de funciones

5. Propiedades de funciones de orden superior

5 / 49

IM Tema 8: Razonamiento sobre programas

Razonamiento ecuacional

Propiedad de intercambia

Propiedad de intercambia

Programa:

intercambia :: (a,b) -> (b,a)
intercambia (x,y) = (y,x)

-- intercambia

Propiedad: intercambia (intercambia (x,y)) = (x,y).
Demostración:

intercambia (intercambia (x,y))
= intercambia (y,x)
= (x,y)

[por intercambia]
[por intercambia]

6 / 49

IM Tema 8: Razonamiento sobre programas

Razonamiento ecuacional

Propiedad de intercambia

Propiedad de intercambia
Comprobación con QuickCheck

Propiedad:

prop_intercambia :: Eq a => a -> a -> Bool
prop_intercambia x y =

intercambia (intercambia (x,y)) == (x,y)

Comprobación:

*Main> quickCheck prop_intercambia
+++ OK, passed 100 tests.

7 / 49

IM Tema 8: Razonamiento sobre programas

Razonamiento ecuacional

Inversa de listas unitarias

Tema 8: Razonamiento sobre programas

1. Razonamiento ecuacional
Cálculo con longitud
Propiedad de intercambia
Inversa de listas unitarias
Razonamiento ecuacional con análisis de casos

2. Razonamiento por inducción sobre los naturales

3. Razonamiento por inducción sobre listas

4. Equivalencia de funciones

5. Propiedades de funciones de orden superior

8 / 49

IM Tema 8: Razonamiento sobre programas

Razonamiento ecuacional

Inversa de listas unitarias

Inversa de listas unitarias

Inversa de una lista:

inversa :: [a] -> [a]
inversa []
inversa (x:xs) = inversa xs ++ [x]

= []

-- inversa.1
-- inversa.2

Prop.: inversa [x] = [x]

inversa [x]
= inversa (x:[])
= (inversa []) ++ [x]
= [] ++ [x]
= [x]

[notación de lista]
[inversa.2]
[inversa.1]
[def. de ++]

9 / 49

IM Tema 8: Razonamiento sobre programas

Razonamiento ecuacional

Inversa de listas unitarias

Inversa de listas unitarias
Comprobación con QuickCheck

Propiedad:

prop_inversa_unitaria :: Eq a => a -> Bool
prop_inversa_unitaria x =

inversa [x] == [x]

Comprobación:

*Main> quickCheck prop_inversa_unitaria
+++ OK, passed 100 tests.

10 / 49

IM Tema 8: Razonamiento sobre programas

Razonamiento ecuacional

Razonamiento ecuacional con análisis de casos

Tema 8: Razonamiento sobre programas

1. Razonamiento ecuacional
Cálculo con longitud
Propiedad de intercambia
Inversa de listas unitarias
Razonamiento ecuacional con análisis de casos

2. Razonamiento por inducción sobre los naturales

3. Razonamiento por inducción sobre listas

4. Equivalencia de funciones

5. Propiedades de funciones de orden superior

11 / 49

IM Tema 8: Razonamiento sobre programas

Razonamiento ecuacional

Razonamiento ecuacional con análisis de casos

Razonamiento ecuacional con análisis de casos

Negación lógica:

not :: Bool -> Bool
not False = True
not True = False

Prelude

Prop.: not (not x) = x
Demostración por casos:

Caso 1: x = True:

not (not True) = not False

= True

Caso 2: x = False:

not (not False) = not True

= False

[not.2]
[not.1]

[not.1]
[not.2]

12 / 49

IM Tema 8: Razonamiento sobre programas

Razonamiento ecuacional

Razonamiento ecuacional con análisis de casos

Razonamiento ecuacional con análisis de casos
Comprobación con QuickCheck

Propiedad:

prop_doble_negacion :: Bool -> Bool
prop_doble_negacion x =

not (not x) == x

Comprobación:

*Main> quickCheck prop_doble_negacion
+++ OK, passed 100 tests.

13 / 49

IM Tema 8: Razonamiento sobre programas

Razonamiento por inducción sobre los naturales

Esquema de inducción sobre los naturales

Tema 8: Razonamiento sobre programas

1. Razonamiento ecuacional

2. Razonamiento por inducción sobre los naturales

Esquema de inducción sobre los naturales
Ejemplo de inducción sobre los naturales

3. Razonamiento por inducción sobre listas

4. Equivalencia de funciones

5. Propiedades de funciones de orden superior

14 / 49

IM Tema 8: Razonamiento sobre programas

Razonamiento por inducción sobre los naturales

Esquema de inducción sobre los naturales

Esquema de inducción sobre los números naturales
Para demostrar que todos los números naturales tienen una propiedad
P basta probar:
1. Caso base n=0:

P(0).

2. Caso inductivo n=(m+1):

Suponiendo P(m) demostrar P(m+1).

En el caso inductivo, la propiedad P(n) se llama la hipótesis de
inducción.

15 / 49

IM Tema 8: Razonamiento sobre programas

Razonamiento por inducción sobre los naturales

Ejemplo de inducción sobre los naturales

Tema 8: Razonamiento sobre programas

1. Razonamiento ecuacional

2. Razonamiento por inducción sobre los naturales

Esquema de inducción sobre los naturales
Ejemplo de inducción sobre los naturales

3. Razonamiento por inducción sobre listas

4. Equivalencia de funciones

5. Propiedades de funciones de orden superior

16 / 49

IM Tema 8: Razonamiento sobre programas

Razonamiento por inducción sobre los naturales

Ejemplo de inducción sobre los naturales

Ejemplo de inducción sobre los naturales: Propiedad

(replicate n x) es la lista formda por n elementos iguales a x.

Por ejemplo,
replicate 3 5 [5,5,5]

Prelude

replicate :: Int -> a -> [a]
replicate 0 _ = []
replicate n x = x : replicate (n-1) x

Prop.: length (replicate n x) = n

17 / 49

IM Tema 8: Razonamiento sobre programas

Razonamiento por inducción sobre los naturales

Ejemplo de inducción sobre los naturales

Ejemplo de inducción sobre los naturales: Demostración

Caso base (n=0):

length (replicate 0 x)
= length []
= 0

[por replicate.1]
[por def. length]

Caso inductivo (n=m+1):

length (replicate (m+1) x)
= length (x:(replicate m x))
= 1 + length (replicate m x)
= 1 + m
= m + 1

[por replicate.2]
[por def. length]
[por hip. ind.]
[por conmutativa de +]

18 / 49

IM Tema 8: Razonamiento sobre programas

Razonamiento por inducción sobre los naturales

Ejemplo de inducción sobre los naturales

Ejemplo de inducción sobre los naturales: Verificación
Verificación con QuickCheck:

Especificación de la propiedad:

prop_length_replicate :: Int -> Int -> Bool
prop_length_replicate n xs =

length (replicate m xs) == m
where m = abs n

Comprobación de la propiedad:

*Main> quickCheck prop_length_replicate
OK, passed 100 tests.

19 / 49

IM Tema 8: Razonamiento sobre programas
Razonamiento por inducción sobre listas

Esquema de inducción sobre listas

Tema 8: Razonamiento sobre programas

1. Razonamiento ecuacional

2. Razonamiento por inducción sobre los naturales

3. Razonamiento por inducción sobre listas

Esquema de inducción sobre listas
Asociatividad de ++
[] es la identidad para ++ por la derecha
Relación entre length y ++
Relación entre take y drop
La concatenación de listas vacías es vacía

4. Equivalencia de funciones

20 / 49

IM Tema 8: Razonamiento sobre programas
Razonamiento por inducción sobre listas

Esquema de inducción sobre listas

Esquema de inducción sobre listas
Para demostrar que todas las listas finitas tienen una propiedad P
basta probar:
1. Caso base xs=[]:

P([]).

2. Caso inductivo xs=(y:ys):

Suponiendo P(ys) demostrar P(y:ys).

En el caso inductivo, la propiedad P(ys) se llama la hipótesis de
inducción.

21 / 49

IM Tema 8: Razonamiento sobre programas
Razonamiento por inducción sobre listas

Asociatividad de ++

Tema 8: Razonamiento sobre programas

1. Razonamiento ecuacional

2. Razonamiento por inducción sobre los naturales

3. Razonamiento por inducción sobre listas

Esquema de inducción sobre listas
Asociatividad de ++
[] es la identidad para ++ por la derecha
Relación entre length y ++
Relación entre take y drop
La concatenación de listas vacías es vacía

4. Equivalencia de funciones

22 / 49

IM Tema 8: Razonamiento sobre programas
Razonamiento por inducción sobre listas

Asociatividad de ++

Asociatividad de ++

Programa:

Prelude

(++) ::