Download fdldp - Teoría de la computación

BENEMÉRITA UNIVERSIDAD AUTÓNOMA DE PUEBLA
VICERRECTORÍA DE DOCENCIA
DIRECCIÓN GENERAL DE EDUCACIÓN SUPERIOR
UNIDAD ACADÉMICA:
FACULTAD DE CIENCIAS DE LA COMPUTACIÓN
CARRERA:
LICENCIATURA EN CIENCIAS DE LA COMPUTACIÓN
NÚMERO
DE CÓDIGO Y NOMBRE DEL CURSO:
NUEVA 7
FUNDAMENTOS DE LENGUAJES DE PROGRAMACIÓN.
FECHA DE ELABORACION DEL CURSO:
ABRIL 2000
NIVEL
EN QUE SE UBICA EN EL MAPA CURRICULAR:
NIVEL FORMATIVO
NOMBRE(S)
DE EL (LOS) PROFESORES QUE ELABORARON EL PROGRAMA:
JOSÉ DE JESÚS LAVALLE MARTÍNEZ
JESÚS GARCÍA FERNÁNDEZ
GUILLERMO DE ITA LUNA
DAVID EDUARDO PINTO AVENDAÑO
JOSÉ JUAN PALACIOS PÉREZ
PEDRO VARGAS GARCÍA
OLIVA LÓPEZ PÉREZ
BENEMÉRITA UNIVERSIDAD AUTÓNOMA DE PUEBLA
ESQUEMA DEL CURSO
TÍTULO DEL CURSO
FUNDAMENTOS DE LENGUAJES DE PROGRAMACIÓN.
CÓDIGO
NUEVA 7
CRÉDITOS
10
H.T. 5
H. P. 0
PRERREQUISITOS
CCO 500
OBJETIVOS GENERALES DEL CURSO
Que el estudiante aprenda los fundamentos en los que se sustenta la semántica de los
lenguajes de programación, cómo se pueden formalizar las nociones de evaluación, tipos, validez,
completez y poder expresivo de un lenguaje.
OBJETIVOS ESPECÍFICOS
El estudiante aprenderá mediante los lenguajes PCF y While las semánticas que se pueden
definir para ellos, las diferencias en cuanto a abstracción requerida, su equivalencia y el impacto en
el diseño de lenguajes de programación.
El estudiante aprenderá como se puede modelar algebraícamente el concepto de tipo de
datos.
Estudiará en detalle al cálculo lambda con tipos, sus sintaxis y el modelo de recursión.
CONTENIDO Y ESQUEMA DEL CURSO
1. El lenguaje PCF.
1.1. Sintaxis de PCF.
1.1.1. Boléanos y números naturales.
1.1.2. Apareamiento y funciones.
1.1.3. Declaración y azúcar sintáctica.
1.1.4. Recursión y operadores de punto fijo.
1.2. Programas PCF y sus semánticas.
1.2.1. Programas y resultados.
1.2.2. Semántica axiomática.
1.2.3. Semántica denotacional.
1.2.4. Semántica operacional.
1.2.5. Relaciones de Equivalencia definidas para cada forma de semántica.
1.3. Reducción PCF e interpretes simbólicos.
1.3.1. Reducción no determinística.
1.3.2. Estrategias de reducción.
1.3.3. Las estrategias reducción más izquierda y reducción retardada.
1.3.4. Reducción paralela.
1.3.5. PCF ávido.
1.4. Ejemplos de programación PCF, poder expresivo y limitaciones.
1.4.1. Registros y n-tuplas.
1.4.2. Buscando a los números naturales.
1.4.3. Iteración y recursión de cola.
1.4.4. Funciones recursivas totales.
1.4.5. Funciones recursivas parciales.
1.4.6. Indefinibilidad de operaciones paralelas.
2. Álgebra Universal y Tipos de datos algebraicos.
2.1. Preliminares de especificación algebraica.
2.2. Álgebras, firmas y términos.
2.2.1. Álgebras.
2.2.2. Sintaxis de términos algebraicos.
2.2.3. Álgebras y la interpretación de términos.
2.2.4. El lema de sustitución.
2.3. Ecuaciones, validez y completez.
2.3.1. Ecuaciones.
2.3.2. Álgebras de términos y sustitución.
2.3.3. Implicación semántica y un sistema de pruebas ecuacional.
2.3.4. Formas de Completez.
2.3.5. Congruencia, cocientes y completez deductiva.
2.3.6. Sorts no vacíos y la propiedad del modelo mínimo.
2.4. Homomorfismos e inicialidad.
2.4.1. Homomorfismos e isomorfismos
2.4.2. Álgebras iniciales.
2.5. Tipos de datos algebraicos.
2.5.1. Especificación y abstracción de datos.
2.5.2. Semántica del álgebra inicial e inducción sobre tipos de datos.
2.5.3. Ejemplos y valores error.
2.5.4. Enfoques alternativos a valores error.
3. Calculo lambda con tipos simples, modelos de cálculo lambda con tipos y recursión.
3.1. Tipos.
3.1.1. Sintaxis.
3.1.2. Interpretación de Tipos.
3.2. Términos.
3.2.1. Sintaxis sensible al contexto.
3.2.2. Sintaxis de términos .
3.2.3. Términos con producto, suma y tipo relacionado.
3.2.4. La correspondencia fórmulas como tipos.
3.2.5. Algoritmos de asignación de tipos (Typing).
3.3. Validez y completez.
3.3.1. Modelos generales y el significado de términos.
3.3.2. Estructuras aplicativas, extensionalidad y marcos.
3.3.3. La condición del modelo del medio ambiente.
3.3.4. Validez de tipos y ecuacional.
3.4. Modelos de teoria de dominios y puntos fijos.
3.4.1. Definiciones recursivas y operadores de punto fijo.
3.4.2. Ordenes parciales completos, producto lifting y cartesiano.
3.4.3. Funciones continuas.
3.4.4. Puntos fijos y la jerarquía del continuo completo.
3.4.5. Modelo de orden parcial completo para PCF.
3.5. Inducción de punto fijo.
3.6. Adecuación computacional y abstracción completa.
3.6.1. Teorema de aproximación y adecuación computacional.
3.6.2. Abstracción completa para PCF con operaciones paralelas.
3.7. Modelo de la teoría de recursión.
3.7.1. Introducción.
3.7.2. Conjuntos modestos.
3.7.3. Jerarquía recursiva completa.
4. Programas imperativos.
4.1. Programas While.
4.1.1. L-valores y R-valores.
4.1.2. Sintaxis de los programas While.
4.2. Semántica operacional
4.2.1. Símbolos básicos en expresiones.
4.2.2. Locaciones y almacenes.
4.2.3. Evaluación de expresiones.
4.2.4. Ejecución de comandos.
4.3. Semántica denotacional.
4.3.1. Cálculo lambda de asignación de tipos con almacenes.
4.3.2. Funciones semánticas.
4.3.3. Equivalencia de semántica operacional y denotacional.
4.4. Aserciones antes-después sobre programas While.
4.4.1. Aserciones de correctez de primer orden y parcial
4.4.2. Reglas de prueba.
4.4.3. Validez.
4.4.4. Completez relativa.
CRITERIOS DE EVALUACIÓN
1. Realización de dos exámenes parciales. Cada examen parcial representa el 20%
2. El alumno debe entregar una lista de ejercicios que se dejarán durante el curso. 20%.
3. Construcción de un programa. Entrega del programa 40%.
TEXTOS Y REFERENCIAS REQUERIDAS
Foundations for Programming Languages, J. C. Mitchell, MIT Press, 1996.
Semantics of Programming Languages: Structures and Techniques, G. A. Gunter, MIT
Press, 1992.
The Formal Semantics of Programming Languages, G. Winskel, MIT Press, 1993.