31 agosto 2020 – Vestigium

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

PorJosé A. Alonso 31 agosto 20201 septiembre 2020

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)

PorJosé A. Alonso 31 agosto 202031 agosto 2020

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

mcd(m,n) = n

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

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

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 la sesión en Lean Web,
al código,
al libro “DAO con Lean” y
al repositorio en GitHub “DAO con Lean”.

A continuación, se muestra el vídeo