Vestigium

I1M2018: El tipo abstracto de datos de las colas en Haskell

PorJosé A. Alonso 21 marzo 201923 marzo 2019

En la primera parte de la clase de hoy del curso de Informática de 1º del Grado en Matemáticas hemos continuado el estudio de los tipos abstractos (TAD) de datos en Haskell y hemos presentados el TAD de las colas siguiendo el esquema usado para el TAD de las pilas.

Se ha comenzado la modelización de las pilas observando la forma de introducir o extraer sus elementos. El resultado de la modelización es la especificación del TAD: su signatura y propiedades características.

A continuación se han estudiados dos implementaciones (una basada listas y la otra en pares de listas) juntos con sus complejidades.

Se ha vuelto a resaltar la forma de conseguir la abstracción de tipos en Haskell mediante módulos y exportación sólo de la signatura.

Finalmente, usando QuickCheck se comprueban las propiedades características del TAD de las colas.

Los apuntes correspondientes a la clase son los del tema 15

LMF2018: Ejercicios de deducción natural en lógica de primer orden con Isabelle/HOL

PorJosé A. Alonso 20 marzo 201925 marzo 2019

En la clase de hoy del curso Lógica matemática y fundamentos se ha explicado demostraciones en Isabelle/HOL de los ejercicios 10, 13, 20 y 27 de la relación 6.

LMF2018: Deducción natural en lógica de primer orden

PorJosé A. Alonso 19 marzo 2019

En la clase de hoy del curso Lógica matemática y fundamentos se presentado la ampliación del cálculo de deducción natural proposional para tratar los cuantificadores y la igualdad. Se han comentado distintas equivalencias lógicas y se han demostrado por deducción natural las principales equivalencias.

Las transparencias de esta clase son las del tema 4.

A la vez que se han ido haciendo las demostraciones se ha explicado cómo hacerlas en Isabelle/HOL.

La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “LMF2018: Deducción natural en lógica de primer orden”

I1M2018: El tipo abstracto de datos de las pilas en Haskell

PorJosé A. Alonso 19 marzo 201923 marzo 2019

En la primera parte de la clase de hoy del curso de Informática de 1º del Grado en Matemáticas hemos empezado el estudio de los tipos abstractos (TAD) de datos en Haskell.

Después de tratar de la abstracción, los TAD en general y su analogía con las estructuras algebraicas, se ha estudiado el primero de los TAD: las pilas.

A continuación se han estudiados dos implementaciones (una basada en tipos de datos algebraicos y otra en listas) y las complejidades de las operaciones.

Un punto importante es la forma de conseguir la abstracción de tipos en Haskell mediante módulos y exportación sólo de la signatura.

Finalmente, usando QuickCheck se comprueban las propiedades características del TAD de las pilas.

Los apuntes correspondientes a la clase son los del tema 14

I1M2018: De la matemática a la máquina

PorJosé A. Alonso 15 marzo 201918 marzo 2019

En la segunda parte de la clase de hoy del curso de Informática de 1º del Grado en Matemáticas se ha comentado cómo los se pueden representar los conceptos matemáticos en los ordenadores.

Para ello se ha visto cómo la definición de factorial se puede definir en distintos paradigmas desde la matemática al código máquina. Las definiciones consideradas han sido

En matemáticas

     n
n! = ∏ k 
    k=1

n! = ∏ k

k=1

En programación funcional (Haskell).

factorial :: Int -> Int
factorial n = product [1..n]

1 2	factorial :: Int -> Int factorial n = product [1..n]

En programación imperativa (C).

int factorial(int n)
{
    int ret = 1;

    while (n > 1)
    {
        ret *= n;
        n--;
    }

    return ret;
}

int factorial(int n)

{

int ret = 1;

while (n > 1)

{

ret *= n;

n--;

}

return ret;

}

En ensamblador.

factorial:
    mov rdi, 1

  .loop:
    cmp rax, 1
    jle .done

    imul rdi, rax
    dec rax

    jmp .loop

  .done:
    ret

factorial:

mov rdi, 1

.loop:

cmp rax, 1

jle .done

imul rdi, rax

dec rax

jmp .loop

.done:

ret

En código máquina.

48 bf 01 00 00 00 00 00 00 00 48 3d 01 00 00 00 7e 0c 48 0f af f8 48 ff
c8 e9 ec ff ff ff c3

1 2	48 bf 01 00 00 00 00 00 00 00 48 3d 01 00 00 00 7e 0c 48 0f af f8 48 ff c8 e9 ec ff ff ff c3

La exposición se ha basado en el artículo From math to machine: translating a function to machine code de Brian Steffens.