Lambda

El λ–c´lculo (sin tipos y con tipos) a

Blas Carlos Ruiz Jim´nez† e Pablo Guerrero Garc´ ıa‡ †Dpto. de Lenguajes y Ciencias de la Computaci´n o ‡Dpto. de Matem´tica Aplicada a Universidad de M´laga a Pza. El Ejido s/n, 29013–M´laga, Espa˜a a n e–mails blas@lcc.uma.es pablito@lcc.uma.es fax †34–5–2131397 ‡34–5–2132766

6th March 2002

ii

Contents
I El λ–c´lculo sin tipos a 1
3 3 6 7 99 9 10 12 12 14 15 15 19 22 25 25 27 30 35 35 36

0 Lambda expresiones 0.0 0.1 0.2 Sintaxis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Variables libres y asociadas . . . . . . . . . . . . . . . . . . . . . Subt´rminos y contextos . . . . . . . . . . . . . . . . . . . . . . . e

1 Sem´ntica operacional a 1.0 Evaluaci´n de λ–expresiones . . . . . . . . . . . . . . . . . . .. . o 1.0.0 1.0.1 1.1 1.1.0 1.1.1 1.2 1.2.0 1.2.1 1.3 δ–reducci´n . . . . . . . . . . . . . . . . . . . . . . . . . . o β–conversi´n . . . . . . . . . . . . . . . . . . . . . . . . . o Relaciones definibles en Λ . . . . . . . . . . . . . . . . . . λ–teor´ ıas . . . . . . . . . . . . . . . . . . . . . . . . . . . Convenio de variables y concepto de sustituci´n . . . . . . o La sustituci´n frente alas relaciones en Λ . . . . . . . . . o

Reducci´n en Λ . . . . . . . . . . . . . . . . . . . . . . . . . . . . o

Sustituciones y α–equivalencias . . . . . . . . . . . . . . . . . . .

Eta–conversi´n y extensionalidad . . . . . . . . . . . . . . . . . . o

2 Formas normales 2.0 2.1 2.2 2.3 El concepto de forma normal . . . . . . . . . . . . . . . . . . . . Confluencia . . . . . . . . . . .. . . . . . . . . . . . . . . . . . . Los teoremas de Church–Rosser . . . . . . . . . . . . . . . . . . . Formas normales por la cabeza . . . . . . . . . . . . . . . . . . . ´ 2.3.0 Ordenes de reducci´n . . . . . . . . . . . . . . . . . . . . o 2.3.1 El teorema de estandarizaci´n . . . . . . . . . . . . . . . . o iii

iv 2.4

CONTENTS Formas d´bil–normales . . . . . . . . . . . . . . . . . .. . . . . . e 42 45 45 45 46 47 47 50 51 53 53 55 55 56 61 61 61 62 62 63 65 66 66 66 68 69 69 70 71 71 72 73

3 Teor´ de combinadores ıa 3.0 Combinadores . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.0.0 3.0.1 3.1 3.1.0 3.1.1 3.1.2 3.1.3 3.1.4 3.2 3.2.0 3.2.1 Los combinadores est´ndares . . . . . . . . . . . . . . . . a Potencias y potencias de K . . . . . . . . . . . . . . . . .Fundamentos de LC . . . . . . . . . . . . . . . . . . . . . Relaci´n entre λ–t´rminos y t´rminos combinatorios . . . o e e Reducci´n en forma perezosa . . . . . . . . . . . . . . . . o Generadores y bases . . . . . . . . . . . . . . . . . . . . . Equivalencia entre λC y LC . . . . . . . . . . . . . . . . . Expresando la recursi´n . . . . . . . . . . . . . . . . . . . o Combinadores para puntosfijos . . . . . . . . . . . . . . .

La teor´ de combinadores . . . . . . . . . . . . . . . . . . . . . . ıa

Puntos fijos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

4 Lambda definibilidad 4.0 4.1 Operaciones l´gicas . . . . . . . . . . . . . . . . . . . . . . . . . . o 4.0.0 4.1.0 4.1.1 4.1.2 4.1.3 4.2 4.2.0 4.2.1 4.3 4.3.0 4.3.1 Constantes y operaciones l´gicas . . . . . . . . .. . . . . o Sistemas de numerales y numerales de Church . . . . . . Computabilidad y λ–definibilidad . . . . . . . . . . . . . . . . . . Funciones λ–definibles y recursivas. Teorema de Kleene . Aritm´tica y Numerales de Church . . . . . . . . . . . . . e Extensi´n del λC con la aritm´tica . . . . . . . . . . . . . o e λ–definibilidad de las funciones b´sicas para listas . . . . a Las listas en un λCcon constantes . . . . . . . . . . . . . Un autoint´rprete para el λC . . . . . . . . . . . . . . . . e Aplicaciones de la autointerpretaci´n . . . . . . . . . . . . o

Listas en el λC puro . . . . . . . . . . . . . . . . . . . . . . . . .

Autointerpretaci´n en el λC . . . . . . . . . . . . . . . . . . . . . o

5 Solubilidad 5.0 5.1 5.2 Introducci´n . . . . . . . . . . . . . . . . . ....