Inducción

La inducción un método para demostrar la validez de propiedades sobre estructuras de datos recursivas, como listas o árboles, utilizando un caso base y un paso inductivo.

La idea que rige este principio consiste en demostrar dos cosas:

• Por un lado verificar que la propiedad se satisface para los elementos “más chicos” del dominio (por ejemplo, la lista $[]$).

• Por otro lado demostrar para un elemento arbitrario del dominio (por ejemplo, la lista $(x\;▹\;xs)$) que si suponemos que la propiedad es cierta para todos los elementos más chicos que él (por ejemplo $xs$), entonces la propiedad también es satisfecha por ese elemento.

Dado que todo elemento de un dominio inductivo puede ser “construido” a partir de elementos más simples, este procedimiento demuestra que la propiedad es satisfecha por todos los elementos del dominio, y por lo tanto es válida.

Ejercicios resueltos - Inducción en funciones

Considerando las siguientes funciones, probar las siguientes propiedades por inducción.

1.

Definimos el caso base ($xs = [ ]$):

≡{ Caso base de $length$ }

≡{ Aritmética }

Definimos el paso inductivo ($xs = (x \;▹ \;xs)$):

≡{ Definición de $length$ }

≡{ Aritmética }

2.

Definimos el caso base ($xs = [ ]$):

≡{ Caso base de $sumar1, length, sumatoria$ }

≡{ Caso base de $sumatoria$, Aritmética }

≡{ Aritmética }

Definimos el paso inductivo ($xs = (x \;▹ \;xs)$):

≡{ Definición de $sumar1, length, sumatoria$ }

≡{ Definición de $sumatoria$ }

≡{ Hipótesis Inductiva }

≡{ Asociatividad de $+$, reflexividad de $=$ }

Considerando las siguientes funciones, probar las siguientes propiedades por inducción.

3.

Definimos el caso base ($xs = [ ]$):

≡{ Caso base de $sacaUnos, productoria$ }

≡{ Caso base de $productoria$ }

≡{ Reflexividad de $=$ }

Definimos el paso inductivo ($xs = (x \;▹ \;xs)$):

Caso 1: $x = 1$

≡{ Definición de $sacaUnos, productoria$ }

≡{ Hipótesis Inductiva, Aritmética }

≡{ Reflexividad de $=$ }

Caso 2: $x \neq 1$

≡{ Definición de $sacaUnos, productoria$ }

≡{ Definición de $productoria$ }

≡{ Hipótesis Inductiva}

≡{ Reflexividad de $=$ }

Al ser verdadera para ambos casos, la propiedad es válida.

Cálculo de Predicados

El cálculo de predicados es una técnica permite demostrar propiedades sobre estructuras de datos recursivas, como listas o árboles, utilizando reglas de inferencia y cuantificadores.

Semántica de Lógica de Predicados

La lógica de cuantificadores extiende la lógica proposicional incorporando dos operadores de cuantificación y el uso de predicados:

• El cuantificador universal $∀$ permite expresar que una fórmula se satisface para todo valor posible del universo.

Por ejemplo, si tenemos el predicado $mult3.x$ (devuelve $True$ si $x$ es múltiplo de $3$ y $False$ en caso contrario) el predicado “todo $x$ es múltiplo de $3$” se puede expresar formalmente como: $⟨∀x : : mult3.x⟩$.

• El cuantificador existencial $∃$ expresa que la propiedad es satisfecha por al menos un valor posible del universo.

Por ejemplo, la expresión $\bigl \langle \; ∃x : : mult3.x \; \bigr \rangle$ significa “existe un $x$ que es múltiplo de $3$”.

Para restringir o hacer explícito el universo al que nos referimos se utilizan otros predicados que diferenciamos como rango. Por ejemplo, si queremos restringir el universo a aquellos elementos que cumplen con una determinada propiedad $R.x$ lo denotamos de la siguiente manera:

Si decimos que “todos los hombres son mortales” lo podemos expresar formalmente como:

Si nuestro rango es verdadero para todos los elementos, podemos omitirlo y escribir simplemente:

Tanto los corchetes $\bigl \langle \; \bigr \rangle$ como el par de “dos puntos” ($:$) sirven para delimitar las distintas partes de las expresiones cuantificadas. Por tal motivo, las agrupan como paéntesis y esto debería ayudar a evitar confusiones de asociatividad y precedencia.

