Menu Close

Mes: agosto 2020

PFH: Funciones de orden superior en Haskell (Parte 1 de 3)

He añadido a la lista Programación funcional con Haskell el vídeo Funciones de orden superior en Haskell (Parte 1 de 3) en el que se ha iniciado el estudio de las funciones de orden superior.

En primer lugar, se ha explicado en qué consiste lo de orden superior.

En segundo lugar, se han estudiado las funciones de procesamiento de listas (map) y de filtrado (filter) definiéndolas por comprensión y por recursión. También se ha puesto un ejemplo de utilización de dichas funciones para definir nuevas funciones.

Finalmente, se han explicado otras funciones predefinidas de orden superior: all, any, takeWhile y dropWhile. También se ha comentado cómo buscarlas en Hoogle y cómo consultar sus definiciones.

El vídeo es

Los apuntes correspondientes son

Una versión interactiva de los apuntes en IHaskell se encuentra aquí.

ForMatUS: El máximo común divisor de m y n es igual a m si, y sólo si, m divide a n (en Lean)

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo El máximo común divisor de m y n es igual a m si, y sólo si, m divide a n (en Lean) en el que se comenta la prueba en Lean de la siguiente propiedad de los números naturales: el máximo común divisor de a y b es igual a a si, y sólo si, a divide a b. Más concretamente,

Sean m y n son números naturales. Entonces, son equivalentes

  1. mcd(m,n) = n
  2. m divide a n

Su enunciado en Lean es

import data.nat.gcd
 
open nat
 
variables (a b : )
 
example : a ∣ b  gcd a b = a :=
sorry

En la demostración se utilizan los siguientes propiedades de los números naturales:

dvd_refl:      a ∣ a
dvd_antisymm : a ∣ b  b ∣ a  a = b 
dvd_gcd_iff :  c ∣ gcd a b  c ∣ a  c ∣ b
gcd_dvd :      gcd a b ∣ a  gcd a b ∣ b

Los enlaces correspondientes son:

A continuación, se muestra el vídeo

ForMatUS: Formulación equivalente de lemas con dos hipótesis

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo Formulación equivalente de lemas con dos hipótesis en el que se comentan 5 demostraciones en Lean de la fórmula

(P ∧ Q → R) ↔ (P → (Q → R))

usando distintos estilos de prueba,

Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.

A continuación, se muestra el vídeo

ForMatUS: Conmutatividad de la conjunción en Lean

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo Conmutatividad de la conjunción en Lean en el que se comentan 9 demostraciones en Lean de la conmutatividad de la conjunción usando los distintos estilos: aplicativa con táctica, declarativa estructurada, funcional con término de prueba y automática.

Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.

A continuación, se muestra el vídeo

ForMatUS: Conectivas y desigualdades en Lean

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo Conectivas y desigualdades en Lean en el se comentan las demostraciones en Lean de algunas de las propiedades de las desigualdades de los números reales estudiadas en vídeos anteriores, pero formuladas con conectivas. Concretamente, se demuestran las 5 propiedades siguientes:

Sean a, b y c números reales.

  1. 0 ≤ a → b ≤ a + b
  2. 0 ≤ b → a ≤ a + b
  3. (0 ≤ a ∧ 0 ≤ b) → 0 ≤ a + b
  4. 0 ≤ a → (0 ≤ b → 0 ≤ a + b)
  5. Si (0 ≤ a ∧ 0 ≤ b) → 0 ≤ a + b, entonces 0 ≤ a → (0 ≤ b → 0 ≤ a + b)

Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.

A continuación, se muestra el vídeo

PFH: Definiciones por recursión en Haskell (Parte 2 de 2)

He añadido a la lista Programación funcional con Haskell el vídeo Definiciones por recursión en Haskell (Parte 2 de 2) en el que se completa el estudio de las definiciones por recursión en Haskell comenzado en el vídeo anterior. Concretamente, hemos visto ejemplos de

  • recursión sobre varios argumento,
  • recursión múltiple y
  • de recursión mutua.

El vídeo es

Los apuntes correspondientes son

Una versión interactiva de los apuntes en IHaskell se encuentra aquí.

PFH: Definiciones por recursión en Haskell (Parte 1 de 2)

He añadido a la lista Programación funcional con Haskell el vídeo Definiciones por recursión en Haskell (Parte 1 de 2) en el que se e,pieza el estudio de las definiciones por recursión en Haskell. Concretamente, hemos visto ejemplos de

  • recursión sobre los números naturales y
  • recursión sobre listas.

El vídeo es

Los apuntes correspondientes son

Una versión interactiva de los apuntes en IHaskell se encuentra aquí.