En clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentando las soluciones de los 8 primeros ejercicios de evaluación de la 14ª relación sobre aplicaciones de la programación funcional con listas infinitas.
Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2015: Aplicaciones de la programación funcional con listas infinitas”
En la clase de hoy del curso de Lógica Informática” se ha presentado la resolución en la lógica de primer orden como ampliación del presentado en el tema 5
para la lógica proposicional.
Las principales diferencias se encuentran en la unificación, separación de variables y factorización.
Las transparencias de esta clase son las del tema 12
En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado el tema 13 sobre programas interativos.
Se ha empezado observando un procedimiento que pide que se escriba una cadena y devuelve su longitud:
|
1 2 3 4 5 6 7 |
longitudCadena :: IO () longitudCadena = do putStr "Escribe una cadena: " xs <- getLine putStr "La cadena tiene " putStr (show (length xs)) putStrLn " caracteres" |
A continuación se han estudiado los elementos implicados en el procedimiento anterior: el tipo de las acciones de entrada/salida (IO), las acciones básicas (getChar, putChar y return), la secuenciación de acciones con do y la definición de algunos procedimientos del preludio (getLine, putStr, putStrLn, y sequence_).
Como aplicación se han estudiado dos programas:
Finalmente se ha estudiado cómo representar gráficamente funciones con gnuplot. Concretamente se ha visto
plotFunc),linearScale),EPS, Grid, Title, Key y XLabel),plotList),plotFuncs),plotParamFunc) yplotFunc3d).La documentación de las funciones anteriores y otras funciones se encuentra en la página de la librería Graphics.Gnuplot.Simple.
En la clase de hoy del curso de Razonamiento automático se ha presentado cómo se puede demostrar propiedades de programas funcionales con Isabelle/HOL.
Para ello, se ha visto cómo representar en Isabelle/HOL las demostraciones de propiedades de programas estudiadas en el tema 8 del curso de Informática.
Los métodos de demostración utilizados son razonamiento ecuacional, inducción sobre los números naturales, inducción sobre listas e inducción sobre esquemas correspondientes a definiciones recursivas.
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2015: Razonamiento estructurado sobre programas con Isabelle/HOL”
En la primera parte de la clase de hoy del curso de Razonamiento automático se ha comentado las soluciones de la 2ª relación de ejercicios cuyo objetivo es demostrar automáticamente con Isabelle/HOL propiedades de programas.
Los ejercicios y sus soluciones se muestran a continuación
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 |
header {* R2: Razonamiento automático sobre programas *} theory R2 imports Main begin text {* --------------------------------------------------------------- Ejercicio 1. Definir la función sumaImpares :: nat ⇒ nat tal que (sumaImpares n) es la suma de los n primeros números impares. Por ejemplo, sumaImpares 5 = 25 ------------------------------------------------------------------ *} fun sumaImpares :: "nat ⇒ nat" where "sumaImpares 0 = 0" | "sumaImpares (Suc n) = sumaImpares n + (2*n+1)" value "sumaImpares 5" -- "= 25" text {* --------------------------------------------------------------- Ejercicio 2. Demostrar que sumaImpares n = n*n ------------------------------------------------------------------- *} lemma "sumaImpares n = n*n" by (induct n) auto text {* --------------------------------------------------------------- Ejercicio 3. Definir la función sumaPotenciasDeDosMasUno :: nat ⇒ nat tal que (sumaPotenciasDeDosMasUno n) = 1 + 2^0 + 2^1 + 2^2 + ... + 2^n. Por ejemplo, sumaPotenciasDeDosMasUno 3 = 16 ------------------------------------------------------------------ *} fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where "sumaPotenciasDeDosMasUno 0 = 2" | "sumaPotenciasDeDosMasUno (Suc n) = sumaPotenciasDeDosMasUno n + 2^(n+1)" value "sumaPotenciasDeDosMasUno 3" -- "= 16" text {* --------------------------------------------------------------- Ejercicio 4. Demostrar que sumaPotenciasDeDosMasUno n = 2^(n+1) ------------------------------------------------------------------- *} lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)" by (induct n) auto text {* --------------------------------------------------------------- Ejercicio 5. Definir la función copia :: nat ⇒ 'a ⇒ 'a list tal que (copia n x) es la lista formado por n copias del elemento x. Por ejemplo, copia 3 x = [x,x,x] ------------------------------------------------------------------ *} fun copia :: "nat ⇒ 'a ⇒ 'a list" where "copia 0 x = []" | "copia (Suc n) x = x # copia n x" value "copia 3 x" -- "= [x,x,x]" text {* --------------------------------------------------------------- Ejercicio 6. Definir la función todos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool tal que (todos p xs) se verifica si todos los elementos de xs cumplen la propiedad p. Por ejemplo, todos (λx. x>(1::nat)) [2,6,4] = True todos (λx. x>(2::nat)) [2,6,4] = False ------------------------------------------------------------------ *} fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where "todos p [] = True" | "todos p (x#xs) = (p x ∧ todos p xs)" value "todos (λx. x>(1::nat)) [2,6,4]" -- "= True" value "todos (λx. x>(2::nat)) [2,6,4]" -- "= False" text {* --------------------------------------------------------------- Ejercicio 7. Demostrar que todos los elementos de (copia n x) son iguales a x. ------------------------------------------------------------------- *} lemma "todos (λy. y=x) (copia n x)" by (induct n) auto text {* --------------------------------------------------------------- Ejercicio 8. Definir la función factR :: nat ⇒ nat tal que (factR n) es el factorial de n. Por ejemplo, factR 4 = 24 ------------------------------------------------------------------ *} fun factR :: "nat ⇒ nat" where "factR 0 = 1" | "factR (Suc n) = Suc n * factR n" value "factR 4" -- "= 24" text {* --------------------------------------------------------------- Ejercicio 9. Se considera la siguiente definición iterativa de la función factorial factI :: "nat ⇒ nat" where factI n = factI' n 1 factI' :: nat ⇒ nat ⇒ nat" where factI' 0 x = x factI' (Suc n) x = factI' n (Suc n)*x Demostrar que, para todo n y todo x, se tiene factI' n x = x * factR n ------------------------------------------------------------------- *} fun factI' :: "nat ⇒ nat ⇒ nat" where "factI' 0 x = x" | "factI' (Suc n) x = factI' n (x * Suc n)" fun factI :: "nat ⇒ nat" where "factI n = factI' n 1" value "factI 4" -- "= 24" lemma fact: "factI' n x = x * factR n" by (induct n arbitrary: x) (auto simp del: mult_Suc) text {* --------------------------------------------------------------- Ejercicio 10. Demostrar que factI n = factR n ------------------------------------------------------------------- *} corollary "factI n = factR n" by (simp add: fact) text {* --------------------------------------------------------------- Ejercicio 11. Definir, recursivamente y sin usar (@), la función amplia :: 'a list ⇒ 'a ⇒ 'a list tal que (amplia xs y) es la lista obtenida añadiendo el elemento y al final de la lista xs. Por ejemplo, amplia [d,a] t = [d,a,t] ------------------------------------------------------------------ *} fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where "amplia [] y = [y]" | "amplia (x#xs) y = x # amplia xs y" value "amplia [d,a] t" -- "= [d,a,t]" text {* --------------------------------------------------------------- Ejercicio 12. Demostrar que amplia xs y = xs @ [y] ------------------------------------------------------------------- *} lemma "amplia xs y = xs @ [y]" by (induct xs) auto end |