Utilizaremos los cuantificadores en esta asignatura es para expresar propiedades sobre listas. En general, nos interesa referirnos a los elementos de la lista por lo que definiremos el predicado $x ∈_ℓ xs$ como “$x$ está en la lista $xs$”. Este predicado se puede definir recursivamente en Haskell como la función pert:

pert :: Eq a => a -> [a] -> Bool
pert e [] = False
pert e (x:xs) = e==x || (pert e xs)
 
-- pert 3 [1,2,3,4,5] 
-- True

Por ejemplo, si queremos decir que “todos los elementos de la lista $xs$ son múltiplos de $3$” lo podemos expresar utilizando el cuantificador universal y el predicado que ya definimos:

Ejercicios resueltos - Semántica de Lógica de Predicados

Dada una lista de figuras $xs$ las siguientes propiedades, expresar formalmente y en Haskell utilizando los cuantificadores y los predicados y funciones ya definidas:

1.

Todas las figuras de $xs$ son rojas.

propA :: [Figura] -> Bool
 
propA [] = True
propA (x : xs) = roja x && propA xs
 
-- propA [Circulo Rojo 3, Cuadrado Azul 4, Triangulo Rojo 5]
-- False

2.

Todas las figuras de $xs$ son de tamaño menor a $5$.

propB :: [Figura] -> Bool
 
propB [] = True
propB (x : xs) = tamaño x < 5 && propB xs
 
-- propB [Circulo Rojo 3, Cuadrado Azul 4, Triangulo Rojo 5]
-- True

3.

Todos los triángulos de $xs$ son rojos.

propC :: [Figura] -> Bool
 
propC [] = True
propC (x : xs) = (triangulo x && roja x) && propC xs
 
-- propC [Circulo Rojo 3, Cuadrado Azul 4, Triangulo Rojo 5]
-- False

4.

Existe un cuadrado verde en $xs$.

propD :: [Figura] -> Bool
 
propD [] = False
propD (x : xs) = (cuadrado x && verde x) || propD xs
 
-- propD [Circulo Rojo 3, Cuadrado Azul 4, Triangulo Rojo 5]
-- False

5.

Todos los círculos de $xs$ son azules y de tamaño menor a $10$.

propE :: [Figura] -> Bool
 
propE [] = True
propE (x : xs) = (circulo x && azul x && tamaño x < 10) && propE xs
 
-- propE [Circulo Rojo 3, Cuadrado Azul 4, Triangulo Rojo 5]
-- False

6.

Ningún triángulo de $xs$ es azul.

propF :: [Figura] -> Bool
 
propF [] = True
propF (x : xs) = not (triangulo x && azul x) && propF xs
 
-- propF [Circulo Rojo 3, Cuadrado Azul 4, Triangulo Rojo 5]
-- True

7.

En $xs$ no hay círculos amarillos ni verdes.

propG :: [Figura] -> Bool
 
propG [] = True
propG (x : xs) = not (amarillo x) && not (verde x) && propG xs
 
-- propG [Circulo Rojo 3, Cuadrado Azul 4, Triangulo Rojo 5]
-- True

8.

En $xs$ no hay números pares.

propH :: [Int] -> Bool
 
propH [] = True
propH (x : xs) = not (par x) && propH xs
 
-- propH [1,3,5,7,9]
-- True

9.

En $xs$ todos los números son 0.

propI :: [Int] -> Bool
 
propI [] = True
propI (x : xs) = x == 0 && propI xs
 
-- propI [0,0,0,0,0]
-- True

Axiomas y Teoremas de Lógica de Predicados

Podemos utilizar los axiomas y teoremas de la lógica de predicados (junto a los de lógica proposicional) para demostrar propiedades sobre listas.

Axiomas:

A1 Intercambio entre rango y término: $\bigl \langle \; ∀x : R.x : T.x \; \bigr \rangle ≡ \bigl \langle \; ∀x : : R.x ⇒ T.x \; \bigr \rangle$

