PDF de programación - LPO en Haskell

Lógica de primer orden en Haskell

Departamento de Ciencias de la Computación e Inteligencia Artificial

Facultad de Matemáticas

Trabajo Fin de Grado

Eduardo Paluzo Hidalgo

2

Me gustaría agradecer:
A mis padres y mi abuela estar siempre ahí,
facilitándome infinitamente la vida.
A mi profesora María del Carmen haberme
motivado a elegir matemáticas.
A mi tutor José Antonio la paciencia y dedica-
ción que ha demostrado, así como el haberme
dado la oportunidad de trabajar con él.

3

El presente Trabajo Fin de Grado se ha realizado en el Departamento de
Ciencias de la Computación e Inteligencia Artificial de la Universidad de
Sevilla.

Supervisado por

José Antonio Alonso Jiménez

4

Abstract

This final degree project consists in the implementation of First Order Logic theory
and algorithms in Haskell, a functional programming language. Furthermore, a re-
lation between maths and programming based on Curry-Howard correspondence is
established, giving an intuitive sort of examples. Moreover, it aims to give an intro-
duction to Haskell and other sources as git and doctest.

Esta obra está bajo una licencia Reconocimiento–NoComercial–CompartirIgual 2.5 Spain
de Creative Commons.

5

Se permite:

copiar, distribuir y comunicar públicamente la obra

hacer obras derivadas

Bajo las condiciones siguientes:

Reconocimiento. Debe reconocer los créditos de la obra de la manera especificada
por el autor.

No comercial. No puede utilizar esta obra para fines comerciales.

Compartir bajo la misma licencia. Si altera o transforma esta obra, o genera una
obra derivada, sólo puede distribuir la obra generada bajo una licencia idéntica a
ésta.

Al reutilizar o distribuir la obra, tiene que dejar bien claro los términos de la licencia de
esta obra.

Alguna de estas condiciones puede no aplicarse si se obtiene el permiso del titular de los
derechos de autor.

Esto es un resumen del texto legal (la licencia completa). Para ver una copia de es-
ta licencia, visite http://creativecommons.org/licenses/by-nc-sa/2.5/es/ o envie
una carta a Creative Commons, 559 Nathan Abbott Way, Stanford, California 94305,
USA.

6

Índice general

Introducción

9

1 Programación funcional con Haskell

13
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
Introducción a Haskell
. . . . . . . . . . . . . . . . . . . . . . . . 15
1.1.1 Comprensión de listas
. . . . . . . . . . . . . . . . . . . . . . . . 15
1.1.2
Funciones map y filter
1.1.3 n-uplas . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
1.1.4 Conjunción, disyunción y cuantificación . . . . . . . . . . . . . . 17
1.1.5 Plegados especiales foldr y foldl . . . . . . . . . . . . . . . . . . . 18
1.1.6 Teoría de tipos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
1.1.7 Generador de tipos en Haskell: Descripción de funciones . . . . 21

. .

.

2 Sintaxis y semántica de la lógica de primer orden

25
Representación de modelos . . . . . . . . . . . . . . . . . . . . . . . . . . 25
Lógica de primer orden en Haskell
. . . . . . . . . . . . . . . . . . . . . 28
Evaluación de fórmulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
Términos funcionales .
2.4.1 Generadores .
.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
2.4.2 Otros conceptos de la lógica de primer orden . . . . . . . . . . . 43

1.1

2.1
2.2
2.3
2.4

3.1
3.2
3.3

3.4

3 El método de los tableros semánticos

.
.
.

.

.

.
.
.

.
.
.

.
.
.

47
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
.
.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
Formas normales
. . . . . . . . . . . . . . . . . . . . . . . . . . . 54
Forma rectificada . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
Forma normal prenexa . . . . . . . . . . . . . . . . . . . . . . . . 60
Forma normal prenexa conjuntiva . . . . . . . . . . . . . . . . . . 61
Forma de Skolem . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 65

Sustitución . .
Unificación . .
Skolem .
.
3.3.1
3.3.2
3.3.3
3.3.4
3.3.5
Tableros semánticos .

.

7

8

Índice general

4 Modelos de Herbrand

77
Universo de Herbrand . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
4.1
Base de Herbrand .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
4.2
4.3
Interpretacion de Herbrand . . . . . . . . . . . . . . . . . . . . . . . . . 85
4.4 Modelos de Herbrand . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
Consistencia mediante modelos de Herbrand . . . . . . . . . . . . . . . 88
4.5
4.6
Extensiones de Herbrand . . . . . . . . . . . . . . . . . . . . . . . . . . . 88

.

.

5 Resolución en lógica de primer orden

.

5.1
5.2
5.3

5.4

.

.

.

