Tema 10

Inform´
atica

–

Haskell

– Matem´
aticas – Curso 2004-2005

Pepe Gallardo – Universidad de M´
alaga

Tema 10. Razonamiento ecuacional
10.1 Pruebas directas
10.2 Pruebas por casos
10.3 Pruebas por inducci´on

10.1 Pruebas directas
El razonamiento formal con programas funcionales es simple
Gracias a la transparencia referencial podemos sustituir t´
erminos equivalentes
Consideraremos lasecuaciones en una definici´
on de funci´
on como equivalencias (Axiomas)

EJEMPLO
cambio
::
cambio (x , y ) =

(a , b ) → (b , a )
(y , x )

Demostrar que
∀ m ::a , n ::b

cambio (cambio (m , n )) ≡≡ (m , n )

Axiomas
∀ x ::a , ∀ y ::b

cambio (x , y ) ≡≡ (y , x )

– – Ax1

Demostraci´
on

cambio (cambio (m, n))
≡≡

{por Ax1 }

cambio (n, m)
≡≡

{por Ax1 }

(m , n )

Inform´
atica – Pepe Gallardo –Universidad de M´
alaga

10.1

10.2 Pruebas por casos
Para tipos no recursivos, basta con probar la propiedad para cada constructor

EJEMPLO

data Bool =

False | True

not
:: Bool → Bool
not True = False
not False = True
Demostrar que
∀ x ::Bool

not (not x ) ≡≡ x

Axiomas

not True ≡≡ False
not False ≡≡ True

– – Ax1
– – Ax2

Demostraci´
on
Si x es False , hay que demostrar

Si x es True , hay quedemostrar

not (not False ) ≡≡ False

not (not True ) ≡≡ True

not (not F alse)

not (not T rue)

≡≡

{por Ax2 }

≡≡

not F alse

not T rue
≡≡

{por Ax1 }

False

{por Ax1 }

≡≡

{por Ax2 }

True

La propiedad queda demostrada para cualquier x ::Bool

Inform´
atica – Pepe Gallardo – Universidad de M´
alaga

10.2

10.3 Pruebas por inducci´
on
Para tipos recursivos, el n´
umero de casos a considerares infinito
No podemos demostrar todos los casos
Se usa la inducci´
on

EJEMPLO

data Nat = Cero | Suc Nat deriving Show
(< + >)
::
m < + > Cero =
m < + > Suc n =

Nat → Nat → Nat
m
Suc (m < + > n )

Demostrar que
∀ x ::Nat

Cero < + > x ≡≡ x

Principio de inducci´
on para el tipo Nat
P (Cero)
∧
∀x :: N at
P (x) ⇔
∀x :: N at
P (x) ⇒ P (Suc x)

Caso base: Hay que demostrar P (Cero )
Pasoinductivo: Hay que demostrar P (Suc x ) supuesto P (x )

Inform´
atica – Pepe Gallardo – Universidad de M´
alaga

10.3

Pruebas por inducci´
on (2)
Propiedad
∀ x ::Nat

Cero < + > x ≡≡ x

Axiomas
∀ m ::Nat
∀ m , n ::Nat

m < + > Cero ≡≡ m
m < + > Suc n ≡≡ Suc (m < + > n )

– – Ax1
– – Ax2

Caso base: Hay que demostrar

Cero < + > Cero ≡≡ Cero
Demostraci´
on
Cero < + > Cero
≡≡

{por Ax1 }

Cero

Pasoinductivo: Hay que demostrar
∀ x ::Nat

(Cero < + > x ≡≡ x) ⇒ (Cero < + > Suc x ≡≡ Suc x )
Hip´o tesis de Inducci´o n

Demostraci´
on
Cero < + > Suc x
≡≡

{por Ax2 }

Suc (Cero < + > x)
≡≡

{por hip´
otesis de inducci´
on}

Suc x

La propiedad queda demostrada para cualquier x ::Nat

Inform´
atica – Pepe Gallardo – Universidad de M´
alaga

10.4

Pruebas por inducci´
on (3)
Las listas tambi´
en son untipo recursivo

data [a ] = [ ] | a : [a ]

∀ls :: [a]

Principio de inducci´
on para listas
P ([ ])
∧
P (ls) ⇔
∀xs :: [a], ∀x :: a
P (xs) ⇒ P (x : xs)

Caso base: Hay que demostrar P ([ ])
Paso inductivo: Hay que demostrar P (x : xs ) supuesto P (xs )

EJEMPLO

suma
:: [Int ] → Int
suma [ ]
= 0
suma (x : xs ) = x + suma xs
doble
:: [Int ] → [Int ]
doble [ ]
= []
doble (x : xs ) = 2 ∗ x : doblexs
Demostrar
∀ ls ::[Int ]

suma (doble ls ) ≡≡ 2 ∗ suma ls

Caso base: Hay que demostrar suma (doble [ ]) ≡≡ 2 ∗ suma [ ]
Paso inductivo: Hay que demostrar
∀ xs ::[Int ], ∀ x ::Int
suma (doble xs ) ≡≡ 2 ∗ suma xs
– – Hip´
otesis
⇒
suma (doble (x : xs )) ≡≡ 2 ∗ suma (x : xs )
Inform´
atica – Pepe Gallardo – Universidad de M´
alaga

de inducci´
on

10.5

Pruebas por inducci´
on (4)
Axiomas

suma []
≡≡ 0
∀ x ::Int , ∀ xs ::[Int ] suma (x : xs ) ≡≡ x + suma xs

– – AxSuma1
– – AxSuma2

doble [ ]
≡≡ [ ]
∀ x ::Int , ∀ xs ::[Int ] doble (x : xs ) ≡≡ 2 ∗ x : doble xs

– – AxDoble1
– – AxDoble2

Caso base: Hay que demostrar

suma (doble [ ]) ≡≡ 2 ∗ suma [ ]
Demostraci´
on

suma (doble [ ])
≡≡

{por AxDoble1 }

2 ∗ suma [ ]
≡≡

suma [ ]
≡≡

{por AxSuma1 }

{por AxSuma1 }

2 ∗ 0
≡≡

0

{aritm´...