A2 Regla del Término del $∀$: $\bigl \langle \; ∀x : : T.x \; \bigr \rangle \land \bigl \langle \; ∀x : : U.x \; \bigr \rangle ≡ \bigl \langle \; ∀x : : T.x \land U.x \; \bigr \rangle$

A3 Distributividad de $\lor$ con $\forall$: $Z \lor \bigl \langle \; ∀x :: T.x \; \bigr \rangle ≡ \bigl \langle \; ∀x :: Z \lor T.x \; \bigr \rangle$

A4 Rango unitario de $∀$: $\bigl \langle \; ∀x : x = A : T.x \; \bigr \rangle ≡ \; T.A$

Donde $A$ representa una constante del universo.

A5 Definición de $∃$: $\bigl \langle \; ∃x : R.x : T.x \; \bigr \rangle ≡ \neg \bigl \langle \; ∀x : R.x : \neg T.x \; \bigr \rangle$

A6 Intercambio de cuantificadores del $\forall$: $\bigl \langle \; ∀x :: \bigl \langle \; ∀y :: T.x.y \; \bigr \rangle \; \bigr \rangle ≡ \bigl \langle \; ∀y :: \bigl \langle \; ∀x :: T.x.y \; \bigr \rangle \; \bigr \rangle$

Teoremas básicos del $∀$:

T1 Partición de rango del $∀$: $\bigl \langle \; ∀x : R.x \lor S.x : T.x \; \bigr \rangle ≡ \bigl \langle \; ∀x : R.x : T.x \; \bigr \rangle \land \bigl \langle \; ∀x : S.x : T.x \; \bigr \rangle$

T2 Instanciación del $∀$:

$\bigl \langle \; ∀x :: T.x \; \bigr \rangle ⇒ \; T.A$

$\bigl \langle \; ∀x :: T.x \; \bigr \rangle \equiv \bigl \langle \; ∀x :: T.x \; \bigr \rangle \land \; T.A$

Donde $A$ representa una constante del universo.

T3 Cambio de variable en el $∀$:

$\bigl \langle \; ∀x : R.x : T.x \; \bigr \rangle ≡ \bigl \langle \; ∀y : R.y : T.y \; \bigr \rangle$

(Si $x$ no ocurre libre en $T.y$ ni $y$ en $T.x$)

T4 Regla del término constante de $∀$:

$\bigl \langle \; ∀x :: C \; \bigr \rangle ≡ C$

Donde $C$ es constante.

T5 Rango vacío del $∀$:

$\bigl \langle \; ∀x : False : T.x \; \bigr \rangle ≡ False$

Teoremas básicos del $∃$:

T6 Intercambio entre rango y término del $∃$: $\bigl \langle \; ∃x : R.x : T.x \; \bigr \rangle ≡ \bigl \langle \; ∃x : : R.x \land T.x \; \bigr \rangle$

T7 Regla del término del $∃$: $\bigl \langle \; ∃x : : T.x \; \bigr \rangle \lor \bigl \langle \; ∃x : : S.x \; \bigr \rangle ≡ \bigl \langle \; ∃x : : T.x \lor S.x \; \bigr \rangle$

T8 Distributividad de $\land$ con $∃$: $Z \land \bigl \langle \; ∃x :: T.x \; \bigr \rangle ≡ \bigl \langle \; ∃x :: Z \land T.x \; \bigr \rangle$

T9 Rango unitario del $∃$: $\bigl \langle \; ∃x : x = A : T.x \; \bigr \rangle ≡ T.A$

Donde $A$ representa una constante del universo.

T10 Partición de rango de $∃$: $\bigl \langle \; ∃x : R.x \lor S.x : T.x \; \bigr \rangle ≡ \bigl \langle \; ∃x : R.x : T.x \; \bigr \rangle \lor \bigl \langle \; ∃x : S.x : T.x \; \bigr \rangle$

T11 Testigo:

$t.A ⇒ \bigl \langle \; ∃x :: T.x \; \bigr \rangle$

$\bigl \langle \; ∃x :: T.x \; \bigr \rangle \equiv t.A \lor \bigl \langle \; ∃x :: T.x \; \bigr \rangle$

Donde $A$ representa una constante del universo.

T12 Cambio de variable en el $∃$: $\bigl \langle \; ∃x : R.x : T.x \; \bigr \rangle ≡ \bigl \langle \; ∃y : R.y : T.y \; \bigr \rangle$

