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 \(≡\) }