Calculo Lambda
Páginas: 356 (88978 palabras)
Publicado: 13 de octubre de 2012
Jean-Louis Krivine
LAMBDA-CALCULUS TYPES AND MODELS
Translated from french by Ren´ Cori e
To my daughter
Contents
Introduction 1 Substitution and beta-conversion Simple substitution . . . . . . . . . . Alpha-equivalence and substitution . . Beta-conversion . . . . . . . . . . . . Eta-conversion . . . . . . . . . . . . 5 7 8 12 17 23 29 29 31 34 38
. . . .
. . . .
. . . .. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
2 Representation of recursive functions Head normal forms . . . . . . . . . . . . Representable functions . . . . . . . . . . Fixed point combinators . . . . . . . . . The second fixed point theorem . . . . . .
. . . .
. . . .
. . . .
. . . .. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
3 Intersection type systems 41 System DΩ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 System D . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 Typings for normal terms . . . . . . . . . . . . . . . . . . . . . . . 55 4 Normalization and standardizationTypings for normalizable terms . . . . . Strong normalization . . . . . . . . . . βI-reduction . . . . . . . . . . . . . . The λI-calculus . . . . . . . . . . . . βη-reduction . . . . . . . . . . . . . . The finite developments theorem . . . . The standardization theorem . . . . . . 5 The B¨hm theorem o 3 61 61 69 70 72 74 77 81 87
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
4 6 Combinatory logic
Combinatory algebras . . Extensionality axioms . . Curry’s equations . . . . Translation of λ-calculus
CONTENTS 95 95 98 101 105
. . . .
. . . .
. . . .
. . . .
. . . .. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
7 Models of lambda-calculus Functional models . . . . . . . . . . . . . Spaces of continuous increasing functions . Spaces of initial segments . . . . . . . . . Applications . . . . . . . . . . . . .. . . Retractions . . . . . . . . . . . . . . . . Qualitative domains and stable functions . 8 System F
Definition of system F types . . . Typing rules for system F . . . . The strong normalization theorem Data types in system F . . . . . . Positive second order quantifiers .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
111 . 111 . 116 . 117 . 125 . 130 . 135 147 . 147 . 148 . 153 . 155 . 161 167 . 167 . 174 . 181 . 184 . 188
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . .. .
9 Second order functional arithmetic Second order predicate calculus . . . . . System F A2 . . . . . . . . . . . . . . . Realizability . . . . . . . . . . . . . . . Data types . . . . . . . . . . . . . . . Programming in F A2 . . . . . . . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
.. . . .
. . . . .
. . . . .
10 Representable functions in system F 195 G¨del’s ¬-translation . . . . . . . . . . . . . . . . . . . . . . . . . 198 o Undecidability of strong normalization . . . . . . . . . . . . . . . . 201 Bibliography 205
INTRODUCTION
The lambda-calculus was invented in the early 1930’s, by A. Church, and has been considerably developed since then. This book is...
LAMBDA-CALCULUS TYPES AND MODELS
Translated from french by Ren´ Cori e
To my daughter
Contents
Introduction 1 Substitution and beta-conversion Simple substitution . . . . . . . . . . Alpha-equivalence and substitution . . Beta-conversion . . . . . . . . . . . . Eta-conversion . . . . . . . . . . . . 5 7 8 12 17 23 29 29 31 34 38
. . . .
. . . .
. . . .. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
2 Representation of recursive functions Head normal forms . . . . . . . . . . . . Representable functions . . . . . . . . . . Fixed point combinators . . . . . . . . . The second fixed point theorem . . . . . .
. . . .
. . . .
. . . .
. . . .. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
3 Intersection type systems 41 System DΩ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 System D . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 Typings for normal terms . . . . . . . . . . . . . . . . . . . . . . . 55 4 Normalization and standardizationTypings for normalizable terms . . . . . Strong normalization . . . . . . . . . . βI-reduction . . . . . . . . . . . . . . The λI-calculus . . . . . . . . . . . . βη-reduction . . . . . . . . . . . . . . The finite developments theorem . . . . The standardization theorem . . . . . . 5 The B¨hm theorem o 3 61 61 69 70 72 74 77 81 87
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
4 6 Combinatory logic
Combinatory algebras . . Extensionality axioms . . Curry’s equations . . . . Translation of λ-calculus
CONTENTS 95 95 98 101 105
. . . .
. . . .
. . . .
. . . .
. . . .. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
7 Models of lambda-calculus Functional models . . . . . . . . . . . . . Spaces of continuous increasing functions . Spaces of initial segments . . . . . . . . . Applications . . . . . . . . . . . . .. . . Retractions . . . . . . . . . . . . . . . . Qualitative domains and stable functions . 8 System F
Definition of system F types . . . Typing rules for system F . . . . The strong normalization theorem Data types in system F . . . . . . Positive second order quantifiers .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
111 . 111 . 116 . 117 . 125 . 130 . 135 147 . 147 . 148 . 153 . 155 . 161 167 . 167 . 174 . 181 . 184 . 188
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . .. .
9 Second order functional arithmetic Second order predicate calculus . . . . . System F A2 . . . . . . . . . . . . . . . Realizability . . . . . . . . . . . . . . . Data types . . . . . . . . . . . . . . . Programming in F A2 . . . . . . . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
.. . . .
. . . . .
. . . . .
10 Representable functions in system F 195 G¨del’s ¬-translation . . . . . . . . . . . . . . . . . . . . . . . . . 198 o Undecidability of strong normalization . . . . . . . . . . . . . . . . 201 Bibliography 205
INTRODUCTION
The lambda-calculus was invented in the early 1930’s, by A. Church, and has been considerably developed since then. This book is...
Leer documento completo
Regístrate para leer el documento completo.