91
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
Forma clausal .
Interpretación y modelos de la forma clausal
. . . . . . . . . . . . . . . 94
Resolución proposicional . . . . . . . . . . . . . . . . . . . . . . . . . . . 98
5.3.1 Resolvente binaria . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
Resolución de primer orden . . . . . . . . . . . . . . . . . . . . . . . . . 101
5.4.1
Separación de variables . . . . . . . . . . . . . . . . . . . . . . . . 101
5.4.2 Resolvente binaria . . . . . . . . . . . . . . . . . . . . . . . . . . . 102

6 Correspondencia de Curry-Howard

105

A Implementación alternativa de la sustitución y unificación

111
A.1
Librería Data.Map .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 111
A.2
Sustitución con la librería Data.Map . . . . . . . . . . . . . . . . . . . . . 113
A.3 Unificación con la librería Data.Map . . . . . . . . . . . . . . . . . . . . 116

.

.

.

119
B Trabajando con GitHub
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119
Crear una cuenta .
.
.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 119
Crear un repositorio .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 119
.
.
Conexión .
. .
Pull y push . .
.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 120
.
Ramificaciones (“branches”) . . . . . . . . . . . . . . . . . . . . . . . . . 121

B.1
B.2
B.3
B.4
B.5

.
.

.
.

.
.

C Usando Doctest

Bibliografía

Indice de definiciones

123

126

128

Introducción

La lógica de primer orden o lógica de predicados nace como una extensión de la
lógica proposicional ante algunas carencias que ésta presenta. La lógica proposicional
tiene como objetivo modelizar el razonamiento y nos aporta una manera de formali-
zar las demostraciones. El problema surge cuando aparecen propiedades universales
o nos cuestionamos la existencia de elementos con una cierta propiedad, es decir, apa-
recen razonamientos del tipo

Todos los sevillanos van a la feria.
Yo soy sevillano.
Por lo tanto, voy a la feria.

A pesar de ser yo una clara prueba de que la proposición no es cierta, sí que se infieren
las carencias de la lógica proposicional, la ausencia de cuantificadores.

En este trabajo se pretende realizar una implementación en Haskell de la teoría
impartida en la asignatura Lógica matemática y fundamentos 1 ([3]) del grado en ma-
temáticas. Para ello, se lleva a cabo la adaptación de los programas del libro de J. van
Eijck Computational semantics and type theory 2 ([15]) y su correspondiente teoría.

Se ha comenzado con una introducción a Haskell(1) a través de la definición de
funciones y numerosos ejemplos. Esto lleva a introducir las funciones básicas, la teoría
de tipos y la teoría de generadores. De esta manera, se establece la base de conocimien-
tos propios de la programación que van más allá de la lógica y que son necesarios para
la implementación.

A continuación, en el capítulo sobre sintaxis y semántica de la lógica de primer
orden (2), ilustramos la utilidad de la lógica para dar una representación del conoci-
miento proponiendo un modelo de clasificación botánica. Se construyen los tipos de
datos abstractos que sirven de vehículo en la representación de fórmulas y que son
base de las implementaciones en los restantes capítulos. También se definen la eva-
luación de fórmulas por una interpretación y los términos funcionales, extendiendo el

1https://www.cs.us.es/~jalonso/cursos/lmf-15
2http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.467.1441&rep=rep1&type=

pdf

9

10

Índice general

lenguaje y dando, posteriormente, la construcción de generadores de fórmulas para,
en caso necesario, poder hacer comprobaciones con QuickCheck.

Ya asentadas las bases de la lógica y teniendo un suelo en el que sostenernos, se
trabaja con los tableros semánticos (3). Dicho capítulo tiene como objetivo implemen-
tar el método de tableros, un algoritmo para la prueba de teoremas y búsqueda de
modelos. Para la definición del algoritmo se requiere de distintas definiciones previas:

Sustitución: Nos permite llevar a cabo sustituciones de variables libres por tér-
minos.

Unificación: Se basa en la posibilidad de sustituir términos en varias fórmulas
para unificarlas; es decir, que después de la sustitución sean sintácticamente
iguales. Para ello determinamos tanto su existencia como generamos la lista de
unificadores.

Forma de Skolem: Se trata de una forma de representación de una fórmula dada
que se obtiene a partir de una serie de reglas, a través de las cuales se consi-
guen representaciones equiconsistentes unas de otras de la misma fórmula. En
el proceso de definición de la forma de Skolem se definen las formas normales,
forma rectificada, forma normal prenexa y forma normal prenexa conjuntiva. És-
tas además son necesarias para la definición en un capítulo posterior de la forma
clausal.

Posteriormente hablamos sobre un método constructivo para generar interpretacio-
nes de fórmulas o conjuntos de fórmulas, es lo que llamamos modelos de Herbrand
(4), que debe su nombre al matemático francés Jacques Herbrand. Además, es un méto-
do para determinar la consistencia de un conjunto de cláusulas, pues