(Si $x$ no ocurre libre en $T.y$ ni $y$ en $T.x$)

T13 Regla del término constante de $∃$: $\bigl \langle \; ∃x :: C \; \bigr \rangle ≡ C$

Donde $C$ es constante

T14 Rango vacío del $∃$: $\bigl \langle \; ∃x : False : T.x \; \bigr \rangle ≡ False$

T15 Intercambio de cuantificadores del $∃$: $\bigl \langle \; ∃x :: \bigl \langle \; ∃y :: T.x.y \; \bigr \rangle \; \bigr \rangle ≡ \bigl \langle \; ∃y :: \bigl \langle \; ∃x :: T.x.y \; \bigr \rangle \; \bigr \rangle$

Ejercicios resueltos - Demostraciones con Axiomas y Teoremas

Mediante los axiomas y teoremas anteriormente presentados, demostrar las siguientes propiedades:

1.

Intercambio entre rango y término $∃$: $\bigl \langle \; ∃x : R.x : T.x \; \bigr \rangle ≡ \bigl \langle \; ∃x : : R.x ∧ T.x \; \bigr \rangle$.

$≡$ { Definición de $∃$}

$≡$ { Definición de $∃$, $x:=x, R.x:= True, T.x := R.x ∧ T.x$ }

$≡$ { Intercambio de rango y término de $∀, x:=x , R.x:=R.x, T.x:=¬T.x$ }

$≡$ { Definición de $∃$ }

$≡$ { Reflexividad de $≡$ }

2.

Regla del Término del $∀$ (bis): $\bigl \langle \; ∀x : R.x : T.x \; \bigr \rangle ∧ \bigl \langle \; ∀x : R.x : U.x \; \bigr \rangle ≡ \bigl \langle \; ∀x : R.x : T.x ∧ U.x \; \bigr \rangle.$

$≡$ {Intercambio de rango y término del para $∀$ , $\bigl \langle \; ∀x : R.x : T.x \; \bigr \rangle ≡ \bigl \langle \; ∀x :: R.x ⇒ T.x \; \bigr \rangle$}

$≡$ {Regla de termino de $∀$ }

$≡$ {Distributividad de $⇒$ con $∧$, $P ⇒ ( Q ∧ R ) ≡ (P ⇒ Q ) ∧ ( P ⇒ R )$ }

$≡$ {Relfex. de la $≡$ }

3.

Rango unitario: $\bigl \langle \; ∃x : x = A : T.x \; \bigr \rangle ≡ \; T.A$, donde $A$ representa una constante del universo

$≡$ {Definición de $∃$: $¬ \bigl \langle \; ∀x : R.x : ¬T.x \; \bigr \rangle$}

$≡$ {Intercambio de rango y término de $∀$: $\bigl \langle \; ∀x : R.x : T.x \; \bigr \rangle ≡ \bigl \langle \; ∀x :: R.x ⇒ T.x \; \bigr \rangle$}

$≡$ {Rango unitario de $∀$: $\bigl \langle \; ∀x :: R.x ⇒ T.x \; \bigr \rangle ≡ \; t.A$}

$≡$ {Doble negación $¬¬P ≡ P$}

$≡$ {Reflexividad de la equivalencia}

Verificación de Programas

La verificación de programas nos permite demostrar si una función cumple con su descripción formal (especificación) utilizando técnicas de inducción y cálculo de predicados.

Por ejemplo, en base a la siguiente función:

Y teniendo en cuenta la siguiente propiedad:

Podemos demostrar la siguiente fórmula por inducción:

Definimos el caso base ($xs = [ ]$):

≡{ Caso base de $soloCeros$ }

≡{ Elemento Neutro de $≡$, Propiedad de lista vacía }

≡{ Rango Vacío }

≡{ Reflexividad de $≡$ }

Definimos el paso inductivo ($xs = (x \;▹ \;xs)$):

≡{ Definición de $soloCeros$ }

≡{ Cambio de variable en el $∀$ }

≡{ Rango Unitario, Cambio de variable en el $∀$ }

≡{ Hipótesis Inductiva }

≡{ Reflexividad de $≡$ }